diff --git a/analysis/Analysis/Section_3_4.lean b/analysis/Analysis/Section_3_4.lean
index dd93fec..e42055f 100644
--- a/analysis/Analysis/Section_3_4.lean
+++ b/analysis/Analysis/Section_3_4.lean
@@ -34,7 +34,20 @@ theorem SetTheory.Set.mem_image {X Y:Set} (f:X → Y) (S: Set) (y:Object) :
 
 /-- Alternate definition of image using axiom of specification -/
 theorem SetTheory.Set.image_eq_specify {X Y:Set} (f:X → Y) (S: Set) :
-    image f S = Y.specify (fun y ↦ ∃ x:X, x.val ∈ S ∧ f x = y) := by sorry
+    image f S = Y.specify (fun y ↦ ∃ x:X, x.val ∈ S ∧ f x = y) := by
+  ext y
+  constructor
+  · intro h
+    rw [mem_image] at h
+    obtain ⟨x, hx, hxy⟩ := h
+    rw [specification_axiom'', ←hxy]
+    use (f x).property, x
+  intro h
+  rw [mem_image]
+  rw [specification_axiom''] at h
+  obtain ⟨hy, ⟨x, hx, hxy⟩⟩ := h
+  use x, hx
+  rw [hxy]
 
 /--
   Connection with Mathlib's notion of image.  Note the need to utilize the `Subtype.val` coercion
@@ -69,10 +82,19 @@ theorem SetTheory.Set.image_f_3_4_2 : image f_3_4_2 {1,2,3} = {2,4,6} := by
 example : (fun n:ℤ ↦ n^2) '' {-1,0,1,2} = {0,1,4} := by aesop
 
 theorem SetTheory.Set.mem_image_of_eval {X Y:Set} (f:X → Y) (S: Set) (x:X) :
-    x.val ∈ S → (f x).val ∈ image f S := by sorry
+    x.val ∈ S → (f x).val ∈ image f S := by
+  intro h
+  rw [mem_image]
+  use x
 
 theorem SetTheory.Set.mem_image_of_eval_counter :
-    ∃ (X Y:Set) (f:X → Y) (S: Set) (x:X), ¬((f x).val ∈ image f S → x.val ∈ S) := by sorry
+    ∃ (X Y:Set) (f:X → Y) (S: Set) (x:X), ¬((f x).val ∈ image f S → x.val ∈ S) := by
+  use Nat, Nat, fun x ↦ 0, {((0:Nat):Object)}, 1
+  push_neg
+  simp only [mem_image, mem_singleton, and_true]
+  constructor
+  · use 0
+  simp [Subtype.coe_ne_coe]
 
 /--
   Definition 3.4.4 (inverse images).
@@ -119,7 +141,10 @@ theorem SetTheory.Set.preimage_f_3_4_2 : preimage f_3_4_2 {2,4,6} = {1,2,3} := b
   all_goals simp
 
 theorem SetTheory.Set.image_preimage_f_3_4_2 :
-    image f_3_4_2 (preimage f_3_4_2 {1,2,3}) ≠ {1,2,3} := by sorry
+    image f_3_4_2 (preimage f_3_4_2 {1,2,3}) ≠ {1,2,3} := by
+  intro h
+  have : 1 ∉ image f_3_4_2 (preimage f_3_4_2 {1, 2, 3}) := by simp
+  simp_all
 
 /-- Example 3.4.7 (using the Mathlib notion of preimage) -/
 example : (fun n:ℤ ↦ n^2) ⁻¹' {0,1,4} = {-2,-1,0,1,2} := by
@@ -129,7 +154,13 @@ example : (fun n:ℤ ↦ n^2) ⁻¹' {0,1,4} = {-2,-1,0,1,2} := by
   on_goal 3 => have : 2 ^ 2 = (4:ℤ) := (by norm_num); rw [←h, sq_eq_sq_iff_eq_or_eq_neg] at this
   all_goals aesop
 
-example : (fun n:ℤ ↦ n^2) ⁻¹' ((fun n:ℤ ↦ n^2) '' {-1,0,1,2}) ≠ {-1,0,1,2} := by sorry
+example : (fun n:ℤ ↦ n^2) ⁻¹' ((fun n:ℤ ↦ n^2) '' {-1,0,1,2}) ≠ {-1,0,1,2} := by
+  intro h
+  rw [Set.ext_iff] at h
+  specialize h (-2)
+  have : -2 ∉ ({-1, 0, 1, 2}: _root_.Set ℤ) := by simp
+  apply h.not.mpr this
+  simp
 
 instance SetTheory.Set.inst_pow : Pow Set Set where
   pow := SetTheory.pow
