STG4 family union world 7/7

Stream: new members

[Thijs Vromen]

Can anyone give me some pointers for how to do level 7 of the family union world in the Set Theory Game?
( this one: https://adam.math.hhu.de/#/g/djvelleman/stg4/world/FamUnion/level/7 )
After doing what seems like default simplification steps I tend to repeat the exact same sequence of steps leading me to something that doesn't seem provable.

ext
rw [mem_inter_iff]
rw [mem_sUnion]
rw [mem_sUnion]
apply Iff.intro
intro h
use A
rw [mem_setOf]
apply And.intro
use A
apply And.intro

PS: I've used the "spoiler" option for the code above, but I can't see that it does much. Does anyone know how to make that work?

[Dan Velleman]

Did you think about whether A was the right choice when you did use A, or did you just guess?

[Dan Velleman]

After intro h, you have h : x ∈ A ∧ ∃ t ∈ F, x ∈ t. The second half of h says that something exists. When you know that something exists, it is almost always a good idea to use obtain to introduce a name for the thing that exists. I would do that right after intro h.

[Dan Velleman]

After you have used obtain, I would suggest that you think more about the meaning of the goal. The goal says that there exists some t with a complicated property: it must be an element of a certain set, and x must be an element of it. You need to figure out what set would have that property. That's the set you have to use, and it's not A. Note that you can apply use to a complicated expression--it doesn't have to be just a variable.

[Thijs Vromen]

thank you for the hints! I have indeed used obtain and then also tried using the variable that comes out of that (by default w), but got stuck just the same. But I hadn't considered using more complicated expressions, that sounds helpful! Since I hadn't considered that it was indeed a bit of a guessing game so far

[Dan Velleman]

There's a lesson here: Lean will let you use whatever you want when you are trying to prove an existential statement. But if you make the wrong choice, you may end up trying to prove something that is false.