Why can't `rw` look inside lambda expressions?

Stream: general

[Johan Commelin]

I often find myself trying to do a rewrite, and then it fails miserably while it shouldn't. Suppose I have a finset.sum univ (\lam x, f(x + x)) in my goal, and I know that f is a group hom. Then I want to rewrite that f(x + x) to f(x) + f(x). But Lean always complains. So I have to do a little dance with rw show [relevant part goes here], which feels clumsy. What am I doing wrong?

[Simon Hudon]

rw can't rewrite bound variables. simp is more useful there.

[Simon Hudon]

If you're worried about simp trying too many rules, you can restrict it with simp only [my interesting rule] or disable individual simp rules with simp [my_rule, - no_no_rule]

[Johan Commelin]

It works!

[Simon Hudon]

:party_popper:

[Kevin Buzzard]

You can also use conv in (f(x+x)) begin rw ... end. See Patrick's conv notes in the mathlib docs.

[Johan Commelin]

Thanks, I'll take a look.

[Kevin Buzzard]

https://github.com/leanprover/mathlib/tree/master/docs/extras

[Kevin Buzzard]

conv.md

[Johan Commelin]

Ok, it was a long time ago that I read that doc. It's really cool! I will be able to use that quite a lot I guess.