rw inside quantifier

Stream: new members

[Darij Grinberg]

How do I make Lean's rw do its job inside a quantifier?
Say, I have a goal of the form ... ↔ ∃ a ∈ range (n + 1), .... I want to rewrite the a ∈ range (n + 1) part using mem_range, but without necessarily having avalanche effects elsewhere in the goal (there's simp for that). Is there some "stronger rewrite" for that?

[Etienne Marion]

You can use simp_rw.

[Kenny Lau]

simp (only) and simp_rw both work for this case.

[Darij Grinberg]

Ah, hadn't heard about simp_rw. But it does too much, doesn't it? Can I rewrite only a specific instance?

[Ruben Van de Velde]

You can use conv for that

[Darij Grinberg]

ah!

[Kenny Lau]

btw just in case you didn't know, ∃ a ∈ x, p is sugar for ∃ a, a ∈ x ∧ p

[Darij Grinberg]

yep, this is why I was hoping for mem_range to help :)