bookshelf/Bookshelf/Enderton/Set/Chapter_3.lean

import Bookshelf.Enderton.Set.Chapter_2
import Bookshelf.Enderton.Set.OrderedPair
import Bookshelf.Enderton.Set.Relation
import Common.Logic.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Data.Rel
import Mathlib.Init.Algebra.Classes
import Mathlib.Order.RelClasses
import Mathlib.Tactic.CasesM

/-! # Enderton.Set.Chapter_3

Relations and Functions
-/

namespace Enderton.Set.Chapter_3

open Set.Relation

/-- ### Lemma 3B

If `x ∈ C` and `y ∈ C`, then `⟨x, y⟩ ∈ 𝒫 𝒫 C`.
-/
lemma lemma_3b {C : Set α} (hx : x ∈ C) (hy : y ∈ C)
  : OrderedPair x y ∈ 𝒫 𝒫 C := by
/-
> Let `C` be an arbitrary set and `x, y ∈ C`. Then by definition of the power
> set, `{x}` and `{x, y}` are members of `𝒫 C`.
-/
  have hxs : {x} ⊆ C := Set.singleton_subset_iff.mpr hx
  have hxys : {x, y} ⊆ C := Set.mem_mem_imp_pair_subset hx hy
/-
> Likewise `{{x}, {x, y}}` is a member of `𝒫 𝒫 C`. By definition of an ordered
> pair, `⟨x, y⟩ = {{x}, {x, y}}`. This concludes our proof.
-/
  exact Set.mem_mem_imp_pair_subset hxs hxys

/-- ### Theorem 3D

If `⟨x, y⟩ ∈ A`, then `x` and `y` belong to `⋃ ⋃ A`.
-/
theorem theorem_3d {A : Set (Set (Set α))} (h : OrderedPair x y ∈ A)
  : x ∈ ⋃₀ (⋃₀ A) ∧ y ∈ ⋃₀ (⋃₀ A) := by
/-
> Let `A` be a set and `⟨x, y⟩ ∈ A`. By definition of an ordered pair,
>
> `⟨x, y⟩ = {{x}, {x, y}}`.
>
> By Exercise 2.3, `{{x}, {x, y}} ⊆ ∪ A`. Then `{x, y} ∈ ∪ A`.
-/
  have hp := Chapter_2.exercise_2_3 (OrderedPair x y) h
  unfold OrderedPair at hp
  have hq : {x, y} ∈ ⋃₀ A := hp (by simp)
/-
> Another application of Exercise 2.3 implies `{x, y} ∈ ∪ ∪ A`.
-/
  have : {x, y} ⊆ ⋃₀ ⋃₀ A := Chapter_2.exercise_2_3 {x, y} hq
/-
> Therefore `x, y ∈ ∪ ∪ A`.
-/
  exact ⟨this (by simp), this (by simp)⟩


/-- ### Theorem 3G (i)

Assume that `F` is a one-to-one function. If `x ∈ dom F`, then `F⁻¹(F(x)) = x`.
-/
theorem theorem_3g_i {F : Set.HRelation α β}
  (hF : isOneToOne F) (hx : x ∈ dom F)
  : ∃! y, (x, y) ∈ F ∧ (y, x) ∈ inv F := by
  simp only [mem_self_comm_mem_inv, and_self]
  have ⟨y, hy⟩ := dom_exists hx
  refine ⟨y, hy, ?_⟩
  intro y₁ hy₁
  unfold isOneToOne at hF
  exact (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.HRelation α β}
  (hF : isOneToOne F) (hy : y ∈ ran F)
  : ∃! x, (x, y) ∈ F ∧ (y, x) ∈ inv F := by
  simp only [mem_self_comm_mem_inv, and_self]
  have ⟨x, hx⟩ := ran_exists hy
  refine ⟨x, hx, ?_⟩
  intro x₁ hx₁
  unfold isOneToOne at hF
  exact (single_rooted_eq_unique hF.right hx hx₁).symm

/-- ### Theorem 3H

Assume that `F` and `G` are functions. Then
```
dom (F ∘ G) = {x ∈ dom G | G(x) ∈ dom F}.
```
-/
theorem theorem_3h_dom {F : Set.HRelation β γ} {G : Set.HRelation α β}
  (_ : isSingleValued F) (hG : isSingleValued G)
  : dom (comp F G) = {x ∈ dom G | ∃! y, (x, y) ∈ G ∧ y ∈ dom F} := by
  let rhs := {x ∈ dom G | ∃! y, (x, y) ∈ G ∧ y ∈ dom F }
  rw [Set.Subset.antisymm_iff]
  apply And.intro
  · show ∀ t, t ∈ dom (comp F G) → t ∈ rhs
    intro t ht
    simp only [Set.mem_setOf_eq]
    have ⟨z, hz⟩ := dom_exists ht
    refine ⟨dom_comp_imp_dom_self ht, ?_⟩
    have ⟨a, ha⟩ := hz
    unfold dom
    simp only [Set.mem_image, Prod.exists, exists_and_right, exists_eq_right]
    unfold ExistsUnique
    simp only [and_imp, forall_exists_index]
    refine ⟨a, ⟨ha.left, z, ha.right⟩, ?_⟩
    intro y₁ hy₁
    exact fun _ _ => single_valued_eq_unique hG hy₁ ha.left
  · show ∀ t, t ∈ rhs → t ∈ dom (comp F G)
    intro t ht
    simp only [Set.mem_setOf_eq] at ht
    unfold dom
    simp only [Set.mem_image, Prod.exists, exists_and_right, exists_eq_right]
    have ⟨a, ha⟩ := ht.right
    simp at ha
    have ⟨b, hb⟩ := dom_exists ha.left.right
    refine ⟨b, ?_⟩
    unfold comp
    simp only [Set.mem_setOf_eq]
    exact ⟨a, ha.left.left, hb⟩

/-- ### Theorem 3J (a)

Assume that `F : A → B`, and that `A` is nonempty. There exists a function
`G : B → A` (a "left inverse") such that `G ∘ F` is the identity function on `A`
**iff** `F` is one-to-one.
-/
theorem theorem_3j_a {F : Set.HRelation α β}
  (hF : mapsInto F A B) (hA : Set.Nonempty A)
  : isOneToOne F ↔
      ∃ G, mapsInto G B A ∧ comp G F = { p | p.1 ∈ A ∧ p.1 = p.2 } := by
  apply Iff.intro
  · intro h
    have ⟨a, ha⟩ := hA
    -- `G(y) = if y ∈ ran F then F⁻¹(y) else a`
    let G : Set.HRelation β α :=
      restriction (inv F) B ∪ { p | p.1 ∈ B ∧ p.1 ∉ ran F ∧ p.2 = a }

    refine ⟨G, ⟨?_, ?_, ?_⟩, ?_⟩
    · show isSingleValued G
      intro x hx
      have ⟨y, hy⟩ := dom_exists hx
      refine ⟨y, ⟨mem_pair_imp_snd_mem_ran hy, hy⟩, ?_⟩
      intro y₁ hy₁
      dsimp only at hy₁
      apply Or.elim hy₁.right
      · -- Supposes `y₁ ∈ ran F`.
        intro hF_inv
        unfold restriction at hF_inv
        simp only [Prod.exists, Set.mem_setOf_eq, Prod.mk.injEq] at hF_inv
        dsimp only at hy
        unfold restriction at hy
        simp only [Set.mem_union, Set.mem_setOf_eq] at hy
        apply Or.elim hy
        · intro ⟨hz, _⟩
          have : isOneToOne (inv F) := one_to_one_self_iff_one_to_one_inv.mp h
          exact single_valued_eq_unique this.left hF_inv.left hz
        · intro hz
          rw [hz.right.right]
          simp only [mem_self_comm_mem_inv] at hF_inv
          have := mem_pair_imp_snd_mem_ran hF_inv.left
          exact absurd this hz.right.left
      · -- Supposes `y₁ ∉ ran F`.
        intro hF_id
        simp at hF_id
        dsimp only at hy
        unfold restriction at hy
        simp at hy
        apply Or.elim hy
        · intro hz
          have := mem_pair_imp_snd_mem_ran hz.left
          exact absurd this hF_id.right.left
        · intro hz
          rw [hF_id.right.right, hz.right.right]

    · show dom G = B
      ext b
      unfold dom Prod.fst Set.image
      simp only [
        Set.mem_union,
        Set.mem_setOf_eq,
        Prod.exists,
        exists_and_right,
        exists_eq_right
      ]
      apply Iff.intro
      · intro ⟨x, hx⟩
        apply Or.elim hx (fun hb => hb.right) (fun hb => hb.left)
      · intro hb
        by_cases hb' : b ∈ ran F
        · have ⟨t, ht⟩ := ran_exists hb'
          refine ⟨t, ?_⟩
          left
          unfold restriction inv
          simp only [Prod.exists, Set.mem_setOf_eq, Prod.mk.injEq]
          exact ⟨⟨t, b, ht, rfl, rfl⟩, hb⟩
        · refine ⟨a, ?_⟩
          right
          exact ⟨hb, hb', rfl⟩

    · show ∀ t, t ∈ ran G → t ∈ A  -- `ran G ⊆ A`
      intro t ht
      dsimp only at ht
      unfold ran Prod.snd restriction inv at ht
      simp only [
        Prod.exists,
        Set.mem_setOf_eq,
        Set.mem_image,
        exists_eq_right,
        not_exists,
        Set.mem_union,
        Prod.mk.injEq
      ] at ht
      have ⟨a₁, ha₁⟩ := ht
      apply Or.elim ha₁
      · intro ⟨⟨a, b, hab⟩, _⟩
        have := mem_pair_imp_fst_mem_dom hab.left
        rwa [← hab.right.right, ← hF.dom_eq]
      · intro h
        rwa [h.right.right]

    · -- Show that `G ∘ F` is the identity function on `A`.
      show comp G F = {p | p.fst ∈ A ∧ p.fst = p.snd}
      unfold comp
      ext p
      have (x, y) := p
      simp only [Set.mem_union, Set.mem_setOf_eq]
      apply Iff.intro
      · intro ⟨t, hx, ht⟩
        refine ⟨hF.dom_eq ▸ mem_pair_imp_fst_mem_dom hx, ?_⟩
        apply Or.elim ht
        · intro ht'
          unfold restriction inv at ht'
          simp at ht'
          have ⟨c, d, hcd⟩ := ht'.left
          rw [hcd.right.left, hcd.right.right] at hcd
          exact single_rooted_eq_unique h.right hx hcd.left
        · intro ht'
          exact absurd (mem_pair_imp_snd_mem_ran hx) ht'.right.left
      · intro hx
        rw [← hF.dom_eq] at hx
        have ⟨t, ht⟩ := dom_exists hx.left
        refine ⟨t, ht, ?_⟩
        left
        unfold restriction
        simp only [Set.mem_setOf_eq, mem_self_comm_mem_inv]
        rw [← hx.right]
        exact ⟨ht, hF.ran_ss (mem_pair_imp_snd_mem_ran ht)⟩

  · intro ⟨G, hG₁, hG₂⟩
    refine ⟨hF.is_func, ?_⟩
    unfold isSingleRooted
    intro y hy
    have ⟨x₁, hx₁⟩ := ran_exists hy
    refine ⟨x₁, ⟨mem_pair_imp_fst_mem_dom hx₁, hx₁⟩, ?_⟩
    intro x₂ hx₂
    have hc_x₁ : (x₁, x₁) ∈ comp G F := by
      rw [hG₂]
      simp only [Set.mem_setOf_eq, and_true]
      rw [← hF.dom_eq]
      exact mem_pair_imp_fst_mem_dom hx₁
    have hc_x₂ : (x₂, x₂) ∈ comp G F := by
      rw [hG₂]
      simp only [Set.mem_setOf_eq, and_true]
      rw [← hF.dom_eq]
      exact hx₂.left
    unfold comp at hc_x₁ hc_x₂
    have ⟨t₁, ht₁⟩ := hc_x₁
    have ⟨t₂, ht₂⟩ := hc_x₂
    simp only at ht₁ ht₂
    rw [← single_valued_eq_unique hF.is_func hx₁ ht₁.left] at ht₁
    rw [← single_valued_eq_unique hF.is_func hx₂.right ht₂.left] at ht₂
    exact single_valued_eq_unique hG₁.is_func ht₂.right ht₁.right

/-- ### Theorem 3J (b)

Assume that `F : A → B`, and that `A` is nonempty. There exists a function
`H : B → A` (a "right inverse") such that `F ∘ H` is the identity function on
`B` only if `F` maps `A` onto `B`.
-/
theorem theorem_3j_b {F : Set.HRelation α β} (hF : mapsInto F A B)
  : (∃ H, mapsInto H B A ∧ comp F H = { p | p.1 ∈ B ∧ p.1 = p.2 }) →
      mapsOnto F A B := by
  intro ⟨H, _, hH₂⟩
  refine ⟨hF.is_func, hF.dom_eq, Set.Subset.antisymm hF.ran_ss ?_⟩
  show ∀ y, y ∈ B → y ∈ ran F
  intro y hy
  suffices y ∈ ran (comp F H) from ran_comp_imp_ran_self this
  rw [hH₂]
  unfold ran Prod.snd Set.image
  simp only [Set.mem_setOf_eq, Prod.exists, exists_eq_right, Set.setOf_mem_eq]
  exact hy

/-- ### Theorem 3K (a)

