# Zulip Chat Archive

## 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!

#### Patrick Massot (May 04 2018 at 19:19):

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

#### 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 -- use rw add_comm somehow 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 rw add_comm, end

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

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 (_ + _) { rw add_comm }, 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: Dec 20 2023 at 11:08 UTC