rw doesn't work under ∃

Stream: new members

[Maris Ozols]

Is there any reason why the rewrite here doesn't work?

import Mathlib.Data.Nat.Prime.Infinite

example (n : ℕ) : ∃ p, Nat.Prime p ∧ n ≤ p := by
  rw [and_comm]
  exact Nat.exists_infinite_primes n

[Kevin Buzzard]

The reason is commonly referred to as "rw doesn't work under binders" but this statement is not strictly accurate; more accurate would be "rw often doesn't work under binders". Try simp only [and_comm] or simp_rw [and_comm] and maybe you'll have more luck.

[Aaron Liu]

"rw doesn't match expressions containing bound variables"

[Ruben Van de Velde]

Though simp may have trouble because it loops. You can specify the and_comm more to avoid that, or use the conv tactic

[Kyle Miller]

conv is a great way to use rw for particular positions. To use it, you need to get acquainted with the enter mini-language, and also hover over expressions in the Infoview to know how things are encoded:

import Mathlib.Data.Nat.Prime.Infinite

example (n : ℕ) : ∃ p, Nat.Prime p ∧ n ≤ p := by
  conv => enter [1, _]; rw [and_comm]
  exact Nat.exists_infinite_primes n

If you use an identifier in place of _, then that names the existential binder as you enter.

The reason for the 1 is that existentials are encoded as Exists fun p => ..., so we need to enter the first explicit argument and then the function.

[Kyle Miller]

(In the very near future rw will work under binders.)

[Aaron Liu]

conv? is also great when it works (and when #25889 is merged it will work a lot more)