World: Family Union World

Stream: new members

[Yagub Aliyev]

I am currently at the level https://adam.math.hhu.de/#/g/djvelleman/stg4/world/FamUnion/level/7

Objects:
U: Type
A: Set U
F: Set (Set U)

Goal:
A ∩ ⋃₀ F = ⋃₀ {B | ∃ S ∈ F, B = A ∩ S}

I started with the direction

h1: A ∩ ⋃₀ F ⊆ ⋃₀ {B | ∃ S ∈ F, B = A ∩ S}

But there is a serious obstacle to this.
Using "intro" and "obtain" I reduced it to this level:
Objects:
U: Type
A: Set U
F: Set (Set U)
x: U
w: Set U
Assumptions:
h: x ∈ A ∧ x ∈ ⋃₀ F
hA: x ∈ A
hw: w ∈ F ∧ x ∈ w
Goal:
∃ S ∈ F, w = A ∩ S

I know that I can "use w" but I can't prove w = A ∩ w from the assumptions. Any recommendation?

[Dan Velleman]

Using intro and obtain, I end up with the goal: x ∈ ⋃₀ {B | ∃ S ∈ F, B = A ∩ S}. And writing out the definition of that goal (with rewrite [fam_union_def]) leads to the goal ∃ S ∈ {B | ∃ S ∈ F, B = A ∩ S}, x ∈ S. I think you must have done one further step, which was to use w as the "witness" for S in the goal. Choosing a witness for an existential goal is always a somewhat risky step--you are free to use whatever you want as the witness, but if you make the wrong choice you can get stuck. That's what's happened in this case. You need to back up and choose your witness more carefully.

[Dan Velleman]

It might be confusing that the letter S is used for two different things in the goal. I'm going to tweak this world to try to avoid this double use of the letter S.