The following hold for any sets. (`F` need not be a function.)
The image of a union is the union of the images:
```
F⟦⋃ 𝓐⟧ = ⋃ {F⟦A⟧ | A ∈ 𝓐}
```
-/
theorem theorem_3k_a {F : Set.HRelation α β} {𝓐 : Set (Set α)}
  : image F (⋃₀ 𝓐) = ⋃₀ { image F A | A ∈ 𝓐 } := by
  rw [Set.Subset.antisymm_iff]
  apply And.intro
  · show ∀ v, v ∈ image F (⋃₀ 𝓐) → v ∈ ⋃₀ { image F A | A ∈ 𝓐 }
    intro v hv
    unfold image at hv
    simp only [Set.mem_sUnion, Set.mem_setOf_eq] at hv
    have ⟨u, hu⟩ := hv
    have ⟨A, hA⟩ := hu.left
    simp only [Set.mem_sUnion, Set.mem_setOf_eq, exists_exists_and_eq_and]
    refine ⟨A, hA.left, ?_⟩
    show v ∈ image F A
    unfold image
    simp only [Set.mem_setOf_eq]
    exact ⟨u, hA.right, hu.right⟩
  · show ∀ v, v ∈ ⋃₀ {x | ∃ A, A ∈ 𝓐 ∧ image F A = x} → v ∈ image F (⋃₀ 𝓐)
    intro v hv
    simp only [Set.mem_sUnion, Set.mem_setOf_eq, exists_exists_and_eq_and] at hv
    have ⟨A, hA⟩ := hv
    unfold image at hA
    simp only [Set.mem_setOf_eq] at hA
    have ⟨u, hu⟩ := hA.right
    unfold image
    simp only [Set.mem_sUnion, Set.mem_setOf_eq]
    exact ⟨u, ⟨A, hA.left, hu.left⟩, hu.right⟩

/-! ### Theorem 3K (b)

The following hold for any sets. (`F` need not be a function.)
The image of an intersection is included in the intersection of the images:
```
F⟦⋂ 𝓐⟧ ⊆ ⋂ {F⟦A⟧ | A ∈ 𝓐}
```
Equality holds if `F` is single-rooted.
-/

theorem theorem_3k_b_i {F : Set.HRelation α β} {𝓐 : Set (Set α)}
  : image F (⋂₀ 𝓐) ⊆ ⋂₀ { image F A | A ∈ 𝓐} := by
  show ∀ v, v ∈ image F (⋂₀ 𝓐) → v ∈ ⋂₀ { image F A | A ∈ 𝓐}
  intro v hv
  unfold image at hv
  simp only [Set.mem_sInter, Set.mem_setOf_eq] at hv
  have ⟨u, hu⟩ := hv
  simp only [
    Set.mem_sInter,
    Set.mem_setOf_eq,
    forall_exists_index,
    and_imp,
    forall_apply_eq_imp_iff₂
  ]
  intro A hA
  unfold image
  simp only [Set.mem_setOf_eq]
  exact ⟨u, hu.left A hA, hu.right⟩

