Rewrite in Existential Membership

Stream: new members

[Luna]

Is there a good way to rewrite a x ∈ S in ∃ x ∈ S, P x?

I'm trying to apply rw [Subgroup.mem_map] to ∃ x ∈ Subgroup.map φ S, P x and it fails. I understand why since existential membership is syntactically and grammatically different. But is there a good way to get around that?

[Yaël Dillies]

Do you know about simp_rw?

[Luna]

I do not. That is exactly what I was looking for. Thank you!

[Yaël Dillies]

Luna said:

I understand why since existential membership is syntactically and grammatically different.

I am not quite sure what you mean by "grammatically different", but it certainly isn't syntactically different. ∃ x ∈ s, p x is notation for ∃ x, x ∈ s ∧ p x and the reason you can't use rw on the x ∈ s inside it is that rw cannot rewrite subexpressions that depend on a binder (the binder here being x). simp (and therefore simp_rw) uses another algorithm for rewriting which doesn't have this limitation