Tactics for ⊢ {x : ℝ | ∃ (a b : ℤ), p x a b } = q

Stream: new members

[Lars Ericson]

I have a goal of form:

⊢ {x : ℝ | ∃ (a b : ℤ), p x a b } = q

for example:

⊢ {x : ℝ | ∃ (a b : ℤ), x = ↑a + ↑b * 9 ^ (1 / 4)} = ↑((zsqrtd.to_real _).range)

What tactics or theorems are there in mathlib to rewrite this set equality into something I can operate on?

[Floris van Doorn]

ext and then rw with docs#set.mem_set_of_eq might be a good start?

[Lars Ericson]

Thanks, that rewrites the above to

⊢ (∃ (a b : ℤ), x = ↑a + ↑b * 9 ^ (1 / 4)) ↔ x ∈ ↑((zsqrtd.to_real _).range)

which seems helpful because now I can work with the existential quantifier directly and it's contents.