How to solve logic proofs

edit

-- 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