Enderton. Formally verify theorem 3G.

Bookshelf/Enderton/Set.tex

@@ -3194,7 +3194,7 @@ For any one-to-one function $F$, $F^{-1}$ is also one-to-one.
 
 \end{proof}
 
-\subsection{\partial{Theorem 3G}}%
+\subsection{\verified{Theorem 3G}}%
 \label{sub:theorem-3g}
 
 \begin{theorem}[3G]
@@ -3207,6 +3207,14 @@ For any one-to-one function $F$, $F^{-1}$ is also one-to-one.
 
 \begin{proof}
 
+  \statementpadding
+
+  \lean*{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.theorem\_3g\_i}
+
+  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.theorem\_3g\_ii}
+
   Suppose $F$ is a one-to-one \nameref{ref:function}.
   Then \nameref{sub:lemma-1} indicates $F^{-1}$ is a one-to-one function with
     domain $\ran{F}$ and range $\dom{F}$.

Bookshelf/Enderton/Set/Chapter_3.lean

@@ -436,18 +436,28 @@ theorem exercise_6_9_ii {A : Set (Set.Relation α)}
 
 Assume that `F` is a one-to-one function. If `x ∈ dom F`, then `F⁻¹(F(x)) = x`.
 -/
-theorem theorem_3g_i {F : Set.Relation α}
+theorem theorem_3g_i {α : Type _} {x y : α} {F : Set.Relation α}
-  (hF : Set.Relation.isOneToOne F) (hx : x ∈ F.dom)
+  (hF : Set.Relation.isOneToOne F) (hx : x ∈ Set.Relation.dom F)
   : ∃! y, (x, y) ∈ F ∧ (y, x) ∈ F.inv := by
-  sorry
+  simp only [Set.Relation.mem_self_comm_mem_inv, and_self]
+  have ⟨y, hy⟩ := Set.Relation.dom_exists hx
+  refine ⟨y, hy, ?_⟩
+  intro y₁ hy₁
+  unfold Set.Relation.isOneToOne at hF
+  exact (Set.Relation.single_valued_eq_unique hF.left hy hy₁).symm
 
 /-- ### Theorem 3G (ii)
 
 Assume that `F` is a one-to-one function. If `y ∈ ran F`, then `F(F⁻¹(y)) = y`.
 -/
 theorem theorem_3g_ii {F : Set.Relation α}
-  (hF : Set.Relation.isOneToOne F) (hy : x ∈ F.ran)
+  (hF : Set.Relation.isOneToOne F) (hy : y ∈ F.ran)
   : ∃! x, (x, y) ∈ F ∧ (y, x) ∈ F.inv := by
-  sorry
+  simp only [Set.Relation.mem_self_comm_mem_inv, and_self]
+  have ⟨x, hx⟩ := Set.Relation.ran_exists hy
+  refine ⟨x, hx, ?_⟩
+  intro x₁ hx₁
+  unfold Set.Relation.isOneToOne at hF
+  exact (Set.Relation.single_rooted_eq_unique hF.right hx hx₁).symm
 
 end Enderton.Set.Chapter_3

Common/Set/Relation.lean

@@ -43,7 +43,7 @@ theorem mem_pair_imp_fst_mem_dom {R : Relation α} (h : (x, y) ∈ R)
 If `x ∈ dom R`, there exists some `y` such that `⟨x, y⟩ ∈ R`.
 -/
 theorem dom_exists {R : Relation α} (hx : x ∈ R.dom)
-  : ∃ y, (x, y) ∈ R := by
+  : ∃ y : α, (x, y) ∈ R := by
   unfold dom at hx
   simp only [mem_image, Prod.exists, exists_and_right, exists_eq_right] at hx
   exact hx
@@ -63,7 +63,7 @@ theorem mem_pair_imp_snd_mem_ran {R : Relation α} (h : (x, y) ∈ R)
 If `x ∈ ran R`, there exists some `t` such that `⟨t, x⟩ ∈ R`.
 -/
 theorem ran_exists {R : Relation α} (hx : x ∈ R.ran)
-  : ∃ t, (t, x) ∈ R := by
+  : ∃ t : α, (t, x) ∈ R := by
   unfold ran at hx
   simp only [mem_image, Prod.exists, exists_eq_right] at hx
   exact hx
@@ -192,6 +192,21 @@ exists exactly one `x` such that `⟨x, y⟩ ∈ R`.
 def isSingleRooted (R : Relation α) : Prop :=
   ∀ y ∈ R.ran, ∃! x, x ∈ R.dom ∧ (x, y) ∈ R
 
+/--
+A single-rooted `Relation` should map the same output to the same input.
+-/
+theorem single_rooted_eq_unique {R : Relation α} {x₁ x₂ y : α}
+  (hR : isSingleRooted R)
+  : (x₁, y) ∈ R → (x₂, y) ∈ R → x₁ = x₂ := by
+  intro hx₁ hx₂
+  unfold isSingleRooted at hR
+  have := hR y (mem_pair_imp_snd_mem_ran hx₁)
+  have ⟨y₁, hy₁⟩ := this
+  simp only [and_imp] at hy₁
+  have h₁ := hy₁.right x₁ (mem_pair_imp_fst_mem_dom hx₁) hx₁
+  have h₂ := hy₁.right x₂ (mem_pair_imp_fst_mem_dom hx₂) hx₂
+  rw [h₁, h₂]
+
 /--
 A `Relation` `R` is said to be single-valued **iff** for all `x ∈ dom R`, there
 exists exactly one `y` such that `⟨x, y⟩ ∈ R`.
@@ -201,6 +216,21 @@ Notice, a `Relation` that is single-valued is a function.
 def isSingleValued (R : Relation α) : Prop :=
   ∀ x ∈ R.dom, ∃! y, y ∈ R.ran ∧ (x, y) ∈ R
 
+/--
+A single-valued `Relation` should map the same input to the same output.
+-/
+theorem single_valued_eq_unique {R : Relation α} {x y₁ y₂ : α}
+  (hR : isSingleValued R)
+  : (x, y₁) ∈ R → (x, y₂) ∈ R → y₁ = y₂ := by
+  intro hy₁ hy₂
+  unfold isSingleValued at hR
+  have := hR x (mem_pair_imp_fst_mem_dom hy₁)
+  have ⟨x₁, hx₁⟩ := this
+  simp only [and_imp] at hx₁
+  have h₁ := hx₁.right y₁ (mem_pair_imp_snd_mem_ran hy₁) hy₁
+  have h₂ := hx₁.right y₂ (mem_pair_imp_snd_mem_ran hy₂) hy₂
+  rw [h₁, h₂]
+
 /--
 For a set `F`, `F⁻¹` is a function **iff** `F` is single-rooted.
 -/