World: Family Intersection World

Stream: new members

[Yagub Aliyev]

I am in Set theory game at level:
https://adam.math.hhu.de/#/g/djvelleman/stg4/world/FamInter/level/5
Objects:
U: Type
A: Set U
F: Set (Set U)
B: Set U
Assumptions:
h: A ⊆ ⋂₀ F
h0: B ∈ F
Goal:
A ⊆ B

I tried

apply h at h0

but it gives strange results. What do you recommend?

[Kyle Miller]

Is apply ... at ... covered in this? When I clicked on apply it doesn't mention this form. (Incidentally, you can make progress with it if you understand what the ? variables mean, and how you got to the goal state given the definition of subset and ⋂₀, but I don't think that is a very understandable proof.)

In any case, I would suggest using intro as a next step.

[Dan Velleman]

No, apply ... at ... is not covered in the set theory game.

Throughout the game, the advice for proving a subset statement has been to introduce first an arbitrary object and then the assumption that the object is an element of the left side of the subset statement.

[Dan Velleman]

I recommend a "put off thinking as long as possible" approach to proofs--especially for beginners. There are certain steps in proofs that you can do without thinking, and it is usually best to do those steps before you start thinking about why the theorem is true.

This proof is a good example of that. If your goal is A ⊆ B, then without even thinking about why the theorem is true, you can do two steps: introduce an arbitrary x, and assume that x is an element of A. It is only once you have done those steps that you are ready to think about the central issue in this proof, which is: if x is an element of A, why should it be an element of B?

Yes, there are exceptions. Occasionally some other approach works better. But if your goal is A ⊆ B and you're stuck, then I would say that you're thinking too soon. Do the automatic steps first; then start thinking.

[Yagub Aliyev]

I did intro and solved one direction (h1). I am stuck with the opposite direction :-(

Objects:
U: Type
A: Set U
F: Set (Set U)
B: Set U
a: U
S: Set U
Assumptions:
h1: A ⊆ ⋂₀ F → ∀ B ∈ F, A ⊆ B
h0: B ∈ F
h9: A ⊆ B
h: a ∈ B
h8: S ∈ F
Goal:
a ∈ S

[Dan Velleman]

I don't think your current assumptions imply your goal, so you've gone wrong somewhere.

I'm going to take a wild guess at how you got to where you are. You should be proving the implication (∀ B ∈ F, A ⊆ B) → A ⊆ ⋂₀ F. If you typed that in, but left out the parentheses, then Lean would interpret it as ∀ B ∈ F, (A ⊆ B → A ⊆ ⋂₀ F). That statement is not, in general, true, so if you try to prove it you'll get stuck. Is that how you got to where you are?

[Ruben Van de Velde]

(deleted)

[Ruben Van de Velde]

This is the goal state I get from introducing blindly:

H: ∀ B ∈ F, A ⊆ B
hx: x ∈ A
hs: s ∈ F
Goal:
x ∈ s

which is straightforward to finish

[Yagub Aliyev]

Thank you @Ruben Van de Velde
The mistake was with parentheses. I successfully completed the task after correction.

[Yagub Aliyev]

I am now at level:
https://adam.math.hhu.de/#/g/djvelleman/stg4/world/FamUnion/level/4

I did one direction (h1). I am stuck here.

Objects:
U: Type
AB: Set U
x: U
w: Set U
Assumptions:
h1: A ∪ B ⊆ ⋃₀ {A, B}
hw: w ∈ {A, B} ∧ x ∈ w
hA: w = A
Goal:
x ∈ A

[Kevin Buzzard]

Do you know the maths proof of how you want to continue?

[Yagub Aliyev]

Kevin Buzzard said:

Do you know the maths proof of how you want to continue?

From mathematics side it is kind of obvious. If w ∈ {A, B} ∧ x ∈ w
and w = A, then for sure x ∈ A. No? I don't know how to do this in Lean.

[Kevin Buzzard]

Which part of this argument can't you do in Lean? You need to (1) access the fact that x \in w (2) deduce x \in A from x \in w and w = A. I'm not sure how you've been playing this game (my impression is that you have switched off the "learn the tactics in order" switch and are just applying tactics randomly to anything) but surely the tactics which you have learnt so far in the game will get you through here.

[Yagub Aliyev]

Kevin Buzzard said:

Which part of this argument can't you do in Lean? You need to (1) access the fact that x \in w (2) deduce x \in A from x \in w and w = A. I'm not sure how you've been playing this game (my impression is that you have switched off the "learn the tactics in order" switch and are just applying tactics randomly to anything) but surely the tactics which you have learnt so far in the game will get you through here.

I could do (1) but can't do (2)

(1) access the fact that x \in w
done!

(2) deduce x \in A from x \in w and w = A.
?

I was trying many different tactics throughout the game but it seems I missed somewhere the tactic to use equality of sets or substitution tactic. I am stuck for real :/

Current status looks like this

U: Type
AB: Set U
x: U
w: Set U
Assumptions:
h1: A ∪ B ⊆ ⋃₀ {A, B}
hw: w ∈ {A, B} ∧ x ∈ w
hA: w = A
h6: x ∈ w
Goal:
x ∈ A

[Dan Velleman]

Take a look at the rewrite tactic.

[Dan Velleman]

The rewrite tactic was introduced in Complement World. The use of rewrite with statements of the form P ↔ Q was introduced in level 3 of that world, and the use with statements of the form P = Q was introduced in level 5.

[Yagub Aliyev]

Thank you I completed.