Rewriting with context in nested expressions (congruence rules)

Question

I am trying to prove the following example in Lean 4:

-- defining my own version of List.contains, because I could not figure out how 
-- to use the equality type class used in the existing one
def List.contains' (x: A): List A → Prop
  | [] => False
  | (y::ys) => x = y ∨ ys.contains' x

example
  {l: List Nat}
  {f: Nat → Nat}
  (h: ∀ (x: Nat), l.contains' x → (f (f x) = f x))
  : l.map (λx => f (f x)) = l.map (λx => f x)
  := by
    simp [h] -- fails

This example works without the l.contains' x precondition in h, but with the precondition it seems the context is missing.

My question is how I can teach Lean to do this rewrite automatically?

For context:

I am coming from Isabelle, where this example is simply:

theorem example: 
  assumes ‹∀x∈set l. f (f x) = f x›
  shows ‹map (λx. f (f x)) l = map (λx. f x) l›
  using assms by simp

What I tried so far:

Try 1

Since Isabelle uses congruence rules to guide the simplifier for nested terms, I tried to define a congruence rule in Lean as well:

@[congr]
def map_congr'
  {f g : A → B}
  {xs ys : List A}
  (h1: xs = ys)
  (h2: ∀(x: A), xs.contains' x → f x = g x)
  : xs.map f = ys.map g
  := sorry

However, this rule was not picked up by the simp, rw, or conv tactic.

Only manually applying worked:

example
  {l: List Nat}
  {f: Nat → Nat}
  (h: ∀ (x: Nat), l.contains' x → (f (f x) = f x))
  : l.map (λx => f (f x)) = l.map (λx => f x)
  := by
    apply map_congr' (xs := l)
    · exact show l = l from rfl
    · exact h

Try 2

Next, I tried to define a version of map that makes the fact that l.contains' x available in the function f:

def List.map' : (l: List A) → (f: (x: A) → l.contains' x → B) → List B
  | [], f => []
  | (x::xs), f =>
      have c1: (x::xs).contains' x := by simp [List.contains']
      f x c1 :: map' xs (fun y p =>
        have c2: (x::xs).contains' y := by simp [List.contains', p]
        f y c2)

I was expecting that this lets me use the rw or simp tactic, but again it failed:

example
  {l: List Nat}
  {f: Nat → Nat}
  (h: ∀ (x: Nat), l.contains' x → (f (f x) = f x))
  : l.map' (λx p => f (f x)) = l.map' (λx p => f x)
  := by
      rw [h] -- tactic 'rewrite' failed, did not find instance of the pattern in the target expression

It worked with the conv tactic, but my feeling is that there is an easier way to do this.

example
  {l: List Nat}
  {f: Nat → Nat}
  (h: ∀ (x: Nat), l.contains' x → (f (f x) = f x))
  : l.map' (λx p => f (f x)) = l.map' (λx p => f x)
  := by
      conv =>
        pattern (λx p => f (f x))
        intro x
        intro p
        rw [h x p]

Answer 1

You can see your congruence theorem is being applied using set_option trace.Debug.Meta.Tactic.simp true, but by default simp does not dynamically extend the context during traversal with local facts such as from xs.contains' x → _. You can tell it to do so via

by simp (config := { contextual := true }) [h]

or you can use the "heavy-weight" by simp_all that does both contextual simplification as well as simplification of assumptions via other assumptions.