Stream: new members

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

Lars Ericson (Jan 07 2021 at 04:18):

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 (Jan 07 2021 at 05:55):

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

Lars Ericson (Jan 07 2021 at 17:43):

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.

Last updated: May 13 2021 at 06:15 UTC