rw under lambda

Stream: general

[Reid Barton]

rw refuses to perform rewrites inside a lambda, as far as I can tell. Is there a convenient way to do so?
For example, frequently my goal is of the form ∃ x, P x ∧ Q x and I would like to rewrite it to ∃ x, P x ∧ Q' x (where I know Q x ↔ Q' x).

[Simon Hudon]

use simp instead of rw if you want to rewrite under lambda. If you don't want simp to use default simp rules, you can do simp only [my_rule]

[Reid Barton]

Oops, I tried simp only, but I mixed up .symm and .mpr so it didn't appear to work. Thanks!

[Patrick Massot]

See also https://github.com/leanprover/mathlib/blob/master/docs/extras/conv.md

[Reid Barton]

I couldn't work out how to do this with conv:

example (h : ∃ a b, a + b = 0) : ∃ a b, b + a = 0 :=
begin
  conv begin
    -- use rw add_comm somehow
  end,
  exact h
end

[Reid Barton]

I tried congr, funext, congr but I got an error that I didn't understand on the second congr

[Simon Hudon]

try:

example : (∃ a b, a + b = 0) ↔ ∃ a b, b + a = 0 :=
by conv in (_ + _) begin
  rw add_comm,
end

[Reid Barton]

ah, interesting

[Simon Hudon]

This would also work, btw:

example (h : (∃ a b, a + b = 0)) : ∃ a b, b + a = 0 :=
begin
  conv in (_ + _)
  { rw add_comm },
  exact h
end

[Patrick Massot]

conv in ( _ = _) would also work, but I would be interested in seeing a solution without pattern matching. It seems we lack some navigation tactic (like to_lhs/to_rhs, congr). @Gabriel Ebner @Mario Carneiro any idea?