Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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