## Stream: general

### Topic: rw under lambda

#### Reid Barton (May 04 2018 at 18:33):

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 (May 04 2018 at 18:35):

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 (May 04 2018 at 18:39):

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

#### Reid Barton (May 04 2018 at 19:59):

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
end,
exact h
end


#### Reid Barton (May 04 2018 at 20:00):

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

#### Simon Hudon (May 04 2018 at 20:05):

try:

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


ah, interesting

#### Simon Hudon (May 04 2018 at 20:31):

This would also work, btw:

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


#### Patrick Massot (May 04 2018 at 21:48):

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?

Last updated: May 11 2021 at 00:31 UTC