# How to solve logic proofs

-- Instructions: Replace all "sorry"s with proofs.
-- Hint: The two lemmas are lemmas and not examples for a reason.
open set
variables {U I : Type}
variables A B C : set U
variables D E : I → set U
variable u : U
def Union (A : I → set U) : set U := { x | ∃ i : I, x ∈ A i }
notation `∪`

binders `,`

r:(scoped f, Union f) := r
def Inter (A : I → set U) : set U := { x | ∀ i : I, x ∈ A i }
notation `∩`

binders `,`

r:(scoped f, Inter f) := r
variable ext {A B : set U} (h : ∀ x : U, x ∈ A ↔ x ∈ B) : A = B

1.example : A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C) := sorry

2.example : (∩ i, D i) ∪ (∩ i, E i) ⊆ ∩ i, (D i ∪ E i) := sorry

3.lemma subsets_are_transitive {X Y Z : set U} (h1 : X ⊆ Y) (h2 : Y ⊆ Z) : X ⊆ Z := sorry

4.lemma biggest_subset (X : set U) : X ∈ powerset X := sorry

5.example : (A ⊆ B) ↔ (powerset A) ⊆ (powerset B) := sorry

I'm afraid that nobody on

`ask.agemath.org`

will do your homework for you.However, you may deign have a look at the relevant documentation.