Rewrite tactic fails in lambda body

Stream: lean4

[Tomas Skrivan]

I have a lemma that should be able to rewrite lamba's body, but it fails and claims that tactic 'rewrite' failed, did not find instance of the pattern in the target expression

Example:

variable {X Y} [Add X] [Add Y]
instance : Add (X×Y) := ⟨λ p q => (p.1 + q.1, p.2 + q.2)⟩

def foo (x x' : X) (y y' : Y) : (x, y) + (x', y') = (x + x', y + y') := sorry

def bar : (λ (x : X) (y : Y) => (x, y) + (x, y) + (x, y)) = (λ x y => (x + x + x, y + y + y)) :=
by
  -- funext x y
  rw [foo]; rw [foo] -- fails

Why is rewrite failing here? Am I doing something wrong?

[Patrick Massot]

At least in lean 3 the rewrite tactic was never meant to work in a lambda body (the simplifier does).

[Tomas Skrivan]

Ok. In this minimal example marking foo with @[simp] does the job but in my actual code the simplified does nothing. I have to investigate further.

[Leonardo de Moura]

You can also use conv mode to go inside lambdas and then apply rw.
https://leanprover.github.io/theorem_proving_in_lean4/conv.html
Here is your example

example : (λ (x : X) (y : Y) => (x, y) + (x, y) + (x, y)) = (λ x y => (x + x + x, y + y + y)) := by
 conv => enter [1, x, y]; rw [foo]

-- same as above but without `enter` macro
example : (λ (x : X) (y : Y) => (x, y) + (x, y) + (x, y)) = (λ x y => (x + x + x, y + y + y)) := by
 conv => lhs; intro x y; rw [foo]

[Tomas Skrivan]

Thanks a lot for the link to the doc. Google always took me to https://leanprover.github.io/lean4/doc/ and there the section on tactic is really limited.