## Stream: new members

### Topic: rw on sub expressions?

#### Martin C. Martin (Feb 12 2023 at 14:29):

Why can't rw find an instance of P ∧ Q here?

example : ∃ (n : ℕ ), 10 < n ∧ n < 20 :=
begin
rw and_comm,
sorry
end


How can I swap the order of the conjuncts in the goal?

#### Pedro Sánchez Terraf (Feb 12 2023 at 14:32):

Might be related to the fact that rw finds it difficult to work under binders

#### Martin C. Martin (Feb 12 2023 at 14:34):

Interesting, thanks! The suggestion in that thread, using simp_rw, doesn't work for me. Is there a way to swap the order of the conjuncts?

#### Pedro Sánchez Terraf (Feb 12 2023 at 14:37):

(I'm also a new member). For fine tuning, you have the conv mode.

#### Pedro Sánchez Terraf (Feb 12 2023 at 14:48):

I also don't know why simp_rw won't work. Here's one solution (surely not an optimal one), using the approach above.

#### Riccardo Brasca (Feb 12 2023 at 15:49):

You can also try simp_rw.

#### Michael Stoll (Feb 12 2023 at 15:56):

rwdoes not work on expressions that contain bound variables. simp_rw does, but applies lemmas repeatedly and so gets trapped in a loop when you give it and_comm. simp_rw [and_comm (10 < _)] does work, since the lemma applies only once with a left argument to and that matches 10 < _.

#### Gareth Ma (Feb 12 2023 at 16:36):

Or as Kevin Buzzard taught me, simp_rw uses simp only under the hood, and for the latter there is a context (ctx) optional parameter. So you can do this:

example : ∃ (n : ℕ), 10 < n ∧ n < 20 :=
begin
-- rw and_comm,
-- simp_rw [and_comm],
simp only [and_comm _] { single_pass := tt },
end


#### Gareth Ma (Feb 12 2023 at 16:36):

You need this when specifying the arguments doesn't work, which happened to me a while ago

Last updated: Dec 20 2023 at 11:08 UTC