theorem theorem_3k_b_ii {F : Set.HRelation α β} {𝓐 : Set (Set α)}
  (hF : isSingleRooted F) (h𝓐 : Set.Nonempty 𝓐)
  : image F (⋂₀ 𝓐) = ⋂₀ { image F A | A ∈ 𝓐} := by
  rw [Set.Subset.antisymm_iff]
  refine ⟨theorem_3k_b_i, ?_⟩
  show ∀ v, v ∈ ⋂₀ {x | ∃ A, A ∈ 𝓐 ∧ image F A = x} → v ∈ image F (⋂₀ 𝓐)
  intro v hv
  simp only [
    Set.mem_sInter,
    Set.mem_setOf_eq,
    forall_exists_index,
    and_imp,
    forall_apply_eq_imp_iff₂
  ] at hv
  unfold image at hv
  simp only [Set.mem_setOf_eq] at hv
  have ⟨u, hu⟩ : ∃ u, (∀ (a : Set α), a ∈ 𝓐 → u ∈ a) ∧ (u, v) ∈ F := by
    have ⟨A, hA⟩ := h𝓐
    have ⟨_, ⟨_, hv'⟩⟩ := hv A hA
    have ⟨u, hu⟩ := hF v (mem_pair_imp_snd_mem_ran hv')
    simp only [and_imp] at hu
    refine ⟨u, ?_, hu.left.right⟩
    intro a ha
    have ⟨u₁, hu₁⟩ := hv a ha
    have := hu.right u₁ (mem_pair_imp_fst_mem_dom hu₁.right) hu₁.right
    rw [← this]
    exact hu₁.left
  unfold image
  simp only [Set.mem_sInter, Set.mem_setOf_eq]
  exact ⟨u, hu⟩

/-! ### Theorem 3K (c)

The following hold for any sets. (`F` need not be a function.)
The image of a difference includes the difference of the images:
```
F⟦A⟧ - F⟦B⟧ ⊆ F⟦A - B⟧.
```
Equality holds if `F` is single-rooted.
-/

theorem theorem_3k_c_i {F : Set.HRelation α β} {A B : Set α}
  : image F A \ image F B ⊆ image F (A \ B) := by
  show ∀ v, v ∈ image F A \ image F B → v ∈ image F (A \ B)
  intro v hv
  have hv' : v ∈ image F A ∧ v ∉ image F B := hv
  conv at hv' => arg 1; unfold image; simp only [Set.mem_setOf_eq, eq_iff_iff]
  have ⟨u, hu⟩ := hv'.left
  have hw : ∀ w ∈ B, (w, v) ∉ F := by
    intro w hw nw
    have nv := hv'.right
    unfold image at nv
    simp only [Set.mem_setOf_eq, not_exists, not_and] at nv
    exact absurd nw (nv w hw)
  have hu' : u ∉ B := by
    by_contra nu
    exact absurd hu.right (hw u nu)
  unfold image
  simp only [Set.mem_diff, Set.mem_setOf_eq]
  exact ⟨u, ⟨hu.left, hu'⟩, hu.right⟩

theorem theorem_3k_c_ii {F : Set.HRelation α β} {A B : Set α}
  (hF : isSingleRooted F)
  : image F A \ image F B = image F (A \ B) := by
  rw [Set.Subset.antisymm_iff]
  refine ⟨theorem_3k_c_i, ?_⟩
  show ∀ v, v ∈ image F (A \ B) → v ∈ image F A \ image F B
  intro v hv
  unfold image at hv
  simp only [Set.mem_diff, Set.mem_setOf_eq] at hv
  have ⟨u, hu⟩ := hv
  have hv₁ : v ∈ image F A := by
    unfold image
    simp only [Set.mem_setOf_eq]
    exact ⟨u, hu.left.left, hu.right⟩
  have hv₂ : v ∉ image F B := by
    intro nv
    unfold image at nv
    simp only [Set.mem_setOf_eq] at nv
    have ⟨u₁, hu₁⟩ := nv
    have := single_rooted_eq_unique hF hu.right hu₁.right
    rw [← this] at hu₁
    exact absurd hu₁.left hu.left.right
  exact ⟨hv₁, hv₂⟩

/-! ### Corollary 3L

For any function `G` and sets `A`, `B`, and `𝓐`:

```
G⁻¹⟦⋃ 𝓐⟧ = ⋃ {G⁻¹⟦A⟧ | A ∈ 𝓐},
G⁻¹⟦𝓐⟧ = ⋂ {G⁻¹⟦A⟧ | A ∈ 𝓐} for 𝓐 ≠ ∅,
G⁻¹⟦A - B⟧ = G⁻¹⟦A⟧ - G⁻¹⟦B⟧.
```
-/

theorem corollary_3l_i {G : Set.HRelation β α} {𝓐 : Set (Set α)}
  : image (inv G) (⋃₀ 𝓐) = ⋃₀ {image (inv G) A | A ∈ 𝓐} := theorem_3k_a

theorem corollary_3l_ii {G : Set.HRelation β α} {𝓐 : Set (Set α)}
  (hG : isSingleValued G) (h𝓐 : Set.Nonempty 𝓐)
  : image (inv G) (⋂₀ 𝓐) = ⋂₀ {image (inv G) A | A ∈ 𝓐} := by
  have hG' : isSingleRooted (inv G) :=
    single_valued_self_iff_single_rooted_inv.mp hG
  exact theorem_3k_b_ii hG' h𝓐

theorem corollary_3l_iii {G : Set.HRelation β α} {A B : Set α}
  (hG : isSingleValued G)
  : image (inv G) (A \ B) = image (inv G) A \ image (inv G) B := by
  have hG' : isSingleRooted (inv G) :=
    single_valued_self_iff_single_rooted_inv.mp hG
  exact (theorem_3k_c_ii hG').symm

/-- ### Theorem 3M

If `R` is a symmetric and transitive relation, then `R` is an equivalence
relation on `fld R`.
-/
theorem theorem_3m {R : Set.Relation α}
  (hS : R.isSymmetric) (hT : R.isTransitive)
  : R.isEquivalence (fld R) := by
  refine ⟨Eq.subset rfl, ?_, hS, hT⟩
  intro x hx
  apply Or.elim hx
  · intro h
    have ⟨y, hy⟩ := dom_exists h
    have := hS hy
    exact hT hy this
  · intro h
    have ⟨t, ht⟩ := ran_exists h
    have := hS ht
    exact hT this ht

/-- ### Theorem 3R

Let `R` be a linear ordering on `A`.

(i) There is no `x` for which `xRx`.
(ii) For distinct `x` and `y` in `A`, either `xRy` or `yRx`.
-/
theorem theorem_3r {R : Rel α α} (hR : IsStrictTotalOrder α R)
  : (∀ x : α, ¬ R x x) ∧ (∀ x y : α, x ≠ y → R x y ∨ R y x) := by
  apply And.intro
  · exact hR.irrefl
  · intro x y h
    apply Or.elim (hR.trichotomous x y)
    · intro h₁
      left
      exact h₁
    · intro h₁
      apply Or.elim h₁
      · intro h₂
        exact absurd h₂ h
      · intro h₂
        right
        exact h₂

/-- ### Exercise 3.1

Suppose that we attempted to generalize the Kuratowski definitions of ordered
pairs to ordered triples by defining
```
⟨x, y, z⟩* = {{x}, {x, y}, {x, y, z}}.open Set

```
Show that this definition is unsuccessful by giving examples of objects `u`,
`v`, `w`, `x`, `y`, `z` with `⟨x, y, z⟩* = ⟨u, v, w⟩*` but with either `y ≠ v`
or `z ≠ w` (or both).
-/
theorem exercise_3_1 {x y z u v w : ℕ}
  (hx : x = 1) (hy : y = 1) (hz : z = 2)
  (hu : u = 1) (hv : v = 2) (hw : w = 2)
  : ({{x}, {x, y}, {x, y, z}} : Set (Set ℕ)) = {{u}, {u, v}, {u, v, w}}
  ∧ y ≠ v := by
  apply And.intro
  · rw [hx, hy, hz, hu, hv, hw]
    simp
  · rw [hy, hv]
    simp only

/-- ### Exercise 3.2a

Show that `A × (B ∪ C) = (A × B) ∪ (A × C)`.
-/
theorem exercise_3_2a {A : Set α} {B C : Set β}
  : Set.prod A (B ∪ C) = (Set.prod A B) ∪ (Set.prod A C) := by
  calc Set.prod A (B ∪ C)
    _ = { p | p.1 ∈ A ∧ p.2 ∈ B ∪ C } := rfl
    _ = { p | p.1 ∈ A ∧ (p.2 ∈ B ∨ p.2 ∈ C) } := rfl
    _ = { p | (p.1 ∈ A ∧ p.2 ∈ B) ∨ (p.1 ∈ A ∧ p.2 ∈ C) } := by
      ext x
      rw [Set.mem_setOf_eq]
      conv => lhs; rw [and_or_left]
    _ = { p | p ∈ Set.prod A B ∨ (p ∈ Set.prod A C) } := rfl
    _ = (Set.prod A B) ∪ (Set.prod A C) := rfl

/-- ### Exercise 3.2b

Show that if `A × B = A × C` and `A ≠ ∅`, then `B = C`.
-/
theorem exercise_3_2b {A : Set α} {B C : Set β}
  (h : Set.prod A B = Set.prod A C) (hA : Set.Nonempty A)
  : B = C := by
  by_cases hB : Set.Nonempty B
  · rw [Set.Subset.antisymm_iff]
    have ⟨a, ha⟩ := hA
    apply And.intro
    · show ∀ t, t ∈ B → t ∈ C
      intro t ht
      have : (a, t) ∈ Set.prod A B := ⟨ha, ht⟩
      rw [h] at this
      exact this.right
    · show ∀ t, t ∈ C → t ∈ B
      intro t ht
      have : (a, t) ∈ Set.prod A C := ⟨ha, ht⟩
      rw [← h] at this
      exact this.right
  · have nB : B = ∅ := Set.not_nonempty_iff_eq_empty.mp hB
    rw [nB, Set.prod_right_emptyset_eq_emptyset, Set.ext_iff] at h
    rw [nB]
    by_contra nC
    have ⟨a, ha⟩ := hA
    have ⟨c, hc⟩ := Set.nonempty_iff_ne_empty.mpr (Ne.symm nC)
    exact (h (a, c)).mpr ⟨ha, hc⟩

/-- ### Exercise 3.3

Show that `A × ⋃ 𝓑 = ⋃ {A × X | X ∈ 𝓑}`.
-/
theorem exercise_3_3 {A : Set (Set α)} {𝓑 : Set (Set β)}
  : Set.prod A (⋃₀ 𝓑) = ⋃₀ {Set.prod A X | X ∈ 𝓑} := by
  calc Set.prod A (⋃₀ 𝓑)
    _ = { p | p.1 ∈ A ∧ p.2 ∈ ⋃₀ 𝓑} := rfl
    _ = { p | p.1 ∈ A ∧ ∃ b ∈ 𝓑, p.2 ∈ b } := rfl
    _ = { p | ∃ b ∈ 𝓑, p.1 ∈ A ∧ p.2 ∈ b } := by
      ext x
      rw [Set.mem_setOf_eq]
      apply Iff.intro
      · intro ⟨h₁, b, h₂⟩
        exact ⟨b, h₂.left, h₁, h₂.right⟩
      · intro ⟨b, h₁, h₂, h₃⟩
        exact ⟨h₂, b, h₁, h₃⟩
    _ = ⋃₀ { Set.prod A p | p ∈ 𝓑 } := by
      ext x
      rw [Set.mem_setOf_eq]
      unfold Set.sUnion sSup Set.instSupSetSet
      simp only [Set.mem_setOf_eq, exists_exists_and_eq_and]
      apply Iff.intro
      · intro ⟨b, h₁, h₂, h₃⟩
        exact ⟨b, h₁, h₂, h₃⟩
      · intro ⟨b, h₁, h₂, h₃⟩
        exact ⟨b, h₁, h₂, h₃⟩

/-- ### Exercise 3.5a

Assume that `A` and `B` are given sets, and show that there exists a set `C`
such that for any `y`,
```
y ∈ C ↔ y = {x} × B for some x in A.
```
In other words, show that `{{x} × B | x ∈ A}` is a set.
-/
theorem exercise_3_5a {A : Set α} {B : Set β}
  : ∃ C : Set (Set (α × β)),
      y ∈ C ↔ ∃ x ∈ A, y = Set.prod {x} B := by
  let C := {y ∈ 𝒫 (Set.prod A B) | ∃ a ∈ A, ∀ x, (x ∈ y ↔ ∃ b ∈ B, x = (a, b))}
  refine ⟨C, ?_⟩
  apply Iff.intro
  · intro hC
    simp only [Set.mem_setOf_eq] at hC
    have ⟨_, ⟨a, ⟨ha, h⟩⟩⟩ := hC
    refine ⟨a, ⟨ha, ?_⟩⟩
    ext x
    apply Iff.intro
    · intro hxy
      unfold Set.prod
      simp only [Set.mem_singleton_iff, Set.mem_setOf_eq]
      have ⟨b, ⟨hb, hx⟩⟩ := (h x).mp hxy
      rw [Prod.ext_iff] at hx
      simp only at hx
      rw [← hx.right] at hb
      exact ⟨hx.left, hb⟩
    · intro hx
      simp only [Set.mem_singleton_iff, Set.mem_setOf_eq] at hx
      have := (h (a, x.snd)).mpr ⟨x.snd, ⟨hx.right, rfl⟩⟩
      have hxab : x = (a, x.snd) := by
        ext <;> simp
        exact hx.left
      rwa [← hxab] at this
  · intro ⟨x, ⟨hx, hy⟩⟩
    show y ∈ 𝒫 Set.prod A B ∧ ∃ a, a ∈ A ∧
           ∀ (x : α × β), x ∈ y ↔ ∃ b, b ∈ B ∧ x = (a, b)
    apply And.intro
    · simp only [Set.mem_powerset_iff]
      rw [hy]
      unfold Set.prod
      simp only [
        Set.mem_singleton_iff,
        Set.setOf_subset_setOf,
        and_imp,
        Prod.forall
      ]
      intro a b ha hb
      exact ⟨by rw [ha]; exact hx, hb⟩
    · refine ⟨x, ⟨hx, ?_⟩⟩
      intro p
      apply Iff.intro
      · intro hab
        rw [hy] at hab
        unfold Set.prod at hab
        simp only [Set.mem_singleton_iff, Set.mem_setOf_eq] at hab
        exact ⟨p.2, ⟨hab.right, by ext; exact hab.left; simp⟩⟩
      · intro ⟨b, ⟨hb, hab⟩⟩
        rw [hy]
        unfold Set.prod
        simp only [Set.mem_singleton_iff, Set.mem_setOf_eq]
        rw [Prod.ext_iff] at hab
        simp only at hab
        rw [hab.right]
        exact ⟨hab.left, hb⟩

/-- ### Exercise 3.5b

With `A`, `B`, and `C` as above, show that `A × B = ∪ C`.
-/
theorem exercise_3_5b {A : Set α} (B : Set β)
  : Set.prod A B = ⋃₀ {Set.prod ({x} : Set α) B | x ∈ A} := by
  rw [Set.Subset.antisymm_iff]
  apply And.intro
  · show ∀ t, t ∈ Set.prod A B → t ∈ ⋃₀ {Set.prod {x} B | x ∈ A}
    intro t h
    unfold Set.sUnion sSup Set.instSupSetSet
    simp only [Set.mem_setOf_eq, exists_exists_and_eq_and]
    unfold Set.prod at h
    simp only [Set.mem_setOf_eq] at h
    refine ⟨t.fst, ⟨h.left, ?_⟩⟩
    unfold Set.prod
    simp only [Set.mem_singleton_iff, Set.mem_setOf_eq, true_and]
    exact h.right
  · show ∀ t, t ∈ ⋃₀ {Set.prod {x} B | x ∈ A} → t ∈ Set.prod A B
    unfold Set.prod
    intro t ht
    simp only [
      Set.mem_singleton_iff,
      Set.mem_sUnion,
      Set.mem_setOf_eq,
      exists_exists_and_eq_and
    ] at ht
    have ⟨a, ⟨h, ⟨ha, hb⟩⟩⟩ := ht
    simp only [Set.mem_setOf_eq]
    rw [← ha] at h
    exact ⟨h, hb⟩


/-- ### Exercise 3.6

Show that a set `A` is a relation **iff** `A ⊆ dom A × ran A`.
-/
theorem exercise_3_6 {A : Set.HRelation α β}
  : A ⊆ Set.prod (dom A) (ran A) := by
  show ∀ t, t ∈ A → t ∈ Set.prod (Prod.fst '' A) (Prod.snd '' A)
  intro (a, b) ht
  unfold Set.prod
  simp only [
    Set.mem_image,
    Prod.exists,
    exists_and_right,
    exists_eq_right,
    Set.mem_setOf_eq
  ]
  exact ⟨⟨b, ht⟩, ⟨a, ht⟩⟩

/-- ### Exercise 3.7

Show that if `R` is a relation, then `fld R = ⋃ ⋃ R`.
-/
theorem exercise_3_7 {R : Set.Relation α}
  : R.fld = ⋃₀ ⋃₀ R.toOrderedPairs := by
  let img := R.toOrderedPairs
  rw [Set.Subset.antisymm_iff]
  apply And.intro
  · show ∀ x, x ∈ R.fld → x ∈ ⋃₀ ⋃₀ img
    intro x hx
    apply Or.elim hx
    · intro hd
      unfold Set.Relation.dom Prod.fst at hd
      simp only [
        Set.mem_image, Prod.exists, exists_and_right, exists_eq_right
      ] at hd
      have ⟨y, hp⟩ := hd
      have hm : OrderedPair x y ∈ Set.image (fun p => OrderedPair p.1 p.2) R := by
        unfold Set.image
        simp only [Prod.exists, Set.mem_setOf_eq]
        exact ⟨x, ⟨y, ⟨hp, rfl⟩⟩⟩
      unfold OrderedPair at hm
      have : {x} ∈ ⋃₀ img := Chapter_2.exercise_2_3 {{x}, {x, y}} hm (by simp)
      exact (Chapter_2.exercise_2_3 {x} this) (show x ∈ {x} by rfl)
    · intro hr
      unfold Set.Relation.ran Prod.snd at hr
      simp only [Set.mem_image, Prod.exists, exists_eq_right] at hr
      have ⟨t, ht⟩ := hr
      have hm : OrderedPair t x ∈ Set.image (fun p => OrderedPair p.1 p.2) R := by
        simp only [Set.mem_image, Prod.exists]
        exact ⟨t, ⟨x, ⟨ht, rfl⟩⟩⟩
      unfold OrderedPair at hm
      have : {t, x} ∈ ⋃₀ img := Chapter_2.exercise_2_3 {{t}, {t, x}} hm
        (show {t, x} ∈ {{t}, {t, x}} by simp)
      exact Chapter_2.exercise_2_3 {t, x} this (show x ∈ {t, x} by simp)

  · show ∀ t, t ∈ ⋃₀ ⋃₀ img → t ∈ Set.Relation.fld R
    intro t ht
    have ⟨T, hT⟩ : ∃ T ∈ ⋃₀ img, t ∈ T := ht
    have ⟨T', hT'⟩ : ∃ T' ∈ img, T ∈ T' := hT.left
    dsimp only at hT'
    unfold Set.Relation.toOrderedPairs at hT'
    simp only [Set.mem_image, Prod.exists] at hT'
    have ⟨x, ⟨y, ⟨p, hp⟩⟩⟩ := hT'.left
    have hr := hT'.right
    rw [← hp] at hr
    unfold OrderedPair at hr
    simp only [Set.mem_singleton_iff, Set.mem_insert_iff] at hr

    -- Use `exercise_6_6` to prove that if `t = x` then `t ∈ dom R` and if
    -- `t = y` then `t ∈ ran R`.
    have hxy_mem : t = x ∨ t = y → t ∈ Set.Relation.fld R := by
      intro ht
      have hz : R ⊆ Set.prod (dom R) (ran R) := exercise_3_6
      have : (x, y) ∈ Set.prod (dom R) (ran R) := hz p
      unfold Set.prod at this
      simp at this
      apply Or.elim ht
      · intro ht'
        rw [← ht'] at this
        exact Or.inl this.left
      · intro ht'
        rw [← ht'] at this
        exact Or.inr this.right

    -- Eliminate `T = {x} ∨ T = {x, y}`.
    apply Or.elim hr
    · intro hx
      have := hT.right
      rw [hx] at this
      simp only [Set.mem_singleton_iff] at this
      exact hxy_mem (Or.inl this)
    · intro hxy
      have := hT.right
      rw [hxy] at this
      simp only [Set.mem_singleton_iff, Set.mem_insert_iff] at this
      exact hxy_mem this

/-- ### Exercise 3.8 (i)

Show that for any set `𝓐`:
```
dom ⋃ A = ⋃ { dom R | R ∈ 𝓐 }
```
-/
theorem exercise_3_8_i {A : Set (Set.HRelation α β)}
  : dom (⋃₀ A) = ⋃₀ { dom R | R ∈ A } := by
  ext x
  unfold dom Prod.fst
  simp only [
    Set.mem_image,
    Set.mem_sUnion,
    Prod.exists,
    exists_and_right,
    exists_eq_right,
    Set.mem_setOf_eq,
    exists_exists_and_eq_and
  ]
  apply Iff.intro
  · intro ⟨y, t, ht, hx⟩
    exact ⟨t, ht, y, hx⟩
  · intro ⟨t, ht, y, hx⟩
    exact ⟨y, t, ht, hx⟩

/-- ### Exercise 3.8 (ii)

Show that for any set `𝓐`:
```
ran ⋃ A = ⋃ { ran R | R ∈ 𝓐 }
```
-/
theorem exercise_3_8_ii {A : Set (Set.HRelation α β)}
  : ran (⋃₀ A) = ⋃₀ { ran R | R ∈ A } := by
  ext x
  unfold ran Prod.snd
  simp only [
    Set.mem_image,
    Set.mem_sUnion,
    Prod.exists,
    exists_eq_right,
    Set.mem_setOf_eq,
    exists_exists_and_eq_and
  ]
  apply Iff.intro
  · intro ⟨t, ⟨y, ⟨hy, ht⟩⟩⟩
    exact ⟨y, ⟨hy, ⟨t, ht⟩⟩⟩
  · intro ⟨y, ⟨hy, ⟨t, ht⟩⟩⟩
    exact ⟨t, ⟨y, ⟨hy, ht⟩⟩⟩

/-- ### Exercise 3.9 (i)

Discuss the result of replacing the union operation by the intersection
operation in the preceding problem.
```
dom ⋃ A = ⋃ { dom R | R ∈ 𝓐 }
```
-/
theorem exercise_3_9_i {A : Set (Set.HRelation α β)}
  : dom (⋂₀ A) ⊆ ⋂₀ { dom R | R ∈ A } := by
  show ∀ x, x ∈ dom (⋂₀ A) → x ∈ ⋂₀ { dom R | R ∈ A }
  unfold dom Prod.fst
  simp only [
    Set.mem_image,
    Set.mem_sInter,
    Prod.exists,
    exists_and_right,
    exists_eq_right,
    Set.mem_setOf_eq,
    forall_exists_index,
    and_imp,
    forall_apply_eq_imp_iff₂
  ]
  intro _ y hy R hR
  exact ⟨y, hy R hR⟩

/-- ### Exercise 3.9 (ii)

Discuss the result of replacing the union operation by the intersection
operation in the preceding problem.
```
ran ⋃ A = ⋃ { ran R | R ∈ 𝓐 }
```
-/
theorem exercise_3_9_ii {A : Set (Set.HRelation α β)}
  : ran (⋂₀ A) ⊆ ⋂₀ { ran R | R ∈ A } := by
  show ∀ x, x ∈ ran (⋂₀ A) → x ∈ ⋂₀ { ran R | R ∈ A }
  unfold ran Prod.snd
  simp only [
    Set.mem_image,
    Set.mem_sInter,
    Prod.exists,
    exists_and_right,
    exists_eq_right,
    Set.mem_setOf_eq,
    forall_exists_index,
    and_imp,
    forall_apply_eq_imp_iff₂
  ]
  intro _ y hy R hR
  exact ⟨y, hy R hR⟩

/-- ### Exercise 3.12

Assume that `f` and `g` are functions and show that
```
f ⊆ g ↔ dom f ⊆ dom g ∧ (∀ x ∈ dom f) f(x) = g(x).
```
-/
theorem exercise_3_12 {f g : Set.HRelation α β}
  (hf : isSingleValued f) (_ : isSingleValued g)
  : f ⊆ g ↔ dom f ⊆ dom g ∧
      (∀ x ∈ dom f, ∃! y : β, (x, y) ∈ f ∧ (x, y) ∈ g) := by
  apply Iff.intro
  · intro h
    apply And.intro
    · show ∀ x, x ∈ dom f → x ∈ dom g
      intro x hx
      have ⟨y, hy⟩ := dom_exists hx
      exact mem_pair_imp_fst_mem_dom (h hy)
    · intro x hx
      have ⟨y, hy⟩ := dom_exists hx
      refine ⟨y, ⟨hy, h hy⟩, ?_⟩
      intro y₁ hy₁
      exact single_valued_eq_unique hf hy₁.left hy
  · intro ⟨_, hx⟩
    show ∀ p, p ∈ f → p ∈ g
    intro (x, y) hp
    have ⟨y₁, hy₁⟩ := hx x (mem_pair_imp_fst_mem_dom hp)
    rw [single_valued_eq_unique hf hp hy₁.left.left]
    exact hy₁.left.right

/-- ### Exercise 3.13

Assume that `f` and `g` are functions with `f ⊆ g` and `dom g ⊆ dom f`. Show
that `f = g`.
-/
theorem exercise_3_13 {f g : Set.HRelation α β}
  (hf : isSingleValued f) (hg : isSingleValued g)
  (h : f ⊆ g) (h₁ : dom g ⊆ dom f)
  : f = g := by
  have h₂ := (exercise_3_12 hf hg).mp h
  have hfg := Set.Subset.antisymm_iff.mpr ⟨h₁, h₂.left⟩
  ext p
  have (a, b) := p
  apply Iff.intro
  · intro hp
    have ⟨x, hx⟩ := h₂.right a (mem_pair_imp_fst_mem_dom hp)
    rw [single_valued_eq_unique hf hp hx.left.left]
    exact hx.left.right
  · intro hp
    rw [← hfg] at h₂
    have ⟨x, hx⟩ := h₂.right a (mem_pair_imp_fst_mem_dom hp)
    rw [single_valued_eq_unique hg hp hx.left.right]
    exact hx.left.left

/-- ### Exercise 3.14 (a)

Assume that `f` and `g` are functions. Show that `f ∩ g` is a function.
-/
theorem exercise_3_14_a {f g : Set.HRelation α β}
  (hf : isSingleValued f) (_ : isSingleValued g)
  : isSingleValued (f ∩ g) :=
  single_valued_subset hf (Set.inter_subset_left f g)

/-- ### Exercise 3.14 (b)

Assume that `f` and `g` are functions. Show that `f ∪ g` is a function **iff**
`f(x) = g(x)` for every `x` in `(dom f) ∩ (dom g)`.
-/
theorem exercise_3_14_b {f g : Set.HRelation α β}
  (hf : isSingleValued f) (hg : isSingleValued g)
  : isSingleValued (f ∪ g) ↔
      (∀ x ∈ dom f ∩ dom g, ∃! y, (x, y) ∈ f ∧ (x, y) ∈ g) := by
  apply Iff.intro
  · intro h x hx
    have ⟨y₁, hy₁⟩ := hf x hx.left
    have ⟨y₂, hy₂⟩ := hg x hx.right
    have : y₁ = y₂ := single_valued_eq_unique h
      (Or.inl hy₁.left.right)
      (Or.inr hy₂.left.right)
    rw [← this] at hy₂
    refine ⟨y₁, ⟨hy₁.left.right, hy₂.left.right⟩, ?_⟩
    intro y₃ hfy₃
    exact single_valued_eq_unique hf hfy₃.left hy₁.left.right
  · intro h x hx
    by_cases hfx : x ∈ dom f <;>
    by_cases hgx : x ∈ dom g
    · -- `x ∈ dom f ∧ x ∈ dom g`
      have ⟨y₁, hy₁⟩ := hf x hfx
      have ⟨y₂, hy₂⟩ := hg x hgx
      refine ⟨y₁, ⟨?_, Or.inl hy₁.left.right⟩, ?_⟩
      · unfold ran
        simp only [Set.mem_image, Set.mem_union, Prod.exists, exists_eq_right]
        exact ⟨x, Or.inl hy₁.left.right⟩
      · intro y₃ hy₃
        apply Or.elim hy₃.right
        · intro hxy
          exact single_valued_eq_unique hf hxy hy₁.left.right
        · refine fun hxy => single_valued_eq_unique hg hxy ?_
          have : y₁ = y₂ := by
            have ⟨z, ⟨hz, _⟩⟩ := h x ⟨hfx, hgx⟩
            rw [
              single_valued_eq_unique hf hy₁.left.right hz.left,
              single_valued_eq_unique hg hy₂.left.right hz.right
            ]
          rw [this]
          exact hy₂.left.right
    · -- `x ∈ dom f ∧ x ∉ dom g`
      have ⟨y, hy⟩ := dom_exists hfx
      have hxy : (x, y) ∈ f ∪ g := (Set.subset_union_left f g) hy
      refine ⟨y, ⟨mem_pair_imp_snd_mem_ran hxy, hxy⟩, ?_⟩
      intro y₁ hy₁
      apply Or.elim hy₁.right
      · intro hx'
        exact single_valued_eq_unique hf hx' hy
      · intro hx'
        exact absurd (mem_pair_imp_fst_mem_dom hx') hgx
    · -- `x ∉ dom f ∧ x ∈ dom g`
      have ⟨y, hy⟩ := dom_exists hgx
      have hxy : (x, y) ∈ f ∪ g := (Set.subset_union_right f g) hy
      refine ⟨y, ⟨mem_pair_imp_snd_mem_ran hxy, hxy⟩, ?_⟩
      intro y₁ hy₁
      apply Or.elim hy₁.right
      · intro hx'
        exact absurd (mem_pair_imp_fst_mem_dom hx') hfx
      · intro hx'
        exact single_valued_eq_unique hg hx' hy
    · -- `x ∉ dom f ∧ x ∉ dom g`
      exfalso
      unfold dom at hx
      simp only [
        Set.mem_image,
        Set.mem_union,
        Prod.exists,
        exists_and_right,
        exists_eq_right
      ] at hx
      have ⟨_, hy⟩ := hx
      apply Or.elim hy
      · intro hz
        exact absurd (mem_pair_imp_fst_mem_dom hz) hfx
      · intro hz
        exact absurd (mem_pair_imp_fst_mem_dom hz) hgx

/-- ### Exercise 3.15

Let `𝓐` be a set of functions such that for any `f` and `g` in `𝓐`, either
`f ⊆ g` or `g ⊆ f`. Show that `⋃ 𝓐` is a function.
-/
theorem exercise_3_15 {𝓐 : Set (Set.HRelation α β)}
  (h𝓐 : ∀ F ∈ 𝓐, isSingleValued F)
  (h : ∀ F, ∀ G, F ∈ 𝓐 → G ∈ 𝓐 → F ⊆ G ∨ G ⊆ F)
  : isSingleValued (⋃₀ 𝓐) := by
  intro x hx
  have ⟨y₁, hy₁⟩ := dom_exists hx
  refine ⟨y₁, ⟨mem_pair_imp_snd_mem_ran hy₁, hy₁⟩, ?_⟩
  intro y₂ hy₂
  have ⟨f, hf⟩ : ∃ f : Set.HRelation α β, f ∈ 𝓐 ∧ (x, y₁) ∈ f := hy₁
  have ⟨g, hg⟩ : ∃ g : Set.HRelation α β, g ∈ 𝓐 ∧ (x, y₂) ∈ g := hy₂.right
  apply Or.elim (h f g hf.left hg.left)
  · intro hf'
    have := hf' hf.right
    exact single_valued_eq_unique (h𝓐 g hg.left) hg.right this
  · intro hg'
    have := hg' hg.right
    exact single_valued_eq_unique (h𝓐 f hf.left) this hf.right

/-! ### Exercise 3.17

Show that the composition of two single-rooted sets is again single-rooted.
Conclude that the composition of two one-to-one functions is again one-to-one.
-/

theorem exercise_3_17_i {F : Set.HRelation β γ} {G : Set.HRelation α β}
  (hF : isSingleRooted F) (hG : isSingleRooted G)
  : isSingleRooted (comp F G):= by
  intro v hv

  have ⟨u₁, hu₁⟩ := ran_exists hv
  have hu₁' := hu₁
  unfold comp at hu₁'
  simp only [Set.mem_setOf_eq] at hu₁'
  have ⟨t₁, ht₁⟩ := hu₁'
  unfold ExistsUnique
  refine ⟨u₁, ⟨mem_pair_imp_fst_mem_dom hu₁, hu₁⟩, ?_⟩

  intro u₂ hu₂
  have hu₂' := hu₂
  unfold comp at hu₂'
  simp only [Set.mem_setOf_eq] at hu₂'
  have ⟨_, ⟨t₂, ht₂⟩⟩ := hu₂'

  have ht : t₁ = t₂ := single_rooted_eq_unique hF ht₁.right ht₂.right
  rw [ht] at ht₁
  exact single_rooted_eq_unique hG ht₂.left ht₁.left

theorem exercise_3_17_ii {F : Set.HRelation β γ} {G : Set.HRelation α β}
  (hF : isOneToOne F) (hG : isOneToOne G)
  : isOneToOne (comp F G) := And.intro
      (single_valued_comp_is_single_valued hF.left hG.left)
      (exercise_3_17_i hF.right hG.right)

/-! ### Exercise 3.18

Let `R` be the set
```
{⟨0, 1⟩, ⟨0, 2⟩, ⟨0, 3⟩, ⟨1, 2⟩, ⟨1, 3⟩, ⟨2, 3⟩}
```
Evaluate the following: `R ∘ R`, `R ↾ {1}`, `R⁻¹ ↾ {1}`, `R⟦{1}⟧`, and
`R⁻¹⟦{1}⟧`.
-/

section Exercise_3_18

variable {R : Set.Relation ℕ}
variable (hR : R = {(0, 1), (0, 2), (0, 3), (1, 2), (1, 3), (2, 3)})

theorem exercise_3_18_i
  : comp R R = {(0, 2), (0, 3), (1, 3)} := by
  rw [hR]
  unfold comp
  simp only [Set.mem_singleton_iff, Set.mem_insert_iff, or_self, Prod.mk.injEq]
  ext x
  have (a, b) := x
  apply Iff.intro
  · simp only [Set.mem_setOf_eq, Set.mem_singleton_iff, Set.mem_insert_iff]
    intro ⟨t, ht₁, ht₂⟩
    casesm* _ ∨ _
    all_goals case _ hl hr => first
      | {rw [hl.right] at hr; simp at hr}
      | {rw [hl.left] at hr; simp at hr}
      | {rw [hl.left, hr.right]; simp}
  · simp only [
      Set.mem_singleton_iff,
      Set.mem_insert_iff,
      Prod.mk.injEq,
      Set.mem_setOf_eq
    ]
    intro h
    casesm* _ ∨ _
    · case _ h =>
        refine ⟨1, Or.inl ⟨h.left, rfl⟩, ?_⟩
        iterate 3 right
        left
        exact ⟨rfl, h.right⟩
    · case _ h =>
        refine ⟨1, Or.inl ⟨h.left, rfl⟩, ?_⟩
        iterate 4 right
        left
        exact ⟨rfl, h.right⟩
    · case _ h =>
        refine ⟨2, ?_, ?_⟩
        · iterate 3 right
          left
          exact ⟨h.left, rfl⟩
        · iterate 5 right
          exact ⟨rfl, h.right⟩

theorem exercise_3_18_ii
  : restriction R {1} = {(1, 2), (1, 3)} := by
  rw [hR]
  unfold restriction
  ext p
  have (a, b) := p
  simp only [
    Set.mem_singleton_iff,
    Set.mem_insert_iff,
    Set.mem_setOf_eq,
    or_self
  ]
  apply Iff.intro
  · intro ⟨hp, ha⟩
    rw [ha]
    simp only [Prod.mk.injEq, true_and]
    casesm* _ ∨ _
    all_goals case _ h => first
      | {rw [ha] at h; simp at h}
      | {simp only [Prod.mk.injEq] at h; left; exact h.right}
      | {simp only [Prod.mk.injEq] at h; right; exact h.right}
  · intro h
    apply Or.elim h
    · intro hab
      simp only [Prod.mk.injEq] at hab
      refine ⟨?_, hab.left⟩
      iterate 3 right
      left
      rw [hab.left, hab.right]
    · intro hab
      simp only [Prod.mk.injEq] at hab
      refine ⟨?_, hab.left⟩
      iterate 4 right
      left
      rw [hab.left, hab.right]

theorem exercise_3_18_iii
  : restriction (inv R) {1} = {(1, 0)} := by
  rw [hR]
  unfold inv restriction
  ext p
  have (a, b) := p
  simp only [
    Set.mem_singleton_iff,
    Set.mem_insert_iff,
    or_self,
    exists_eq_or_imp,
    exists_eq_left,
    Set.mem_setOf_eq,
    Prod.mk.injEq
  ]
  apply Iff.intro
  · intro ⟨hb, ha⟩
    casesm* _ ∨ _
    all_goals case _ hr => first
      | exact ⟨ha, hr.right.symm⟩
      | rw [ha] at hr; simp at hr
  · intro ⟨ha, hb⟩
    rw [ha, hb]
    simp

theorem exercise_3_18_iv
  : image R {1} = {2, 3} := by
  rw [hR]
  unfold image
  ext y
  simp

theorem exercise_3_18_v
  : image (inv R) {1} = {0} := by
  rw [hR]
  unfold inv image
  ext y
  simp

end Exercise_3_18

/-! ### Exercise 3.19

Let
```
A = {⟨∅, {∅, {∅}}⟩, ⟨{∅}, ∅⟩}.
```
Evaluate each of the following: `A(∅)`, `A⟦∅⟧`, `A⟦{∅}⟧`, `A⟦{∅, {∅}}⟧`,
`A⁻¹`, `A ∘ A`, `A ↾ ∅`, `A ↾ {∅, {∅}}`, `⋃ ⋃ A`.
-/

section Exercise_3_19

variable {A : Set.Relation (Set (Set (Set α)))}
variable (hA : A = {(∅, {∅, {∅}}), ({∅}, ∅)})

theorem exercise_3_19_i
  : (∅, {∅, {∅}}) ∈ A := by
  rw [hA]
  simp

theorem exercise_3_19_ii
  : image A ∅ = ∅ := by
  unfold image
  simp

theorem exercise_3_19_iii
  : image A {∅} = {{∅, {∅}}} := by
  unfold image
  rw [hA]
  ext x
  simp only [
    Set.mem_singleton_iff,
    Prod.mk.injEq,
    Set.mem_insert_iff,
    exists_eq_left,
    true_and
  ]
  apply Iff.intro
  · intro hx
    simp at hx
    apply Or.elim hx
    · simp
    · intro ⟨h, _⟩
      exfalso
      rw [Set.ext_iff] at h
      have := h ∅
      simp at this
  · intro hx
    rw [hx]
    simp

theorem exercise_3_19_iv
  : image A {∅, {∅}} = {{∅, {∅}}, ∅} := by
  unfold image
  rw [hA]
  ext x
  simp only [
    Set.mem_singleton_iff,
    Set.mem_insert_iff,
    Prod.mk.injEq,
    exists_eq_or_imp,
    true_and,
    exists_eq_left,
    Set.singleton_ne_empty,
    false_and,
    false_or,
    Set.mem_setOf_eq
  ]
  apply Iff.intro
  · intro h
    apply Or.elim h
    · intro hx₁
      apply Or.elim hx₁
      · intro hx₂; left ; exact hx₂
      · intro hx₂; right; exact hx₂.right
    · intro hx₂
      right
      exact hx₂
  · intro h
    apply Or.elim h
    · intro hx₁; iterate 2 left
      exact hx₁
    · intro hx₁; right; exact hx₁

theorem exercise_3_19_v
  : inv A = {({∅, {∅}}, ∅), (∅, {∅})} := by
  unfold inv
  rw [hA]
  ext x
  simp only [
    Set.mem_singleton_iff,
    Prod.mk.injEq,
    Set.mem_insert_iff,
    exists_eq_or_imp,
    exists_eq_left,
    Set.mem_setOf_eq
  ]
  apply Iff.intro
  · intro hx
    apply Or.elim hx
    · intro hx₁; left ; rw [← hx₁]
    · intro hx₁; right; rw [← hx₁]
  · intro hx
    apply Or.elim hx
    · intro hx₁; left ; rw [← hx₁]
    · intro hx₁; right; rw [← hx₁]

theorem exercise_3_19_vi
  : comp A A = {({∅}, {∅, {∅}})} := by
  unfold comp
  rw [hA]
  ext x
  have (a, b) := x
  simp only [
    Set.mem_singleton_iff, Prod.mk.injEq, Set.mem_insert_iff, Set.mem_setOf_eq
  ]
  apply Iff.intro
  · intro ⟨t, ht₁, ht₂⟩
    casesm* _ ∨ _
    all_goals case _ hl hr => first
      | {
          rw [hl.right] at hr
          have := hr.left
          rw [Set.ext_iff] at this
          simp at this
        }
      | exact ⟨hl.left, hr.right⟩
  · intro ⟨ha, hb⟩
    refine ⟨∅, ?_, ?_⟩
    · right; rw [ha]; simp
    · left ; rw [hb]; simp

theorem exercise_3_19_vii
  : restriction A ∅ = ∅ := by
  unfold restriction
  rw [hA]
  simp

theorem exercise_3_19_viii
  : restriction A {∅} = {(∅, {∅, {∅}})} := by
  unfold restriction
  rw [hA]
  ext x
  have (a, b) := x
  simp only [
    Set.mem_singleton_iff, Prod.mk.injEq, Set.mem_insert_iff, Set.mem_setOf_eq
  ]
  apply Iff.intro
  · intro ⟨h, ha⟩
    apply Or.elim h
    · simp
    · intro ⟨ha', _⟩
      exfalso
      rw [ha', Set.ext_iff] at ha
      simp at ha
  · intro ⟨ha, hb⟩
    rw [ha, hb]
    simp

theorem exercise_3_19_ix
  : restriction A {∅, {∅}} = A := by
  unfold restriction
  rw [hA]
  ext x
  have (a, b) := x
  simp only [
    Set.mem_singleton_iff,
    Prod.mk.injEq,
    Set.mem_insert_iff,
    Set.mem_setOf_eq
  ]
  apply Iff.intro
  · intro ⟨h₁, h₂⟩
    casesm* _ ∨ _
    · case _ hl _ => left ; exact hl
    · case _ hl _ => left ; exact hl
    · case _ hl _ => right; exact hl
    · case _ hl _ => right; exact hl
  · intro h₁
    apply Or.elim h₁ <;>
    · intro ⟨ha, hb⟩
      rw [ha, hb]
      simp

theorem exercise_3_19_x
  : ⋃₀ ⋃₀ A.toOrderedPairs = {∅, {∅}, {∅, {∅}}} := by
  unfold toOrderedPairs OrderedPair Set.sUnion sSup Set.instSupSetSet
  rw [hA]
  ext x
  simp only [
    Set.mem_singleton_iff,
    Prod.mk.injEq,
    Set.mem_image,
    Set.mem_insert_iff,
    exists_eq_or_imp,
    exists_eq_left,
    Set.singleton_ne_empty,
    Set.mem_setOf_eq
  ]
  apply Iff.intro
  · intro ⟨a, ⟨t, ht₁, ht₂⟩, hx⟩
    apply Or.elim ht₁
    · intro ht
      rw [← ht] at ht₂
      simp only [Set.mem_singleton_iff, Set.mem_insert_iff] at ht₂
      apply Or.elim ht₂
      · intro ha
        rw [ha] at hx
        simp only [Set.mem_singleton_iff] at hx
        left
        exact hx
      · intro ha
        rw [ha] at hx
        simp at hx
        apply Or.elim hx <;>
        · intro hx'; rw [hx']; simp
    · intro ht
      rw [← ht] at ht₂
      simp only [
        Set.mem_singleton_iff, Set.singleton_ne_empty, Set.mem_insert_iff
      ] at ht₂
      apply Or.elim ht₂
      · intro ha
        rw [ha] at hx
        simp only [Set.mem_singleton_iff] at hx
        rw [hx]
        simp
      · intro ha
        rw [ha] at hx
        simp only [
          Set.mem_singleton_iff, Set.singleton_ne_empty, Set.mem_insert_iff
        ] at hx
        apply Or.elim hx <;>
        · intro hx'; rw [hx']; simp
  · intro hx
    apply Or.elim hx
    · intro hx₁
      rw [hx₁]
      refine ⟨{{∅}, ∅}, ⟨{{{∅}}, {{∅}, ∅}}, ?_⟩, ?_⟩ <;> simp
    · intro hx₁
      apply Or.elim hx₁
      · intro hx₂
        rw [hx₂]
        refine ⟨{{∅}, ∅}, ⟨{{{∅}}, {{∅}, ∅}}, ?_⟩, ?_⟩ <;> simp
      · intro hx₂
        rw [hx₂]
        refine ⟨{∅, {∅, {∅}}}, ⟨{{∅}, {∅, {∅, {∅}}}}, ?_⟩, ?_⟩ <;> simp

end Exercise_3_19

/-- ### Exercise 3.20

Show that `F ↾ A = F ∩ (A × ran F)`.
-/
theorem exercise_3_20 {F : Set.HRelation α β} {A : Set α}
  : restriction F A = F ∩ (Set.prod A (ran F)) := by
  calc restriction F A
    _ = {p | p ∈ F ∧ p.fst ∈ A} := rfl
    _ = {p | p ∈ F ∧ p.fst ∈ A ∧ p.snd ∈ ran F} := by
      ext x
      have (a, b) := x
      simp only [
        Set.mem_setOf_eq, Set.sep_and, Set.mem_inter_iff, iff_self_and, and_imp
      ]
      intro hF _
      exact ⟨hF, mem_pair_imp_snd_mem_ran hF⟩
    _ = {p | p ∈ F} ∩ {p | p.fst ∈ A ∧ p.snd ∈ ran F} := rfl
    _ = F ∩ {p | p.fst ∈ A ∧ p.snd ∈ ran F} := rfl
    _ = F ∩ (Set.prod A (ran F)) := rfl

/-- ### Exercise 3.22 (a)

Show that the following is correct for any sets.
```
A ⊆ B → F⟦A⟧ ⊆ F⟦B⟧
```
-/
theorem exercise_3_22_a {A B : Set α} {F : Set.HRelation α β} (h : A ⊆ B)
  : image F A ⊆ image F B := by
  show ∀ x, x ∈ image F A → x ∈ image F B
  intro x hx
  have ⟨u, hu⟩ := hx
  have := h hu.left
  exact ⟨u, this, hu.right⟩

/-- ### Exercise 3.22 (b)

Show that the following is correct for any sets.
```
(F ∘ G)⟦A⟧ = F⟦G⟦A⟧⟧
```
-/
theorem exercise_3_22_b {A B : Set α} {F : Set.HRelation α β}
  : image (comp F G) A = image F (image G A) := by
  calc image (comp F G) A
    _ = { v | ∃ u ∈ A, (u, v) ∈ comp F G } := rfl
    _ = { v | ∃ u ∈ A, ∃ a, (u, a) ∈ G ∧ (a, v) ∈ F } := rfl
    _ = { v | ∃ a, ∃ u ∈ A, (u, a) ∈ G ∧ (a, v) ∈ F } := by
      ext p
      apply Iff.intro
      · intro ⟨u, hu, a, ha⟩
        exact ⟨a, u, hu, ha⟩
      · intro ⟨a, u, hu, ha⟩
        exact ⟨u, hu, a, ha⟩
    _ = { v | ∃ a, (∃ u ∈ A, (u, a) ∈ G) ∧ (a, v) ∈ F } := by
      ext p
      apply Iff.intro
      · intro ⟨a, u, h⟩
        exact ⟨a, ⟨u, h.left, h.right.left⟩, h.right.right⟩
      · intro ⟨a, ⟨u, hu⟩, ha⟩
        exact ⟨a, u, hu.left, hu.right, ha⟩
    _ = { v | ∃ a ∈ { w | ∃ u ∈ A, (u, w) ∈ G }, (a, v) ∈ F } := rfl
    _ = { v | ∃ a ∈ image G A, (a, v) ∈ F } := rfl
    _ = image F (image G A) := rfl

/-- ### Exercise 3.22 (c)

Show that the following is correct for any sets.
```
Q ↾ (A ∪ B) = (Q ↾ A) ∪ (Q ↾ B)
```
-/
theorem exercise_3_22_c {A B : Set α} {Q : Set.Relation α}
  : restriction Q (A ∪ B) = (restriction Q A) ∪ (restriction Q B) := by
  calc restriction Q (A ∪ B)
    _ = { p | p ∈ Q ∧ p.1 ∈ A ∪ B } := rfl
    _ = { p | p ∈ Q ∧ (p.1 ∈ A ∨ p.1 ∈ B) } := rfl
    _ = { p | (p ∈ Q ∧ p.1 ∈ A) ∨ (p ∈ Q ∧ p.1 ∈ B) } := by
      ext p
      simp only [Set.sep_or, Set.mem_union, Set.mem_setOf_eq]
    _ = { p | p ∈ Q ∧ p.1 ∈ A} ∪ { p | p ∈ Q ∧ p.1 ∈ B } := rfl
    _ = (restriction Q A) ∪ (restriction Q B) := rfl

/-- ### Exercise 3.23 (i)

Let `I` be the identity function on the set `A`. Show that for any sets `B` and
`C`, `B ∘ I = B ↾ A`.
-/
theorem exercise_3_23_i {A : Set α} {B : Set.HRelation α β} {I : Set.Relation α}
  (hI : I = { p | p.1 ∈ A ∧ p.1 = p.2 })
  : comp B I = restriction B A := by
  rw [Set.Subset.antisymm_iff]
  apply And.intro
  · show ∀ p, p ∈ comp B I → p ∈ restriction B A
    intro (x, y) hp
    have ⟨t, ht⟩ := hp
    rw [hI] at ht
    simp only [Set.mem_setOf_eq] at ht
    show (x, y) ∈ B ∧ x ∈ A
    rw [← ht.left.right] at ht
    exact ⟨ht.right, ht.left.left⟩
  · show ∀ p, p ∈ restriction B A → p ∈ comp B I
    unfold restriction comp
    rw [hI]
    intro (x, y) hp
    refine ⟨x, ⟨hp.right, rfl⟩, hp.left⟩

/-- ### Exercise 3.23 (ii)

Let `I` be the identity function on the set `A`. Show that for any sets `B` and
`C`, `I⟦C⟧ = A ∩ C`.
-/
theorem exercise_3_23_ii {A C : Set α} {I : Set.Relation α}
  (hI : I = { p | p.1 ∈ A ∧ p.1 = p.2 })
  : image I C = A ∩ C := by
  calc image I C
    _ = { v | ∃ u ∈ C, (u, v) ∈ I } := rfl
    _ = { v | ∃ u ∈ C, u ∈ A ∧ u = v } := by
      ext v
      apply Iff.intro
      · intro ⟨u, h₁, h₂⟩
        rw [hI] at h₂
        exact ⟨u, h₁, h₂⟩
      · intro ⟨u, h₁, h₂⟩
        refine ⟨u, h₁, ?_⟩
        · rw [hI]
          exact h₂
    _ = { v | v ∈ C ∧ v ∈ A } := by
      ext v
      simp only [Set.mem_setOf_eq, Set.sep_mem_eq, Set.mem_inter_iff]
      apply Iff.intro
      · intro ⟨u, hC, hA, hv⟩
        rw [← hv]
        exact ⟨hC, hA⟩
      · intro ⟨hC, hA⟩
        exact ⟨v, hC, hA, rfl⟩
    _ = C ∩ A := rfl
    _ = A ∩ C := Set.inter_comm C A

/-- ### Exercise 3.24

Show that for a function `F`, `F⁻¹⟦A⟧ = { x ∈ dom F | F(x) ∈ A }`.
-/
theorem exercise_3_24 {F : Set.HRelation α β} {A : Set β}
  (hF : isSingleValued F)
  : image (inv F) A = { x ∈ dom F | ∃! y : β, (x, y) ∈ F ∧ y ∈ A } := by
  calc image (inv F) A
    _ = { x | ∃ y ∈ A, (y, x) ∈ inv F } := rfl
    _ = { x | ∃ y ∈ A, (x, y) ∈ F } := by simp only [mem_self_comm_mem_inv]
    _ = { x | x ∈ dom F ∧ (∃ y : β, (x, y) ∈ F ∧ y ∈ A) } := by
      ext x
      apply Iff.intro
      · intro ⟨y, hy, hyx⟩
        exact ⟨mem_pair_imp_fst_mem_dom hyx, y, hyx, hy⟩
      · intro ⟨_, y, hxy, hy⟩
        exact ⟨y, hy, hxy⟩
    _ = { x ∈ dom F | ∃ y : β, (x, y) ∈ F ∧ y ∈ A } := rfl
    _ = { x ∈ dom F | ∃! y : β, (x, y) ∈ F ∧ y ∈ A } := by
      ext x
      simp only [Set.mem_setOf_eq, and_congr_right_iff]
      intro _
      apply Iff.intro
      · intro ⟨y, hy⟩
        refine ⟨y, hy, ?_⟩
        intro y₁ hy₁
        exact single_valued_eq_unique hF hy₁.left hy.left
      · intro ⟨y, hy⟩
        exact ⟨y, hy.left⟩

/-- ### Exercise 3.25 (b)

Show that the result of part (a) holds for any function `G`, not necessarily
one-to-one.
-/
theorem exercise_3_25_b {G : Set.HRelation α β} (hG : isSingleValued G)
  : comp G (inv G) = { p | p.1 ∈ ran G ∧ p.1 = p.2 } := by
  ext p
  have (x, y) := p
  apply Iff.intro
  · unfold comp inv
    intro h
    simp only [Prod.exists, Set.mem_setOf_eq, Prod.mk.injEq] at h
    have ⟨t, ⟨a, b, ⟨hab, hb, ha⟩⟩, ht⟩ := h
    rw [hb, ha] at hab
    exact ⟨mem_pair_imp_snd_mem_ran hab, single_valued_eq_unique hG hab ht⟩
  · intro h
    simp only [Set.mem_setOf_eq] at h
    unfold comp inv
    simp only [Prod.exists, Set.mem_setOf_eq, Prod.mk.injEq]
    have ⟨t, ht⟩ := ran_exists h.left
    exact ⟨t, ⟨t, x, ht, rfl, rfl⟩, by rwa [← h.right]⟩

/-- ### Exercise 3.25 (a)

Assume that `G` is a one-to-one function. Show that `G ∘ G⁻¹` is the identity
function on `ran G`.
-/
theorem exercise_3_25_a {G : Set.HRelation α β} (hG : isOneToOne G)
  : comp G (inv G) = { p | p.1 ∈ ran G ∧ p.1 = p.2 } :=
  exercise_3_25_b hG.left

/-- ### Exercise 3.27

Show that `dom (F ∘ G) = G⁻¹⟦dom F⟧` for any sets `F` and `G`. (`F` and `G` need
not be functions.)
-/
theorem exercise_3_27 {F : Set.HRelation β γ} {G : Set.HRelation α β}
  : dom (comp F G) = image (inv G) (dom F) := by
  rw [Set.Subset.antisymm_iff]
  apply And.intro
  · show ∀ x, x ∈ dom (comp F G) → x ∈ image (inv G) (dom F)
    intro x hx
    have ⟨y, t, ht⟩ := dom_exists hx
    have htF : t ∈ dom F := mem_pair_imp_fst_mem_dom ht.right
    unfold image inv
    simp only [Prod.exists, Set.mem_setOf_eq, Prod.mk.injEq]
    exact ⟨t, htF, x, t, ht.left, rfl, rfl⟩

  · show ∀ x, x ∈ image (inv G) (dom F) → x ∈ dom (comp F G)
    intro x hx
    unfold image at hx
    simp only [mem_self_comm_mem_inv, Set.mem_setOf_eq] at hx
    have ⟨u, hu⟩ := hx
    have ⟨t, ht⟩ := dom_exists hu.left

    unfold dom comp
    simp only [
      Set.mem_image,
      Set.mem_setOf_eq,
      Prod.exists,
      exists_and_right,
      exists_eq_right
    ]
    exact ⟨t, u, hu.right, ht⟩

/-- ### Exercise 3.28

Assume that `f` is a one-to-one function from `A` into `B`, and that `G` is the
function with `dom G = 𝒫 A` defined by the equation `G(X) = f⟦X⟧`. Show that `G`
maps `𝒫 A` one-to-one into `𝒫 B`.
-/
theorem exercise_3_28 {A : Set α} {B : Set β}
  {f : Set.HRelation α β} {G : Set.HRelation (Set α) (Set β)}
  (hf : isOneToOne f ∧ mapsInto f A B)
  (hG : G = { p | p.1 ∈ 𝒫 A ∧ p.2 = image f p.1 })
  : isOneToOne G ∧ mapsInto G (𝒫 A) (𝒫 B) := by
  have dG : dom G = 𝒫 A := by
    rw [hG]
    ext p
    unfold dom Prod.fst
    simp

  have hG₁ : isSingleValued G := by
    intro x hx
    have ⟨y, hy⟩ := dom_exists hx
    refine ⟨y, ⟨mem_pair_imp_snd_mem_ran hy, hy⟩, ?_⟩
    intro y₁ hy₁
    rw [hG, Set.mem_setOf_eq] at hy
    conv at hy₁ => rhs; rw [hG, Set.mem_setOf_eq]
    simp only at *
    rw [hy.right, hy₁.right.right]

  apply And.intro
  · show isOneToOne G
    refine ⟨hG₁, ?_⟩
    intro y hy
    have ⟨X₁, hX₁⟩ := ran_exists hy
    refine ⟨X₁, ⟨mem_pair_imp_fst_mem_dom hX₁, hX₁⟩, ?_⟩
    intro X₂ hX₂
    have hX₁' : y = image f X₁ := by
      rw [hG] at hX₁
      simp only [Set.mem_powerset_iff, Set.mem_setOf_eq] at hX₁
      exact hX₁.right
    have hX₂' : y = image f X₂ := by
      have := hX₂.right
      rw [hG] at this
      simp only [Set.mem_powerset_iff, Set.mem_setOf_eq] at this
      exact this.right

    ext t
    apply Iff.intro
    · intro ht
      rw [dG] at hX₂
      simp only [Set.mem_powerset_iff] at hX₂

      have ht' := hX₂.left ht
      rw [← hf.right.dom_eq] at ht'
      have ⟨ft, hft⟩ := dom_exists ht'
      have hft' : ft ∈ image f X₂ := ⟨t, ht, hft⟩

      rw [← hX₂', hX₁'] at hft'
      have ⟨t₁, ht₁⟩ := hft'
      rw [single_rooted_eq_unique hf.left.right hft ht₁.right]
      exact ht₁.left

    · intro ht
      have hX₁sub := mem_pair_imp_fst_mem_dom hX₁
      rw [dG] at hX₁sub
      simp only [Set.mem_powerset_iff] at hX₁sub

      have ht' := hX₁sub ht
      rw [← hf.right.dom_eq] at ht'
      have ⟨ft, hft⟩ := dom_exists ht'
      have hft' : ft ∈ image f X₁ := ⟨t, ht, hft⟩

      rw [← hX₁', hX₂'] at hft'
      have ⟨t₁, ht₁⟩ := hft'
      rw [single_rooted_eq_unique hf.left.right hft ht₁.right]
      exact ht₁.left

  · show mapsInto G (𝒫 A) (𝒫 B)
    refine ⟨hG₁, dG, ?_⟩
    show ∀ x, x ∈ ran G → x ∈ 𝒫 B
    intro x hx
    rw [hG] at hx
    unfold ran Prod.snd at hx
    simp only [
      Set.mem_powerset_iff,
      Set.mem_image,
      Set.mem_setOf_eq,
      Prod.exists,
      exists_eq_right
    ] at hx
    have ⟨a, ha⟩ := hx
    rw [ha.right]
    show ∀ y, y ∈ image f a → y ∈ B
    intro y ⟨b, hb⟩
    have hz := mem_pair_imp_snd_mem_ran hb.right
    exact hf.right.ran_ss hz

/-- ### Exercise 3.29

Assume that `f : A → B` and define a function `G : B → 𝒫 A` by
```
G(b) = {x ∈ A | f(x) = b}
```
Show that if `f` maps `A` *onto* `B`, then `G` is one-to-one. Does the converse
hold?
-/
theorem exercise_3_29 {f : Set.HRelation α β} {G : Set.HRelation β (Set α)}
  {A : Set α} {B : Set β} (hf : mapsOnto f A B)
  (hG : mapsInto G B (𝒫 A) ∧ G = { p | p.1 ∈ B ∧ p.2 = {x ∈ A | (x, p.1) ∈ f} })
  : isOneToOne G := by
  unfold isOneToOne
  refine ⟨hG.left.is_func, ?_⟩
  intro y hy
  have ⟨x₁, hx₁⟩ := ran_exists hy
  refine ⟨x₁, ⟨mem_pair_imp_fst_mem_dom hx₁, hx₁⟩, ?_⟩
  intro x₂ hx₂

  have hG₁ : (x₁, {x ∈ A | (x, x₁) ∈ f}) ∈ G := by
    rw [hG.right, ← hG.left.dom_eq]
    simp only [Set.mem_setOf_eq, and_true]
    exact mem_pair_imp_fst_mem_dom hx₁
  have hG₂ : (x₂, {x ∈ A | (x, x₂) ∈ f}) ∈ G := by
    rw [hG.right, ← hG.left.dom_eq]
    simp only [Set.mem_setOf_eq, and_true]
    exact hx₂.left
  have heq : {x ∈ A | (x, x₁) ∈ f} = {x ∈ A | (x, x₂) ∈ f} := by
    have h₁ := single_valued_eq_unique hG.left.is_func hx₁ hG₁
    have h₂ := single_valued_eq_unique hG.left.is_func hx₂.right hG₂
    rw [← h₁, ← h₂]

  rw [hG.right, ← hf.ran_eq] at hG₁
  simp only [Set.mem_setOf_eq, and_true] at hG₁
  have ⟨t, ht⟩ := ran_exists hG₁
  have : t ∈ {x ∈ A | (x, x₁) ∈ f} := by
    refine ⟨?_, ht⟩
    rw [← hf.dom_eq]
    exact mem_pair_imp_fst_mem_dom ht
  rw [heq] at this
  exact single_valued_eq_unique hf.is_func this.right ht

/-! ### Exercise 3.30

Assume that `F : 𝒫 A → 𝒫 A` and that `F` has the monotonicity property:
```
X ⊆ Y ⊆ A → F(X) ⊆ F(Y).
```
Define `B = ⋂ {X ⊆ A | F(X) ⊆ X}` and `C = ⋃ {X ⊆ A | X ⊆ F(X)}`.
-/

section Exercise_3_30

variable {F : Set α → Set α} {A B C : Set α}
         (hF : Set.MapsTo F (𝒫 A) (𝒫 A))
         (hMono : ∀ X Y, X ⊆ Y ∧ Y ⊆ A → F X ⊆ F Y)
         (hB : B = ⋂₀ { X | X ⊆ A ∧ F X ⊆ X })
         (hC : C = ⋃₀ { X | X ⊆ A ∧ X ⊆ F X })

/-- #### Exercise 3.30 (a)

Show that `F(B) = B` and `F(C) = C`.
-/
theorem exercise_3_30_a : F B = B ∧ F C = C := by

  have hB_subset : F B ⊆ B := by
    intro x hx
    have : ∀ X, X ⊆ A ∧ F X ⊆ X → x ∈ X := by
      intro X ⟨hX₁, hX₂⟩
      have hB₁ : B ⊆ X := by
        show ∀ t, t ∈ B → t ∈ X
        intro t ht
        rw [hB] at ht
        simp only [Set.mem_sInter] at ht
        exact ht X ⟨hX₁, hX₂⟩
      exact hX₂ (hMono B X ⟨hB₁, hX₁⟩ hx)
    rw [hB]
    exact this

  have hC_supset : C ⊆ F C := by
    intro x hx
    rw [hC] at hx
    simp only [Set.mem_sUnion, Set.mem_setOf_eq] at hx
    have ⟨X, hX⟩ := hx
    have hC₁ : X ⊆ C := by
      show ∀ t, t ∈ X → t ∈ C
      intro t ht
      rw [hC]
      simp only [Set.mem_sUnion, Set.mem_setOf_eq]
      exact ⟨X, hX.left, ht⟩
    have hC₂ : C ⊆ A := by
      show ∀ t, t ∈ C → t ∈ A
      intro t ht
      rw [hC] at ht
      simp only [Set.mem_sUnion, Set.mem_setOf_eq] at ht
      have ⟨T, hT⟩ := ht
      exact hT.left.left hT.right
    exact hMono X C ⟨hC₁, hC₂⟩ (hX.left.right hX.right)

  have hC_sub_A : C ⊆ A := by
    show ∀ t, t ∈ C → t ∈ A
    intro t ht
    rw [hC] at ht
    simp at ht
    have ⟨X, hX⟩ := ht
    exact hX.left.left hX.right

  have hFC_sub_A : F C ⊆ A := by
    show ∀ t, t ∈ F C → t ∈ A
    intro t ht
    have := hF hC_sub_A
    simp only [Set.mem_powerset_iff] at this
    exact this ht

  have hC_subset : F C ⊆ C := by
    suffices ∀ X, X ∈ {X | X ⊆ A ∧ X ⊆ F X} → X ⊆ C from
      this (F C) ⟨hFC_sub_A, hMono C (F C) ⟨hC_supset, hFC_sub_A⟩⟩
    intro X hX
    simp at hX
    rw [hC]
    show ∀ t, t ∈ X → t ∈ ⋃₀ {X | X ⊆ A ∧ X ⊆ F X}
    intro t ht
    simp only [Set.mem_sUnion, Set.mem_setOf_eq]
    exact ⟨X, hX, ht⟩

  have hB_sub_A : B ⊆ A := by
    show ∀ t, t ∈ B → t ∈ A
    intro t ht
    rw [hB] at ht
    simp only [Set.mem_sInter, Set.mem_setOf_eq] at ht
    have := ht C ⟨hC_sub_A, hC_subset⟩
    exact hC_sub_A this

  apply And.intro
  · rw [Set.Subset.antisymm_iff]
    apply And.intro
    · exact hB_subset
    · have hInter : ∀ X, X ∈ {X | X ⊆ A ∧ F X ⊆ X} → B ⊆ X := by
        intro X hX
        simp only [Set.mem_setOf_eq] at hX
        rw [hB]
        show ∀ t, t ∈ ⋂₀ {X | X ⊆ A ∧ F X ⊆ X} → t ∈ X
        intro t ht
        simp only [Set.mem_sInter, Set.mem_setOf_eq] at ht
        exact ht X hX
      refine hInter (F B) ⟨?_, ?_⟩
      · show ∀ t, t ∈ F B → t ∈ A
        intro t ht
        have := hF hB_sub_A
        simp only [Set.mem_powerset_iff] at this
        exact this ht
      · refine hMono (F B) B ⟨hB_subset, hB_sub_A⟩
  · rw [Set.Subset.antisymm_iff]
    exact ⟨hC_subset, hC_supset⟩

/-- #### Exercise 3.30 (b)

Show that if `F(X) = X`, then `B ⊆ X ⊆ C`.
-/
theorem exercise_3_30_b : ∀ X, X ⊆ A ∧ F X = X → B ⊆ X ∧ X ⊆ C := by
  intro X ⟨hX₁, hX₂⟩
  apply And.intro
  · have : F X ⊆ X := Eq.subset hX₂
    rw [hB]
    show ∀ t, t ∈ ⋂₀ {X | X ⊆ A ∧ F X ⊆ X} → t ∈ X
    intro t ht
    simp only [Set.mem_sInter, Set.mem_setOf_eq] at ht
    exact ht X ⟨hX₁, this⟩
  · have : X ⊆ F X := Eq.subset (id (Eq.symm hX₂))
    rw [hC]
    show ∀ t, t ∈ X → t ∈ ⋃₀ {X | X ⊆ A ∧ X ⊆ F X}
    intro t ht
    simp only [Set.mem_sUnion, Set.mem_setOf_eq]
    exact ⟨X, ⟨hX₁, this⟩, ht⟩

end Exercise_3_30

/-- ### Exercise 3.32 (a)

Show that `R` is symmetric **iff** `R⁻¹ ⊆ R`.
-/
theorem exercise_3_32_a {R : Set.Relation α}
  : isSymmetric R ↔ inv R ⊆ R := by
  apply Iff.intro
  · intro hR
    show ∀ p, p ∈ inv R → p ∈ R
    intro (x, y) hp
    simp only [mem_self_comm_mem_inv] at hp
    exact hR hp
  · intro hR
    unfold isSymmetric
    intro x y hp
    rw [← mem_self_comm_mem_inv] at hp
    exact hR hp

/-- ### Exercise 3.32 (b)

Show that `R` is transitive **iff** `R ∘ R ⊆ R`.
-/
theorem exercise_3_32_b {R : Set.Relation α}
  : isTransitive R ↔ comp R R ⊆ R := by
  apply Iff.intro
  · intro hR
    show ∀ p, p ∈ comp R R → p ∈ R
    intro (x, y) hp
    have ⟨t, ht⟩ := hp
    exact hR ht.left ht.right
  · intro hR
    intro x y z hx hz
    have : (x, z) ∈ comp R R := ⟨y, hx, hz⟩
    exact hR this

/-- ### Exercise 3.33

Show that `R` is a symmetric and transitive relation **iff** `R = R⁻¹ ∘ R`.
-/
theorem exercise_3_33 {R : Set.Relation α}
  : isSymmetric R ∧ isTransitive R ↔ R = comp (inv R) R := by
  have hR : comp (inv R) R = { p | ∃ t, (p.1, t) ∈ R ∧ (p.2, t) ∈ R } := by
      ext p
      unfold comp inv
      simp only [Prod.exists, Set.mem_setOf_eq, Prod.mk.injEq]
      apply Iff.intro
      · intro ⟨t, ht, a, b, h⟩
        refine ⟨t, ht, ?_⟩
        rw [← h.right.right, ← h.right.left]
        exact h.left
      · intro ⟨t, ht⟩
        exact ⟨t, ht.left, p.snd, t, ht.right, rfl, rfl⟩

  apply Iff.intro
  · intro h
    rw [Set.Subset.antisymm_iff]
    apply And.intro
    · show ∀ p, p ∈ R → p ∈ comp (inv R) R
      intro (x, y) hp
      have hy := h.left hp
      have hx := h.right hp hy
      rw [hR]
      exact ⟨x, hx, hy⟩
    · show ∀ p, p ∈ comp (inv R) R → p ∈ R
      intro (x, y) hp
      rw [hR] at hp
      have ⟨_, ht⟩ := hp
      have := h.left ht.right
      exact h.right ht.left this
  · intro h
    have hS : isSymmetric R := by
      intro x y hp
      have : inv R = R := by
        calc inv R
          _ = inv (comp (inv R) R) := by conv => lhs; rw [h]
          _ = comp (inv R) (inv (inv R)) := by rw [comp_inv_eq_inv_comp_inv]
          _ = comp (inv R) R := by rw [inv_inv_eq_self]
          _ = R := h.symm
      rwa [← this, mem_self_comm_mem_inv]
    refine ⟨hS, ?_⟩
    intro x y z hx hy
    have : (z, y) ∈ R := hS hy
    rw [h, hR]
    exact ⟨y, hx, this⟩

/-- ### Exercise 3.34 (a)

Assume that `𝓐` is a nonempty set, every member of which is a transitive
relation. Is the set `⋂ 𝓐` a transitive relation?
-/
theorem exercise_3_34_a {𝓐 : Set (Set.Relation α)}
  (_ : Set.Nonempty 𝓐) (h𝓐 : ∀ A ∈ 𝓐, isTransitive A)
  : isTransitive (⋂₀ 𝓐) := by
  intro x y z hx hy
  simp only [Set.mem_sInter] at *
  intro A hA
  have hx' := hx A hA
  have hy' := hy A hA
  exact h𝓐 A hA hx' hy'

/-- ### Exercise 3.34 (b)

Assume that `𝓐` is a nonempty set, every member of which is a transitive
relation. Is `⋃ 𝓐` a transitive relation?
-/
theorem exercise_3_34_b {𝓐 : Set (Set.Relation ℕ)}
  (_ : Set.Nonempty 𝓐) (h𝓐 : 𝓐 = {{(1, 2), (2, 3), (1, 3)}, {(2, 1)}})
  : (∀ A ∈ 𝓐, isTransitive A) ∧ ¬ isTransitive (⋃₀ 𝓐) := by
  apply And.intro
  · intro A hA
    rw [h𝓐] at hA
    simp only [Set.mem_singleton_iff, Set.mem_insert_iff] at hA
    apply Or.elim hA
    · intro hA₁
      rw [hA₁]
      intro x y z hx hy
      simp only [Set.mem_singleton_iff, Set.mem_insert_iff, Prod.mk.injEq] at *
      casesm* _ ∨ _
      all_goals case _ hl hr => first
        | {rw [hl.right] at hr; simp at hr}
        | {rw [hl.left] at hr; simp at hr}
        | {right; right; exact ⟨hl.left, hr.right⟩}
    · intro hA₁
      rw [hA₁]
      intro x y z hx hy
      simp only [Set.mem_singleton_iff, Set.mem_insert_iff, Prod.mk.injEq] at *
      rw [hx.right] at hy
      simp at hy
  · intro h
    have h₁ : (1, 2) ∈ ⋃₀ 𝓐 := by
      simp only [Set.mem_sUnion]
      exact ⟨{(1, 2), (2, 3), (1, 3)}, by rw [h𝓐]; simp, by simp⟩
    have h₂ : (2, 1) ∈ ⋃₀ 𝓐 := by
      simp only [Set.mem_sUnion]
      exact ⟨{(2, 1)}, by rw [h𝓐]; simp, by simp⟩
    have h₃ : (1, 1) ∉ ⋃₀ 𝓐 := by
      simp only [Set.mem_sUnion]
      rw [h𝓐]
      intro ⟨t, ht⟩
      simp only [Set.mem_singleton_iff, Set.mem_insert_iff] at ht
      have := ht.right
      apply Or.elim ht.left <;>
      · intro ht₁
        rw [ht₁] at this
        simp at this
    exact absurd (h h₁ h₂) h₃

/-- ### Exercise 3.35

Show that for any `R` and `x`, we have `[x]_R = R⟦{x}⟧`.
-/
theorem exercise_3_35 {R : Set.Relation α} {x : α}
  : neighborhood R x = image R {x} := by
  calc neighborhood R x
    _ = { t | (x, t) ∈ R } := rfl
    _ = { t | ∃ u ∈ ({x} : Set α), (u, t) ∈ R } := by simp
    _ = image R {x} := rfl

/-- ### Exercise 3.36

Assume that `f : A → B` and that `R` is an equivalence relation on `B`. Define
`Q` to be the set `{⟨x, y⟩ ∈ A × A | ⟨f(x), f(y)⟩ ∈ R}`. Show that `Q` is an
equivalence relation on `A`.
-/
theorem exercise_3_36 {f : Set.HRelation α β}
  {Q : Set.Relation α} {R : Set.Relation β} {A : Set α} {B : Set β}
  (hf : mapsInto f A B) (hR : isEquivalence R B)
  (hQ : Q = { p | ∃ fx fy : β, (p.1, fx) ∈ f ∧ (p.2, fy) ∈ f ∧ (fx, fy) ∈ R })
  : isEquivalence Q A := by
  refine ⟨?_, ?_, ?_, ?_⟩

  · -- `fld Q ⊆ A`
    show ∀ x, x ∈ fld Q → x ∈ A
    intro x hx
    rw [hQ] at hx
    unfold fld dom ran at hx
    simp only [
      exists_and_left,
      Set.mem_union,
      Set.mem_image,
      Set.mem_setOf_eq,
      Prod.exists,
      exists_and_right,
      exists_eq_right
    ] at hx
    apply Or.elim hx
    · intro ⟨_, _, hx₁⟩
      rw [← hf.dom_eq]
      exact mem_pair_imp_fst_mem_dom hx₁.left
    · intro ⟨_, _, _, _, hx₂⟩
      rw [← hf.dom_eq]
      exact mem_pair_imp_fst_mem_dom hx₂.left

  · -- `isReflexive Q A`
    intro x hx
    rw [← hf.dom_eq] at hx
    have ⟨fx, hfx⟩ := dom_exists hx
    have := hR.refl fx (hf.ran_ss $ mem_pair_imp_snd_mem_ran hfx)
    rw [hQ]
    simp only [exists_and_left, Set.mem_setOf_eq]
    exact ⟨fx, hfx, fx, hfx, this⟩

  · -- `isSymmetric Q`
    intro x y h
    rw [hQ] at h
    simp only [exists_and_left, Set.mem_setOf_eq] at h
    have ⟨fx, hfx, fy, hfy, h'⟩ := h
    have := hR.symm h'
    rw [hQ]
    simp only [exists_and_left, Set.mem_setOf_eq]
    exact ⟨fy, hfy, fx, hfx, this⟩

  · -- `isTransitive Q`
    intro x y z hx hy
    rw [hQ] at hx hy
    simp only [exists_and_left, Set.mem_setOf_eq] at hx hy
    have ⟨fx, hfx, fy, hfy, h₁⟩ := hx
    have ⟨fy₁, hfy₁, fz, hfz, h₂⟩ := hy
    have hfy' : fy = fy₁ := single_valued_eq_unique hf.is_func hfy hfy₁
    rw [hfy'] at h₁
    rw [hQ]
    simp only [exists_and_left, Set.mem_setOf_eq]
    exact ⟨fx, hfx, fz, hfz, hR.trans h₁ h₂⟩

/-- ### Exercise 3.37

Assume that `P` is a partition of a set `A`. Define the relation `Rₚ` as
follows:
```
xRₚy ↔ (∃ B ∈ Π)(x ∈ B ∧ y ∈ B).
```
Show that `Rₚ` is an equivalence relation on `A`. (This is a formalized version
of the discussion at the beginning of this section.)
-/
theorem exercise_3_37 {P : Set (Set α)} {A : Set α}
  (hP : Partition P A) (Rₚ : Set.Relation α)
  (hRₚ : ∀ x y, (x, y) ∈ Rₚ ↔ ∃ B ∈ P, x ∈ B ∧ y ∈ B)
  : isEquivalence Rₚ A := by
  have hRₚ_eq : Rₚ = { p | ∃ B ∈ P, p.1 ∈ B ∧ p.2 ∈ B } := by
    ext p
    have (x, y) := p
    exact hRₚ x y

  refine ⟨?_, ?_, ?_, ?_⟩
  · -- `fld Rₚ ⊆ A`
    show ∀ x, x ∈ fld Rₚ → x ∈ A
    rw [hRₚ_eq]
    intro x hx
    unfold fld dom ran at hx
    simp only [
      Set.mem_union,
      Set.mem_image,
      Set.mem_setOf_eq,
      Prod.exists,
      exists_and_right,
      exists_eq_right
    ] at hx
    apply Or.elim hx
    · intro ⟨t, B, hB⟩
      have := hP.p_subset B hB.left
      exact this hB.right.left
    · intro ⟨a, B, hB⟩
      have := hP.p_subset B hB.left
      exact this hB.right.right

  · -- `isReflexive Rₚ A`
    intro x hx
    rw [hRₚ_eq]
    simp only [Set.mem_setOf_eq, and_self]
    exact hP.exhaustive x hx

  · -- `isSymmetric Rₚ`
    intro x y h
    rw [hRₚ_eq] at h
    simp only [Set.mem_setOf_eq] at h
    have ⟨B, hB⟩ := h
    rw [hRₚ_eq]
    simp only [Set.mem_setOf_eq]
    conv at hB => right; rw [and_comm]
    exact ⟨B, hB⟩

  · -- `isTransitive Rₚ`
    intro x y z hx hy
    rw [hRₚ_eq] at hx hy
    simp only [Set.mem_setOf_eq] at hx hy
    have ⟨B₁, hB₁⟩ := hx
    have ⟨B₂, hB₂⟩ := hy
    have hB : B₁ = B₂ := by
      have hy₁ : y ∈ B₁ := hB₁.right.right
      have hy₂ : y ∈ B₂ := hB₂.right.left
      have hy := hP.disjoint B₁ hB₁.left B₂ hB₂.left
      rw [contraposition] at hy
      simp at hy
      suffices B₁ ∩ B₂ ≠ ∅ from hy this
      intro h'
      rw [Set.ext_iff] at h'
      exact (h' y).mp ⟨hy₁, hy₂⟩
    rw [hRₚ_eq]
    simp only [Set.mem_setOf_eq]
    exact ⟨B₁, hB₁.left, hB₁.right.left, by rw [hB]; exact hB₂.right.right⟩

/-- ### Exercise 3.38

Theorem 3P shows that `A / R` is a partition of `A` whenever `R` is an
equivalence relation on `A`. Show that if we start with the equivalence relation
`Rₚ` of the preceding exercise, then the partition `A / Rₚ` is just `P`.
-/
theorem exercise_3_38 {P : Set (Set α)} {A : Set α}
  (hP : Partition P A) (Rₚ : Set.Relation α)
  (hRₚ : ∀ x y, (x, y) ∈ Rₚ ↔ ∃ B ∈ P, x ∈ B ∧ y ∈ B)
  : modEquiv (exercise_3_37 hP Rₚ hRₚ) = P := by
  have hRₚ_eq : Rₚ = { p | ∃ B ∈ P, p.1 ∈ B ∧ p.2 ∈ B } := by
    ext p
    have (x, y) := p
    exact hRₚ x y

  ext B
  apply Iff.intro
  · intro ⟨x, hx⟩
    have ⟨B', hB'⟩ := partition_mem_mem_eq hP hx.left
    simp only at hB'
    suffices B = B' by
      rw [this]
      exact hB'.left.left

    ext y
    apply Iff.intro
    · intro hy
      rw [← hx.right, hRₚ_eq] at hy
      have ⟨B₁, hB₁⟩ := hy
      have := hB'.right B₁ ⟨hB₁.left, hB₁.right.left⟩
      rw [← this]
      exact hB₁.right.right
    · intro hy
      rw [← hx.right, hRₚ_eq]
      exact ⟨B', hB'.left.left, hB'.left.right, hy⟩

  · intro hB
    have ⟨x, hx⟩ := hP.nonempty B hB
    have hx' : x ∈ A := hP.p_subset B hB hx
    refine ⟨x, hx', Eq.symm ?_⟩
    calc B
      _ = {t | x ∈ B ∧ t ∈ B} := by
        ext y
        apply Iff.intro
        · intro hy
          exact ⟨hx, hy⟩
        · intro hy
          exact hy.right
      _ = {t | ∃ B₁ ∈ P, x ∈ B₁ ∧ t ∈ B₁} := by
        ext y
        apply Iff.intro
        · intro hy
          exact ⟨B, hB, hy⟩
        · intro hy
          have ⟨B₁, hB₁⟩ := hy
          have ⟨B', hB'⟩ := partition_mem_mem_eq hP hx'
          simp only [Set.mem_setOf_eq] at *
          have : B = B₁ := by
            have lhs := hB'.right B ⟨hB, hx⟩
            have rhs := hB'.right B₁ ⟨hB₁.left, hB₁.right.left⟩
            rw [lhs, rhs]
          rw [this]
          exact hB₁.right
      _ = {t | (x, t) ∈ Rₚ } := by
        rw [hRₚ_eq]
        simp only [Set.mem_setOf_eq]
      _ = neighborhood Rₚ x := rfl

/-- ### Exercise 3.39

Assume that we start with an equivalence relation `R` on `A` and define `P` to
be the partition `A / R`. Show that `Rₚ`, as defined in Exercise 37, is just
`R`.
-/
theorem exercise_3_39 {P : Set (Set α)} {R Rₚ : Set.Relation α} {A : Set α}
  (hR : isEquivalence R A) (hP : P = modEquiv hR)
  (hRₚ : ∀ x y, (x, y) ∈ Rₚ ↔ ∃ B ∈ P, x ∈ B ∧ y ∈ B)
  : Rₚ = R := by
  have hRₚ_eq : Rₚ = { p | ∃ B ∈ P, p.1 ∈ B ∧ p.2 ∈ B } := by
    ext p
    have (x, y) := p
    exact hRₚ x y

  ext p
  have (x, y) := p
  apply Iff.intro
  · intro hp
    rw [hRₚ_eq] at hp
    have ⟨B, hB, hx, hy⟩ := hp
    rw [hP] at hB
    have ⟨z, hz⟩ := hB
    rw [← hz.right] at hx hy
    exact neighborhood_mem_imp_relate hR hx hy
  · intro hp
    have hxA : x ∈ A := hR.b_on (Or.inl (mem_pair_imp_fst_mem_dom hp))
    have hyA : y ∈ A := hR.b_on (Or.inr (mem_pair_imp_snd_mem_ran hp))
    rw [hRₚ_eq]
    have hx : x ∈ neighborhood R x := neighborhood_self_mem hR hxA
    have hy : y ∈ neighborhood R x := by
      rw [← neighborhood_eq_iff_mem_relate hR hxA hyA] at hp
      rw [hp]
      exact neighborhood_self_mem hR hyA
    refine ⟨neighborhood R x, ?_, ⟨hx, hy⟩⟩
    rw [hP]
    exact ⟨x, hxA, rfl⟩

/-- ### Exercise 3.41 (a)

Let `ℝ` be the set of real numbers and define the realtion `Q` on `ℝ × ℝ` by
`⟨u, v⟩ Q ⟨x, y⟩` **iff** `u + y = x + v`. Show that `Q` is an equivalence
relation on `ℝ × ℝ`.
-/
theorem exercise_3_41_a {Q : Set.Relation (ℝ × ℝ)}
  (hQ : ∀ u v x y, ((u, v), (x, y)) ∈ Q ↔ u + y = x + v)
  : isEquivalence Q (Set.univ : Set (ℝ × ℝ)) := by
  have hQ_eq : Q = {p | p.1.1 + p.2.2 = p.2.1 + p.1.2} := by
    ext p
    apply Iff.intro <;>
    · intro hp
      rwa [hQ] at *

  refine ⟨?_, ?_, ?_, ?_⟩

  · -- `fld Q ⊆ Set.univ`
    show ∀ p, p ∈ fld Q → p ∈ Set.univ
    intro _ _
    simp only [Set.mem_univ]

  · -- `isReflexive Q Set.univ`
    intro (x, y) _
    rw [hQ_eq]
    simp

  · -- `isSymmetric Q`
    intro (u, v) (x, y) hp
    rw [hQ_eq] at *
    exact Eq.symm hp

  · -- `isTransitive Q`
    unfold isTransitive
    intro (u, v) (x, y) (a, b) h₁ h₂
    rw [hQ_eq] at *
    simp at h₁ h₂
    simp
    have h₁' : u - v = x - y := by
      have := sub_eq_of_eq_add h₁
      rw [add_sub_right_comm] at this
      exact eq_sub_of_add_eq this
    have h₂' : x - y = a - b := by
      have := sub_eq_of_eq_add h₂
      rw [add_sub_right_comm] at this
      exact eq_sub_of_add_eq this
    rw [h₂'] at h₁'
    have := eq_add_of_sub_eq' h₁'
    rw [← add_sub_assoc] at this
    have := add_eq_of_eq_sub this
    conv => right; rw [add_comm]
    exact this

/-- ### Exercise 3.43

Assume that `R` is a linear ordering on a set `A`. Show that `R⁻¹` is also a
linear ordering on `A`.
-/
theorem exercise_3_43 {R : Rel α α} (hR : IsStrictTotalOrder α R)
  : IsStrictTotalOrder α R.inv := by
  refine { trichotomous := ?_, irrefl := ?_, trans := ?_ }
  · intro a b
    unfold Rel.inv flip
    apply Or.elim (hR.trichotomous a b)
    · intro h; right; right; exact h
    · intro h
      apply Or.elim h
      · intro h; right; left; exact h
      · intro h; left; exact h
  · intro x h
    unfold Rel.inv flip at h
    exact absurd h (hR.irrefl x)
  · intro a b c hab hac
    unfold Rel.inv flip at *
    exact hR.trans c b a hac hab

/-! ### Exercise 3.44

Assume that `<` is a linear ordering on a set `A`. Assume that `f : A → A` and
that `f` has the property that whenever `x < y`, then `f(x) < f(y)`. Show that
`f` is one-to-one and that whenever `f(x) < f(y)`, then `x < y`.
-/

theorem exercise_3_44_i {R : Rel α α} (hR : IsStrictTotalOrder α R)
  (f : α → α) (hf : ∀ x y, R x y → R (f x) (f y))
  : Function.Injective f := by
  unfold Function.Injective
  intro x₁ x₂ hx
  apply Or.elim (hR.trichotomous x₁ x₂)
  · -- `x₁ < x₂`
    intro hx₁
    have nh := hf x₁ x₂ hx₁
    rw [hx] at nh
    exact absurd nh (hR.irrefl (f x₂))
  · intro hx₁
    apply Or.elim hx₁
    · simp  -- `x₁ = x₂`
    · -- `x₁ > x₂`
      intro hx₂
      have nh := hf x₂ x₁ hx₂
      rw [← hx] at nh
      exact absurd nh (hR.irrefl (f x₁))

theorem exercise_3_44_ii {R : Rel α α} (hR : IsStrictTotalOrder α R)
  (f : α → α) (hf : ∀ x y, R x y → R (f x) (f y))
  : R (f x) (f y) → R x y := by
  intro h
  apply Or.elim (hR.trichotomous x y)
  · simp  -- `x < y`
  · intro h₁
    apply Or.elim h₁
    · -- `x = y`
      intro h₂
      rw [h₂] at h
      exact absurd h (hR.irrefl (f y))
    · -- `x > y`
      intro h₂
      have := hR.trans (f x) (f y) (f x) h (hf y x h₂)
      exact absurd this (hR.irrefl (f x))

/-- ### Exercise 3.45

Assume that `<_A` and `<_B` are linear orderings on `A` and `B`, respectively.
Define the binary relation `<_L` on the Cartesian product `A × B` by:
```
⟨a₁, b₁⟩ <_L ⟨a₂, b₂⟩ iff either a₁ <_A a₂ or (a₁ = a₂ ∧ b₁ <_B b₂).
```
Show that `<_L` is a linear ordering on `A × B`. (The relation `<_L` is called
*lexicographic* ordering, being the ordering used in making dictionaries.)
-/
theorem exercise_3_45 {A : Rel α α} {B : Rel β β} {R : Rel (α × β) (α × β)}
  (hA : IsStrictTotalOrder α A) (hB : IsStrictTotalOrder β B)
  (hR : ∀ a₁ b₁ a₂ b₂, R (a₁, b₁) (a₂, b₂) ↔ A a₁ a₂ ∨ (a₁ = a₂ ∧ B b₁ b₂))
  : IsStrictTotalOrder (α × β) R := by
  refine { trichotomous := ?_, irrefl := ?_, trans := ?_ }
  · intro (a₁, b₁) (a₂, b₂)
    apply Or.elim (hA.trichotomous a₁ a₂)
    · -- `a₁ <_A a₂`
      intro ha
      left
      exact (hR a₁ b₁ a₂ b₂).mpr (Or.inl ha)
    · intro ha
      apply Or.elim ha
      · -- `a₁ = a₂`
        intro ha₁
        apply Or.elim (hB.trichotomous b₁ b₂)
        · -- `b₁ <_B b₂`
          intro hb
          left
          exact (hR a₁ b₁ a₂ b₂).mpr (Or.inr ⟨ha₁, hb⟩)
        · intro hb
          apply Or.elim hb
          · -- `b₁ = b₂`
            intro hb₁
            right; left
            rw [ha₁, hb₁]
          · -- `b₂ <_B b₁`
            intro hb₁
            right; right
            exact (hR a₂ b₂ a₁ b₁).mpr (Or.inr ⟨ha₁.symm, hb₁⟩)
      · -- `a₂ <_A a₁`
        intro ha₁
        right; right
        exact (hR a₂ b₂ a₁ b₁).mpr (Or.inl ha₁)
  · intro (a, b) h
    have := (hR a b a b).mp h
    apply Or.elim this
    · intro ha₁
      exact absurd ha₁ (hA.irrefl a)
    · intro ⟨_, hb₁⟩
      exact absurd hb₁ (hB.irrefl b)
  · intro (a₁, b₁) (a₂, b₂) (a₃, b₃) h₁ h₂
    have h₁' := (hR a₁ b₁ a₂ b₂).mp h₁
    have h₂' := (hR a₂ b₂ a₃ b₃).mp h₂
    apply Or.elim h₁'
    · -- `a₁ <_A a₂`
      intro ha₁
      apply Or.elim h₂'
      · -- `a₂ <_A a₃`
        intro ha₂
        have := hA.trans a₁ a₂ a₃ ha₁ ha₂
        exact (hR a₁ b₁ a₃ b₃).mpr (Or.inl this)
      · -- `a₂ = a₃ ∧ b₂ <_B b₃`
        intro ha₂
        rw [ha₂.left] at ha₁
        exact (hR a₁ b₁ a₃ b₃).mpr (Or.inl ha₁)
    · -- `a₁ = a₂ ∧ b₁ <_B b₂`
      intro ha₁
      apply Or.elim h₂'
      · -- `a₂ <_A a₃`
        intro ha₂
        rw [← ha₁.left] at ha₂
        exact (hR a₁ b₁ a₃ b₃).mpr (Or.inl ha₂)
      · -- `a₂ = a₃ ∧ b₂ <_B b₃`
        intro ⟨ha₂, hb₂⟩
        rw [← ha₁.left] at ha₂
        have := hB.trans b₁ b₂ b₃ ha₁.right hb₂
        exact (hR a₁ b₁ a₃ b₃).mpr (Or.inr ⟨ha₂, this⟩)

end Enderton.Set.Chapter_3