@@ -181,13 +212,35 @@ theorem SetTheory.Set.example_3_4_9 (F:Object) :
 
 /-- Exercise 3.4.6 (i). One needs to provide a suitable definition of the power set here. -/
 def SetTheory.Set.powerset (X:Set) : Set :=
-  (({0,1} ^ X): Set).replace (P := sorry) (by sorry)
+  (({0,1} ^ X): Set).replace (P := fun F Y ↦
+    ∃ f : X → ({0,1}: Set), F = (f : Object) ∧ Y = (preimage f {1})
+  ) (by aesop)
 
 open Classical in
 /-- Exercise 3.4.6 (i) -/
 @[simp]
 theorem SetTheory.Set.mem_powerset {X:Set} (x:Object) :
-    x ∈ powerset X ↔ ∃ Y:Set, x = Y ∧ Y ⊆ X := by sorry
+    x ∈ powerset X ↔ ∃ Y:Set, x = Y ∧ Y ⊆ X := by
+  rw [powerset, replacement_axiom]
+  constructor
+  · rintro ⟨_, ⟨f, _, hfx⟩⟩
+    use preimage f {1}, hfx
+    simp only [subset_def, mem_preimage']
+    rintro _ ⟨a, ⟨rfl, _⟩⟩
+    use a.property
+  intro h
+  obtain ⟨Y, rfl, _⟩ := h
+  let f : X → ({0,1}: Set) := fun x ↦
+    if x.val ∈ Y then ⟨1, by simp⟩
+    else ⟨0, by simp⟩
+  have hf := (powerset_axiom _).mpr (by use f)
+  use ⟨_, hf⟩, f
+  constructor
+  · rfl
+  congr
+  apply Set.ext
+  simp only [mem_preimage']
+  aesop
 
 /-- Lemma 3.4.10 -/
 theorem SetTheory.Set.exists_powerset (X:Set) :
@@ -227,7 +280,9 @@ theorem SetTheory.Set.union_axiom (A: Set) (x:Object) :
 /-- Example 3.4.12 -/
 theorem SetTheory.Set.example_3_4_12 :
     union { (({2,3}:Set):Object), (({3,4}:Set):Object), (({4,5}:Set):Object) } = {2,3,4,5} := by
-  sorry
+  apply Set.ext
+  simp only [union_axiom, Insert.insert]
+  aesop
 
 /-- Connection with Mathlib union -/
 theorem SetTheory.Set.union_eq (A: Set) :
@@ -265,7 +320,13 @@ theorem SetTheory.Set.iUnion_eq (I: Set) (A: I → Set) :
     (iUnion I A : _root_.Set Object) = ⋃ α, (A α: _root_.Set Object) := by
   ext; simp only [mem_iUnion, _root_.Set.mem_setOf_eq, _root_.Set.mem_iUnion]
 
-theorem SetTheory.Set.iUnion_of_empty (A: (∅:Set) → Set) : iUnion (∅:Set) A = ∅ := by sorry
+theorem SetTheory.Set.iUnion_of_empty (A: (∅:Set) → Set) : iUnion (∅:Set) A = ∅ := by
+  ext
+  simp only [not_mem_empty, iff_false, mem_iUnion]
+  push_neg
+  intro α
+  have := α.property
+  aesop
 
 /-- Indexed intersection -/
 noncomputable abbrev SetTheory.Set.nonempty_choose {I:Set} (hI: I ≠ ∅) : I :=
@@ -279,61 +340,154 @@ noncomputable abbrev SetTheory.Set.iInter (I: Set) (hI: I ≠ ∅) (A: I → Set
 
 theorem SetTheory.Set.mem_iInter {I:Set} (hI: I ≠ ∅) (A: I → Set) (x:Object) :
     x ∈ iInter I hI A ↔ ∀ α:I, x ∈ A α := by
-  sorry
+  constructor
+  · intro h
+    rw [specification_axiom''] at h
+    exact h.2
+  intro h
+  rw [specification_axiom'']
+  use h (nonempty_choose hI)
 
 /-- Exercise 3.4.1 -/
 theorem SetTheory.Set.preimage_eq_image_of_inv {X Y V:Set} (f:X → Y) (f_inv: Y → X)
   (hf: Function.LeftInverse f_inv f ∧ Function.RightInverse f_inv f) (hV: V ⊆ Y) :
-    image f_inv V = preimage f V := by sorry
+    image f_inv V = preimage f V := by
+  ext
+  simp only [mem_image, mem_preimage']
+  constructor
+  · rintro ⟨y, hy, rfl⟩
+    use (f_inv y), rfl
+    rwa [hf.2]
+  rintro ⟨x, rfl, hx⟩
+  use (f x), hx
+  rw [hf.1]
 
 /- Exercise 3.4.2.  State and prove an assertion connecting `preimage f (image f S)` and `S`. -/
--- theorem SetTheory.Set.preimage_of_image {X Y:Set} (f:X → Y) (S: Set) (hS: S ⊆ X) : sorry := by sorry
+theorem SetTheory.Set.preimage_of_image {X Y:Set} (f:X → Y) (S: Set) (hS: S ⊆ X) :
+    S ⊆ preimage f (image f S) := by
+  simp only [subset_def, mem_preimage', mem_image] at *
+  intro x xs
+  let x': X := ⟨x, hS x xs⟩
+  use x', rfl, x'
 
 /- Exercise 3.4.2.  State and prove an assertion connecting `image f (preimage f U)` and `U`.
 Interestingly, it is not needed for U to be a subset of Y. -/
--- theorem SetTheory.Set.image_of_preimage {X Y:Set} (f:X → Y) (U: Set) : sorry := by sorry
+theorem SetTheory.Set.image_of_preimage {X Y:Set} (f:X → Y) (U: Set) :
+    image f (preimage f U) ⊆ U := by
+  simp only [subset_def, mem_image]
+  rintro y ⟨x, hx, rfl⟩
+  rwa [mem_preimage] at hx
 
 /- Exercise 3.4.2.  State and prove an assertion connecting `preimage f (image f (preimage f U))` and `preimage f U`.
 Interestingly, it is not needed for U to be a subset of Y.-/
--- theorem SetTheory.Set.preimage_of_image_of_preimage {X Y:Set} (f:X → Y) (U: Set) : sorry := by sorry
+theorem SetTheory.Set.preimage_of_image_of_preimage {X Y:Set} (f:X → Y) (U: Set) :
+    preimage f (image f (preimage f U)) = preimage f U := by
+  aesop
 
 /--
   Exercise 3.4.3.
 -/
 theorem SetTheory.Set.image_of_inter {X Y:Set} (f:X → Y) (A B: Set) :
-    image f (A ∩ B) ⊆ (image f A) ∩ (image f B) := by sorry
+    image f (A ∩ B) ⊆ (image f A) ∩ (image f B) := by
+  simp only [subset_def]
+  aesop
 
 theorem SetTheory.Set.image_of_diff {X Y:Set} (f:X → Y) (A B: Set) :
-    (image f A) \ (image f B) ⊆ image f (A \ B) := by sorry
+    (image f A) \ (image f B) ⊆ image f (A \ B) := by
+  simp only [subset_def, mem_image, mem_inter, mem_sdiff]
+  rintro y ⟨⟨x, ⟨h1, h2⟩⟩, h'⟩
+  have : (x: Object) ∉ B := by contrapose! h'; use x
+  use x, ⟨h1, this⟩
 
 theorem SetTheory.Set.image_of_union {X Y:Set} (f:X → Y) (A B: Set) :
-    image f (A ∪ B) = (image f A) ∪ (image f B) := by sorry
+    image f (A ∪ B) = (image f A) ∪ (image f B) := by
+  aesop
 
 def SetTheory.Set.image_of_inter' : Decidable (∀ X Y:Set, ∀ f:X → Y, ∀ A B: Set, image f (A ∩ B) = (image f A) ∩ (image f B)) := by
   -- The first line of this construction should be either `apply isTrue` or `apply isFalse`
-  sorry
+  apply isFalse
+  push_neg
+  let f : nat → nat := fun x ↦ 0
+  use nat, nat, f, {1}, {2}
+  intro h
+  rw [show ({1} ∩ {2}: Set) = ∅ by apply ext; simp] at h
+  rw [show (image f ∅) = ∅ by apply ext; simp [mem_image]] at h
+  symm at h
+  rw [eq_empty_iff_forall_notMem] at h
+  contrapose! h
+  simp only [mem_inter, mem_image, f]
+  use 0
+  constructor
+  · use 1
+    norm_num
+  use 2
+  norm_num
 
 def SetTheory.Set.image_of_diff' : Decidable (∀ X Y:Set, ∀ f:X → Y, ∀ A B: Set, image f (A \ B) = (image f A) \ (image f B)) := by
   -- The first line of this construction should be either `apply isTrue` or `apply isFalse`
-  sorry
+  apply isFalse
+  push_neg
+  let f : nat → nat := fun x ↦ 0
+  use nat, nat, f, {1, 2}, {2}
+  rw [show ({1, 2}: Set) \ {2} = {1} by apply ext; aesop]
+  intro h
+  rw [Set.ext_iff] at h
+  specialize h 0
+  have : 0 ∈ image f {1} := by rw [mem_image]; use 1; simp [f]
+  have : 0 ∈ image f {2} := by rw [mem_image]; use 2; simp [f]
+  simp_all [f]
 
 /-- Exercise 3.4.4 -/
 theorem SetTheory.Set.preimage_of_inter {X Y:Set} (f:X → Y) (A B: Set) :
-    preimage f (A ∩ B) = (preimage f A) ∩ (preimage f B) := by sorry
+    preimage f (A ∩ B) = (preimage f A) ∩ (preimage f B) := by
+  aesop
 
 theorem SetTheory.Set.preimage_of_union {X Y:Set} (f:X → Y) (A B: Set) :
-    preimage f (A ∪ B) = (preimage f A) ∪ (preimage f B) := by sorry
+    preimage f (A ∪ B) = (preimage f A) ∪ (preimage f B) := by
+  aesop
 
 theorem SetTheory.Set.preimage_of_diff {X Y:Set} (f:X → Y) (A B: Set) :
-    preimage f (A \ B) = (preimage f A) \ (preimage f B)  := by sorry
+    preimage f (A \ B) = (preimage f A) \ (preimage f B)  := by
+  aesop
 
 /-- Exercise 3.4.5 -/
 theorem SetTheory.Set.image_preimage_of_surj {X Y:Set} (f:X → Y) :
-    (∀ S, S ⊆ Y → image f (preimage f S) = S) ↔ Function.Surjective f := by sorry
+    (∀ S, S ⊆ Y → image f (preimage f S) = S) ↔ Function.Surjective f := by
+  constructor
+  · intro h y
+    simp only [subset_def, Set.ext_iff, mem_singleton, mem_image] at h
+    specialize h _ (by aesop) y
+    obtain ⟨x, ⟨_, hx⟩⟩ := h.mpr (by aesop)
+    use x, by rwa [coe_inj] at hx
+  intro h S hS
+  apply ext
+  intro y
+  simp only [mem_image, mem_preimage]
+  constructor
+  · rintro ⟨x, ⟨hx, rfl⟩⟩
+    exact hx
+  intro hy
+  obtain ⟨x, hx⟩ := h ⟨y, hS y hy⟩
+  use x, by rwa [hx], by rw [hx]
 
 /-- Exercise 3.4.5 -/
 theorem SetTheory.Set.preimage_image_of_inj {X Y:Set} (f:X → Y) :
-    (∀ S, S ⊆ X → preimage f (image f S) = S) ↔ Function.Injective f := by sorry
+    (∀ S, S ⊆ X → preimage f (image f S) = S) ↔ Function.Injective f := by
+  constructor
+  · intro h x1 x2 hf
+    simp only [subset_def] at h
+    have hx: ((f x2): Object) ∈ image f {(x2: Object)} := by rw [mem_image]; aesop
+    rwa [←hf, ←mem_preimage, h _ (by aesop), mem_singleton, coe_inj] at hx
+  intro h S hS
+  ext x
+  constructor
+  · simp only [mem_preimage', mem_image]
+    rintro ⟨x1, rfl, x2, hx2, heq⟩
+    rw [coe_inj] at heq
+    rwa [←h heq]
+  intro hx
+  simp only [mem_preimage', mem_image]
+  use ⟨x, hS x hx⟩, rfl, ⟨x, hS x hx⟩
 
 /-- Helper lemma for Exercise 3.4.7. -/
 @[simp]
@@ -349,40 +503,87 @@ lemma SetTheory.Set.mem_union_powerset_replace_iff {S : Set} {P : S.powerset →
 /-- Exercise 3.4.7 -/
 theorem SetTheory.Set.partial_functions {X Y:Set} :
     ∃ Z:Set, ∀ F:Object, F ∈ Z ↔ ∃ X' Y':Set, X' ⊆ X ∧ Y' ⊆ Y ∧ ∃ f: X' → Y', F = f := by
-  sorry
+  use union (Y.powerset.replace (P := fun oY' outer ↦
+    outer = union (X.powerset.replace (P := fun oX' inner ↦
+      ∃ (X' Y' : Set),
+        oX'.val = X' ∧
+        oY'.val = Y' ∧
+        inner = (Y' ^ X': Set)
+    ) (by simp_all))
+  ) (by simp_all))
+  intro F
+  constructor
+  · intro hF
+    simp only [mem_union_powerset_replace_iff, EmbeddingLike.apply_eq_iff_eq] at hF
+    obtain ⟨⟨oY', hY'⟩, _, rfl, hF⟩ := hF
+    simp only [mem_union_powerset_replace_iff, EmbeddingLike.apply_eq_iff_eq] at hF
+    obtain ⟨⟨oX', hX'⟩, Y'X', hF, hF'⟩ := hF
+    simp only [EmbeddingLike.apply_eq_iff_eq] at hF
+    obtain ⟨X', Y', rfl, rfl, rfl⟩ := hF
+    simp_all only [mem_powerset', powerset_axiom]
+    obtain ⟨f, hF⟩ := hF'
+    use X', Y'
+    use hX', hY'
+    use f, hF.symm
+  rintro ⟨X', Y', hX', hY', f, rfl⟩
+  simp_all [mem_union_powerset_replace_iff, EmbeddingLike.apply_eq_iff_eq,
+    exists_eq_left, Subtype.exists]
+  use Y', by simp_all
+  use X', by simp_all
+  use Y' ^ X', by simp_all
+  rw [powerset_axiom]
+  use f
 
 /--
   Exercise 3.4.8.  The point of this exercise is to prove it without using the
   pairwise union operation `∪`.
 -/
 theorem SetTheory.Set.union_pair_exists (X Y:Set) : ∃ Z:Set, ∀ x, x ∈ Z ↔ (x ∈ X ∨ x ∈ Y) := by
-  sorry
+  use union {(X: Object), (Y: Object)}
+  simp [union_axiom]
+  aesop
 
 /-- Exercise 3.4.9 -/
 theorem SetTheory.Set.iInter'_insensitive {I:Set} (β β':I) (A: I → Set) :
-    iInter' I β A = iInter' I β' A := by sorry
+    iInter' I β A = iInter' I β' A := by
+  ext
+  simp_all
 
 /-- Exercise 3.4.10 -/
 theorem SetTheory.Set.union_iUnion {I J:Set} (A: (I ∪ J:Set) → Set) :
     iUnion I (fun α ↦ A ⟨ α.val, by simp [α.property]⟩)
     ∪ iUnion J (fun α ↦ A ⟨ α.val, by simp [α.property]⟩)
-    = iUnion (I ∪ J) A := by sorry
+    = iUnion (I ∪ J) A := by
+  ext
+  simp only [mem_iUnion, mem_union]
+  aesop
 
 /-- Exercise 3.4.10 -/
-theorem SetTheory.Set.union_of_nonempty {I J:Set} (hI: I ≠ ∅) (hJ: J ≠ ∅) : I ∪ J ≠ ∅ := by sorry
+theorem SetTheory.Set.union_of_nonempty {I J:Set} (hI: I ≠ ∅) (hJ: J ≠ ∅) : I ∪ J ≠ ∅ := by
+  intro h
+  simp_all [Set.ext_iff]
 
 /-- Exercise 3.4.10 -/
 theorem SetTheory.Set.inter_iInter {I J:Set} (hI: I ≠ ∅) (hJ: J ≠ ∅) (A: (I ∪ J:Set) → Set) :
     iInter I hI (fun α ↦ A ⟨ α.val, by simp [α.property]⟩)
     ∩ iInter J hJ (fun α ↦ A ⟨ α.val, by simp [α.property]⟩)
-    = iInter (I ∪ J) (union_of_nonempty hI hJ) A := by sorry
+    = iInter (I ∪ J) (union_of_nonempty hI hJ) A := by
+  ext x
+  simp only [mem_iInter, mem_inter]
+  aesop
 
 /-- Exercise 3.4.11 -/
 theorem SetTheory.Set.compl_iUnion {X I: Set} (hI: I ≠ ∅) (A: I → Set) :
-    X \ iUnion I A = iInter I hI (fun α ↦ X \ A α) := by sorry
+    X \ iUnion I A = iInter I hI (fun α ↦ X \ A α) := by
+  apply ext; intro x
+  simp only [mem_sdiff, mem_iUnion]
+  aesop
 
 /-- Exercise 3.4.11 -/
 theorem SetTheory.Set.compl_iInter {X I: Set} (hI: I ≠ ∅) (A: I → Set) :
-    X \ iInter I hI A = iUnion I (fun α ↦ X \ A α) := by sorry
+    X \ iInter I hI A = iUnion I (fun α ↦ X \ A α) := by
+  ext
+  simp only [mem_sdiff, mem_iInter, mem_iUnion]
+  aesop
 
 end Chapter3