Polish further.

Bookshelf/Enderton/Set/Chapter_6.lean

@@ -935,23 +935,76 @@ natural numbers `m, n ∈ ω` such that `dom f ≈ m`, `ran f ≈ n`, and `m ≥
 theorem finite_dom_ran_size [Nonempty α] {A B : Set α}
   (hA : Set.Finite A) (hB : Set.Finite B) (hf : Set.MapsTo f A B)
   : ∃ m n : ℕ, A ≈ Set.Iio m ∧ f '' A ≈ Set.Iio n ∧ m ≥ n := by
+/-
+> Let `A` and `B` be finite sets and `f : A → B` be a function. By definition of
+> finite sets, there exists natural numbers `m, p ∈ ω` such that `A ≈ m` and
+> `B ≈ p`. By definition of the domain of a function, `dom f = A`. Thus
+> `dom f ≈ m`.
+-/
   have ⟨m, hm⟩ := Set.finite_iff_equinumerous_nat.mp hA
   have ⟨p, hp⟩ := Set.finite_iff_equinumerous_nat.mp hB
+/-
+> By *Theorem 6A*, there exists a one-to-one correspondence `g` between `m` and
+> `dom f = A`.
+-/
   have ⟨g, hg⟩ := Set.equinumerous_symm hm
-
+/-
+> For all `y ∈ ran f`, consider `f⁻¹⟦{y}⟧`. Let
+>
+> `A_y = {x ∈ m | f(g(x)) = y}`.
+-/
   let A_y y := { x ∈ Set.Iio m | f (g x) = y }
-  have hA₁ : ∀ y ∈ B, A_y y ≈ f ⁻¹' {y} := by
+/-
+> Since `g` is a one-to-one correspondence, it follows that `A_y ≈ f⁻¹⟦{y}⟧`.
+-/
+  have hA₁ : ∀ y, y ∈ f '' A → A_y y ≈ A ∩ f ⁻¹' {y} := by
+    intro y hy
+    refine ⟨fun x => g x, ?_, ?_, ?_⟩
+    · -- `Set.MapsTo`
+      intro x hx
+      simp only [Set.mem_Iio, Set.mem_setOf_eq, Set.mem_preimage, Set.mem_singleton_iff] at hx ⊢
+      exact ⟨hg.left hx.left, hx.right⟩
+    · -- `Set.InjOn`
+      intro x₁ hx₁ x₂ hx₂ hf
+      exact hg.right.left hx₁.left hx₂.left hf
+    · -- `Set.SurjOn`
+      unfold Set.SurjOn Set.preimage Set.image
+      rw [Set.subset_def]
+      simp only [Set.mem_singleton_iff, Set.mem_inter_iff, Set.mem_setOf_eq, Set.mem_Iio]
+      intro x ⟨hx₁, hx₂⟩
+      have hx₃ := hg.right.right hx₁
+      simp only [Set.mem_image, Set.mem_Iio] at hx₃
+      have ⟨z, hz⟩ := hx₃
+      exact ⟨z, ⟨hz.left, hz.right ▸ hx₂⟩, hz.right⟩
+/-
+> Since `A_y` is a nonempty subset of natural numbers, the
+> *Well Ordering of `ω`* implies there exists a least element, say `q_y`.
+-/
+  have hA₂ : ∀ y, y ∈ f '' A → Set.Nonempty (A_y y) := by
+    intro y hy
+    unfold Set.Nonempty
+    simp only [Set.mem_image, Set.mem_Iio, Set.mem_setOf_eq] at hy ⊢
+    have ⟨x, hx⟩ := hy
+    have ⟨z, hz⟩ := hg.right.right hx.left
+    simp only [Set.mem_Iio] at hz
+    exact ⟨z, hz.left, hz.right ▸ hx.right⟩
+  have hA₃ : ∀ y, y ∈ f '' A → ∃ q, q ∈ A_y y ∧ ∀ p ∈ A_y y, q ≤ p := by
     sorry
-  have hA₂ : ∀ y ∈ B, Set.Nonempty (A_y y) := by
-    sorry
-  have hA₃ : ∀ y ∈ B, ∃ q : ℕ, ∀ p ∈ A_y y, q ≤ p := by
-    sorry
-
-  let C := { q | ∃ y ∈ B, ∀ p ∈ A_y y, q ≤ p }
+/-
+> Define `C = {q_y | y ∈ ran f}`.
+-/
+  let C := { q | ∃ y, y ∈ f '' A ∧ (∀ p ∈ A_y y, q ≤ p) }
+/-
+> Thus `h : C → ran f` given by `h(x) = f(g(x))` is a one-to-on ecorrespondence
+> between `C` and `ran f` by construction. That is, `C ≈ ran f`.
+-/
   let h x := f (g x)
   have hh : C ≈ f '' A := by
     sorry
-
+/-
+> By *Lemma 6F*, there exists some `n ≤ m` such that `C ≈ n`. By *Theorem 6A*,
+> `n ≈ ran f`.
+-/
   sorry
 
 /-- ### Set Difference Size