From dde77d0088707069d4ca7c4bfde2a5c197b202a4 Mon Sep 17 00:00:00 2001
From: Ira Fesefeldt <fesefeldt@cs.rwth-aachen.de>
Date: Sat, 9 Dec 2023 10:05:08 +0100
Subject: [PATCH 01/31] finished proof

---
 Mathlib/Logic/Function/Basic.lean             |   5 +
 Mathlib/Order/FixedPoints.lean                |   3 +
 .../Order/OrdinalApproximantsFixedPoints.lean | 335 ++++++++++++++++++
 Mathlib/SetTheory/Cardinal/Basic.lean         |   7 +
 4 files changed, 350 insertions(+)
 create mode 100644 Mathlib/Order/OrdinalApproximantsFixedPoints.lean

diff --git a/Mathlib/Logic/Function/Basic.lean b/Mathlib/Logic/Function/Basic.lean
index 1168828f19521..d46a05a6a65d0 100644
--- a/Mathlib/Logic/Function/Basic.lean
+++ b/Mathlib/Logic/Function/Basic.lean
@@ -116,6 +116,11 @@ theorem Injective.ne_iff' (hf : Injective f) {x y : α} {z : β} (h : f y = z) :
   h ▸ hf.ne_iff
 #align function.injective.ne_iff' Function.Injective.ne_iff'
 
+theorem Injective.not_exists_equal (h: ¬ Injective f): ∃ a b, a ≠ b ∧ f a = f b := by
+  unfold Injective at h; simp at h
+  let ⟨a, b, h_f, h_ab⟩ := h
+  exact ⟨a, b, h_ab, h_f⟩
+
 /-- If the co-domain `β` of an injective function `f : α → β` has decidable equality, then
 the domain `α` also has decidable equality. -/
 protected def Injective.decidableEq [DecidableEq β] (I : Injective f) : DecidableEq α :=
diff --git a/Mathlib/Order/FixedPoints.lean b/Mathlib/Order/FixedPoints.lean
index 2369cd7b09476..4a04d99fbd119 100644
--- a/Mathlib/Order/FixedPoints.lean
+++ b/Mathlib/Order/FixedPoints.lean
@@ -111,6 +111,9 @@ theorem le_gfp {a : α} (h : a ≤ f a) : a ≤ gfp f :=
   le_sSup h
 #align order_hom.le_gfp OrderHom.le_gfp
 
+theorem fixed_le_gfp {a : α} (h : f a = a) : a ≤ gfp f  :=
+  f.le_gfp h.ge
+
 theorem gfp_le {a : α} (h : ∀ b, b ≤ f b → b ≤ a) : gfp f ≤ a :=
   sSup_le h
 #align order_hom.gfp_le OrderHom.gfp_le
diff --git a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean b/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
new file mode 100644
index 0000000000000..79eb771a9f4db
--- /dev/null
+++ b/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
@@ -0,0 +1,335 @@
+/-
+Copyright (c) 2023 Ira Fesefeldt. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ira Fesefeldt
+-/
+import Mathlib.Order.FixedPoints
+import Mathlib.Logic.Function.Basic
+import Mathlib.SetTheory.Ordinal.Basic
+import Mathlib.SetTheory.Cardinal.Basic
+import Mathlib.SetTheory.Ordinal.Arithmetic
+
+
+/-!
+# Ordinal Approximants for the Fixed points on complete lattices
+
+This file sets up the ordinal approximation theory of fixed points of a monotone function in a complete lattice.
+
+## Main definitions
+
+* `OrdinalApprox.lfp_approx`: The ordinal approximation of the least fixed point of a bundled monotone function.
+* `OrdinalApprox.gfp_approx`: The ordinal approximation of the greatest fixed point of a bundled monotone function.
+
+## Main theorems
+* `OrdinalApprox.lfp_is_lfp_approx`: The approximation of the least fixed point eventually reaches the least fixed point
+* `OrdinalApprox.gfp_is_gfp_approx`: The approximation of the greatest fixed point eventually reaches the greatest fixed point
+
+## Tags
+
+fixed point, complete lattice, monotone function, ordinals, approximation
+-/
+
+namespace Cardinal
+
+universe u
+variable {α : Type u}
+variable (g: Ordinal → α)
+
+open Cardinal Ordinal SuccOrder Function
+
+def limitation : { i : Ordinal // i < (ord $ succ #α)} → α := λ i => g i
+
+lemma limitation_eq : ∀ i, limitation g i = g i := by
+  intro h; unfold limitation; exact rfl
+
+lemma mk_initialSeg_Subtype (ℵ : Cardinal ):
+  #{ i : Ordinal // i < (ord  ℵ)} = lift.{u+1, u} ℵ := by
+  simpa using mk_initialSeg (ord ℵ)
+
+lemma limitation_not_injective: ¬ Injective (limitation g) := by
+  intro h_inj
+  have h₁ := by apply lift_mk_le_lift_mk_of_injective h_inj;
+  rw[mk_initialSeg_Subtype (succ #α), Cardinal.lift_lift, Cardinal.lift_le] at h₁
+  have h₂ := not_le_of_lt (Cardinal.succ_lt #α)
+  exact h₂ h₁
+
+end Cardinal
+
+
+
+namespace Monotone
+
+
+universe u v
+variable {α : Type u}
+variable {β : Type v}
+variable [Preorder α] [PartialOrder β] (f: α → β)
+
+lemma monotone_stabilizing {a₁ a₂ : α} (h_mon : Monotone f) (h_fa : f a₁ = f a₂):
+    ∀ i, a₂ ≥ i → i ≥ a₁ → f i = f a₁ := by
+  intro i h₂ h₁
+  apply le_antisymm
+  . rw[h_fa]; exact h_mon h₂
+  . exact h_mon h₁
+
+lemma antitone_stabilizing {a₁ a₂ : α} (h_anti : Antitone f) (h_fa : f a₁ = f a₂):
+    ∀ i, a₂ ≥ i → i ≥ a₁ → f i = f a₁ := by
+  intro i h₂ h₁
+  apply le_antisymm
+  . exact h_anti h₁
+  . rw[h_fa]; exact h_anti h₂
+
+end Monotone
+
+/-We loosly follow the proof from Frederico Enchenique in A Short and Constructive Proof of
+  Tarski's fixed-point theorem published in the International Journal of Game Theory Volume 33(2),
+  June 2005, pages 215-218. -/
+
+namespace OrdinalApprox
+
+universe u
+variable {α : Type u}
+variable [CompleteLattice α] (f : α →o α)
+
+open Function fixedPoints Cardinal Order OrderHom
+
+/- Ordinal approximants of the least fixed points -/
+def lfp_approx (a : Ordinal.{u}) : α :=
+  sSup { f (lfp_approx b) | (b : Ordinal) (h : b < a) }
+termination_by lfp_approx a => a
+decreasing_by exact h
+
+lemma lfp_approx_monotone : Monotone (lfp_approx f) := by
+  unfold Monotone; intros a b h; unfold lfp_approx
+  refine sSup_le_sSup ?h; simp
+  intros a' h'
+  use a'; apply And.intro; exact lt_of_lt_of_le h' h
+  exact rfl
+
+def lfp_approx_hom : Ordinal.{u} →o α where
+  toFun i := lfp_approx f i
+  monotone' a b h := by simp; apply lfp_approx_monotone f h
+
+lemma lfp_approx_def (a : Ordinal.{u}): lfp_approx f a = sSup { f (lfp_approx f b) | (b : Ordinal) (_ : b < a) } := by
+  conv => left; unfold lfp_approx
+
+lemma lfp_approx_addition (a : Ordinal.{u}) :
+  f (lfp_approx f a) = lfp_approx f (a+1) := by
+  apply le_antisymm
+  . conv => right; rw[lfp_approx_def]
+    apply le_sSup; simp
+    use a
+  . conv => left; rw[lfp_approx_def]
+    apply sSup_le; simp
+    intros a' h
+    apply f.2; apply lfp_approx_monotone; exact h
+
+
+lemma lfp_approx_stabilizing_at_fp (a : Ordinal.{u}) (h: lfp_approx f a ∈ (fixedPoints f)):
+   ∀ b > a, lfp_approx f b = lfp_approx f a := by
+  intro b hab; rw[mem_fixedPoints_iff] at h;
+  induction b using Ordinal.induction with | h b IH =>
+  apply le_antisymm
+  . conv => left; rw[lfp_approx_def]
+    apply sSup_le; simp
+    intro a' ha'b
+    by_cases haa : a' < a
+    . rw[lfp_approx_addition]
+      apply lfp_approx_monotone
+      simp; exact haa
+    . simp at haa
+      cases (le_iff_lt_or_eq.mp haa) with
+      | inl haa => specialize IH a' ha'b haa; rw[IH, h];
+      | inr haa => rw[←haa, h];
+  . conv => right; rw[lfp_approx_def]
+    apply le_sSup; simp
+    use a
+
+lemma lfp_approx_eq_fp (a : Ordinal.{u}) (h: lfp_approx f a ∈ (fixedPoints f)):
+    ∀ b > a, lfp_approx f b ∈ (fixedPoints f)  := by
+  intro b h_ab;
+  rw[mem_fixedPoints_iff]
+  have h_stab := lfp_approx_stabilizing_at_fp f a h b h_ab
+  rw[h_stab]
+  exact mem_fixedPoints_iff.mp h
+
+
+lemma lfp_approx_has_cycle : ∃ i < ord $ succ #α, ∃ j < ord $ succ #α,
+    i ≠ j ∧ lfp_approx f i = lfp_approx f j := by
+  have h_ninj := Function.Injective.not_exists_equal (limitation_not_injective $ lfp_approx f)
+  let ⟨a, b, h_nab, h_fab⟩ := h_ninj
+  rw[limitation_eq, limitation_eq] at h_fab
+  use a.val; apply And.intro a.prop;
+  use b.val; apply And.intro b.prop;
+  apply And.intro
+  . intro h_eq; rw[Subtype.coe_inj] at h_eq; exact h_nab h_eq
+  . exact h_fab
+
+lemma lfp_approx_one_fixedPoint (a b : Ordinal.{u}) (h : a < b) (h_fab : lfp_approx f a = lfp_approx f b):
+    lfp_approx f a ∈ (fixedPoints f) := by
+  rw[mem_fixedPoints_iff,lfp_approx_addition]
+  apply Monotone.monotone_stabilizing (lfp_approx f) (lfp_approx_monotone f) h_fab (a+1) (SuccOrder.succ_le_of_lt h) (SuccOrder.le_succ a)
+
+lemma lfp_approx_many_fixedPoints (a b : Ordinal.{u}) (h : a < b) (h_fab : lfp_approx f a = lfp_approx f b):
+    ∀ i ≥ a, lfp_approx f i ∈ (fixedPoints f) := by
+  intro i h_i;
+  by_cases h_ia : i = a
+  . rw[h_ia]; exact lfp_approx_one_fixedPoint f a b h h_fab
+  . apply lfp_approx_eq_fp f a
+    . exact lfp_approx_one_fixedPoint f a b h h_fab
+    . exact Ne.lt_of_le' h_ia h_i
+
+lemma lfp_approx_has_fixedPoint_cardinal : lfp_approx f (ord $ succ #α) ∈ (fixedPoints f) := by
+  let ⟨a, h_a, b, h_b, h_nab, h_fab⟩ := lfp_approx_has_cycle f
+  cases (le_total a b) with
+  | inl h_ab =>
+    exact lfp_approx_many_fixedPoints f a b (Ne.lt_of_le h_nab h_ab) h_fab (ord $ succ #α) (le_of_lt h_a)
+  | inr h_ba =>
+    exact lfp_approx_many_fixedPoints f b a (Ne.lt_of_le (id (Ne.symm h_nab)) h_ba) (h_fab.symm) (ord $ succ #α) (le_of_lt h_b)
+
+lemma lfp_approx_le_fixedPoint : ∀ a : (fixedPoints f), ∀ i : Ordinal, lfp_approx f i ≤ a := by
+  intro ⟨a, h_a⟩ i
+  induction i using Ordinal.induction with
+  | h i IH =>
+    rw[lfp_approx_def]
+    apply sSup_le; simp
+    intro j h_j
+    rw[←h_a]
+    apply f.monotone'
+    exact IH j h_j
+
+theorem lfp_is_lfp_approx_cardinal : lfp_approx f (ord $ succ #α) = lfp f := by
+  apply le_antisymm
+  . have h_lfp : ∃ x : fixedPoints f, lfp f = x := by use ⊥; exact rfl
+    let ⟨x, h_x⟩ := h_lfp; rw[h_x]
+    exact lfp_approx_le_fixedPoint f x (ord $ succ #α)
+  . have h_fix : ∃ x: fixedPoints f, lfp_approx f (ord $ succ #α) = x := by {simpa using lfp_approx_has_fixedPoint_cardinal f}
+    let ⟨x, h_x⟩ := h_fix; rw[h_x]
+    exact lfp_le_fixed f x.prop
+
+/-- **Constructive Knaster-Tarski Theorem**: Some ordinal approximation of the least fixed point is the least fixed point.
+  Also known as ordinal approximation of the least fixed point.-/
+theorem lfp_is_lfp_approx : ∃ a : Ordinal, lfp_approx f a = OrderHom.lfp f := by
+  use (ord $ succ #α)
+  exact lfp_is_lfp_approx_cardinal f
+
+
+/- Ordinal approximants of the least fixed points -/
+def gfp_approx (a : Ordinal.{u}) : α :=
+  sInf { f (gfp_approx b) | (b : Ordinal) (h : b < a) }
+termination_by gfp_approx a => a
+decreasing_by exact h
+
+lemma gfp_approx_antitone : Antitone (gfp_approx f) := by
+  unfold Antitone; intros a b h; unfold gfp_approx
+  refine sInf_le_sInf ?h; simp
+  intros a' h'
+  use a'; apply And.intro; exact lt_of_lt_of_le h' h
+  exact rfl
+
+lemma gfp_approx_def (a : Ordinal.{u}): gfp_approx f a = sInf { f (gfp_approx f b) | (b : Ordinal) (_ : b < a) } := by
+  conv => left; unfold gfp_approx
+
+lemma gfp_approx_addition (a : Ordinal.{u}) :
+  f (gfp_approx f a) = gfp_approx f (a+1) := by
+  apply le_antisymm
+  . conv => right; rw[gfp_approx_def]
+    apply le_sInf; simp
+    intros a' h
+    apply f.2; apply gfp_approx_antitone; exact h
+  . conv => left; rw[gfp_approx_def]
+    apply sInf_le; simp
+    use a
+
+
+lemma gfp_approx_stabilizing_at_fp (a : Ordinal.{u}) (h: gfp_approx f a ∈ (fixedPoints f)):
+   ∀ b > a, gfp_approx f b = gfp_approx f a := by
+  intro b hab; rw[mem_fixedPoints_iff] at h;
+  induction b using Ordinal.induction with | h b IH =>
+  apply le_antisymm
+  . conv => left; rw[gfp_approx_def]
+    apply sInf_le
+    use a
+  . conv => right; rw[gfp_approx_def]
+    apply le_sInf; simp
+    intro a' ha'b
+    by_cases haa : a' < a
+    . rw[gfp_approx_addition]
+      apply gfp_approx_antitone
+      simp; exact haa
+    . simp at haa
+      cases (le_iff_lt_or_eq.mp haa) with
+      | inl haa => specialize IH a' ha'b haa; rw[IH, h];
+      | inr haa => rw[←haa, h];
+
+lemma gfp_approx_eq_fp (a : Ordinal.{u}) (h: gfp_approx f a ∈ (fixedPoints f)):
+    ∀ b > a, gfp_approx f b ∈ (fixedPoints f)  := by
+  intro b h_ab;
+  rw[mem_fixedPoints_iff]
+  have h_stab := gfp_approx_stabilizing_at_fp f a h b h_ab
+  rw[h_stab]
+  exact mem_fixedPoints_iff.mp h
+
+
+lemma gfp_approx_has_cycle : ∃ i < ord $ succ #α, ∃ j < ord $ succ #α,
+    i ≠ j ∧ gfp_approx f i = gfp_approx f j := by
+  have h_ninj := Function.Injective.not_exists_equal (limitation_not_injective $ gfp_approx f)
+  let ⟨a, b, h_nab, h_fab⟩ := h_ninj
+  rw[limitation_eq, limitation_eq] at h_fab
+  use a.val; apply And.intro a.prop;
+  use b.val; apply And.intro b.prop;
+  apply And.intro
+  . intro h_eq; rw[Subtype.coe_inj] at h_eq; exact h_nab h_eq
+  . exact h_fab
+
+lemma gfp_approx_one_fixedPoint (a b : Ordinal.{u}) (h : a < b) (h_fab : gfp_approx f a = gfp_approx f b):
+    gfp_approx f a ∈ (fixedPoints f) := by
+  rw[mem_fixedPoints_iff,gfp_approx_addition]
+  apply Monotone.antitone_stabilizing (gfp_approx f) (gfp_approx_antitone f) h_fab (a+1) (SuccOrder.succ_le_of_lt h) (SuccOrder.le_succ a)
+
+lemma gfp_approx_many_fixedPoints (a b : Ordinal.{u}) (h : a < b) (h_fab : gfp_approx f a = gfp_approx f b):
+    ∀ i ≥ a, gfp_approx f i ∈ (fixedPoints f) := by
+  intro i h_i;
+  by_cases h_ia : i = a
+  . rw[h_ia]; exact gfp_approx_one_fixedPoint f a b h h_fab
+  . apply gfp_approx_eq_fp f a
+    . exact gfp_approx_one_fixedPoint f a b h h_fab
+    . exact Ne.lt_of_le' h_ia h_i
+
+lemma gfp_approx_has_fixedPoint_cardinal : gfp_approx f (ord $ succ #α) ∈ (fixedPoints f) := by
+  let ⟨a, h_a, b, h_b, h_nab, h_fab⟩ := gfp_approx_has_cycle f
+  cases (le_total a b) with
+  | inl h_ab =>
+    exact gfp_approx_many_fixedPoints f a b (Ne.lt_of_le h_nab h_ab) h_fab (ord $ succ #α) (le_of_lt h_a)
+  | inr h_ba =>
+    exact gfp_approx_many_fixedPoints f b a (Ne.lt_of_le (id (Ne.symm h_nab)) h_ba) (h_fab.symm) (ord $ succ #α) (le_of_lt h_b)
+
+lemma gfp_approx_ge_fixedPoint : ∀ a : (fixedPoints f), ∀ i : Ordinal, gfp_approx f i ≥ a := by
+  intro ⟨a, h_a⟩ i
+  induction i using Ordinal.induction with
+  | h i IH =>
+    rw[gfp_approx_def]
+    apply le_sInf; simp
+    intro j h_j
+    rw[←h_a]
+    apply f.monotone'
+    exact IH j h_j
+
+
+theorem gfp_is_gfp_approx_cardinal : gfp_approx f (ord $ succ #α) = gfp f := by
+  apply le_antisymm
+  . have h_fix : ∃ x: fixedPoints f, gfp_approx f (ord $ succ #α) = x := by {simpa using gfp_approx_has_fixedPoint_cardinal f}
+    let ⟨x, h_x⟩ := h_fix; rw[h_x]
+    exact fixed_le_gfp f x.prop
+  . have h_lfp : ∃ x : fixedPoints f, gfp f = x := by use ⊤; exact rfl
+    let ⟨x, h_x⟩ := h_lfp; rw[h_x]
+    exact gfp_approx_ge_fixedPoint f x (ord $ succ #α)
+
+
+/-- **Dual Constructive Knaster-Tarski Theorem**: Some ordinal approximation of the greatest fixed point is the greatest fixed point.
+  Also known as ordinal approximation of the greatest fixed point.-/
+theorem gfp_is_gfp_approx : ∃ a : Ordinal, gfp_approx f a = gfp f := by
+  use (ord $ succ #α)
+  exact gfp_is_gfp_approx_cardinal f
+
+end OrdinalApprox
diff --git a/Mathlib/SetTheory/Cardinal/Basic.lean b/Mathlib/SetTheory/Cardinal/Basic.lean
index 8145fddfb5a20..99ae619eff48d 100644
--- a/Mathlib/SetTheory/Cardinal/Basic.lean
+++ b/Mathlib/SetTheory/Cardinal/Basic.lean
@@ -826,6 +826,13 @@ theorem add_one_le_succ (c : Cardinal.{u}) : c + 1 ≤ succ c := by
     _ ≤ #β := (f.optionElim b hb).cardinal_le
 #align cardinal.add_one_le_succ Cardinal.add_one_le_succ
 
+theorem no_max : ∀ ℵ : Cardinal, ¬ IsMax ℵ := by
+  intro ℵ h
+  unfold IsMax at h; specialize h (le_of_lt $ cantor ℵ)
+  exact not_lt_of_le h (cantor ℵ)
+
+theorem succ_lt : ∀ ℵ : Cardinal, ℵ < succ ℵ := λ ℵ => Order.lt_succ_of_not_isMax (no_max ℵ)
+
 /-- A cardinal is a limit if it is not zero or a successor cardinal. Note that `ℵ₀` is a limit
   cardinal by this definition, but `0` isn't.
 

From f7693cd7b91a1682330ec4d1058c468a1497bcfd Mon Sep 17 00:00:00 2001
From: Ira Fesefeldt <fesefeldt@cs.rwth-aachen.de>
Date: Mon, 11 Dec 2023 11:27:10 +0100
Subject: [PATCH 02/31] line and characters formatting

---
 .../Order/OrdinalApproximantsFixedPoints.lean | 79 +++++++++++--------
 1 file changed, 48 insertions(+), 31 deletions(-)

diff --git a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean b/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
index 79eb771a9f4db..4881e3c9b1497 100644
--- a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
+++ b/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
@@ -13,16 +13,21 @@ import Mathlib.SetTheory.Ordinal.Arithmetic
 /-!
 # Ordinal Approximants for the Fixed points on complete lattices
 
-This file sets up the ordinal approximation theory of fixed points of a monotone function in a complete lattice.
+This file sets up the ordinal approximation theory of fixed points
+of a monotone function in a complete lattice.
 
 ## Main definitions
 
-* `OrdinalApprox.lfp_approx`: The ordinal approximation of the least fixed point of a bundled monotone function.
-* `OrdinalApprox.gfp_approx`: The ordinal approximation of the greatest fixed point of a bundled monotone function.
+* `OrdinalApprox.lfp_approx`: The ordinal approximation of
+  the least fixed point of a bundled monotone function.
+* `OrdinalApprox.gfp_approx`: The ordinal approximation of
+  the greatest fixed point of a bundled monotone function.
 
 ## Main theorems
-* `OrdinalApprox.lfp_is_lfp_approx`: The approximation of the least fixed point eventually reaches the least fixed point
-* `OrdinalApprox.gfp_is_gfp_approx`: The approximation of the greatest fixed point eventually reaches the greatest fixed point
+* `OrdinalApprox.lfp_is_lfp_approx`: The approximation of
+  the least fixed point eventually reaches the least fixed point
+* `OrdinalApprox.gfp_is_gfp_approx`: The approximation of
+  the greatest fixed point eventually reaches the greatest fixed point
 
 ## Tags
 
@@ -42,8 +47,7 @@ def limitation : { i : Ordinal // i < (ord $ succ #α)} → α := λ i => g i
 lemma limitation_eq : ∀ i, limitation g i = g i := by
   intro h; unfold limitation; exact rfl
 
-lemma mk_initialSeg_Subtype (ℵ : Cardinal ):
-  #{ i : Ordinal // i < (ord  ℵ)} = lift.{u+1, u} ℵ := by
+lemma mk_initialSeg_Subtype (ℵ : Cardinal ): #{ i : Ordinal // i < (ord  ℵ)} = lift.{u+1, u} ℵ := by
   simpa using mk_initialSeg (ord ℵ)
 
 lemma limitation_not_injective: ¬ Injective (limitation g) := by
@@ -110,11 +114,11 @@ def lfp_approx_hom : Ordinal.{u} →o α where
   toFun i := lfp_approx f i
   monotone' a b h := by simp; apply lfp_approx_monotone f h
 
-lemma lfp_approx_def (a : Ordinal.{u}): lfp_approx f a = sSup { f (lfp_approx f b) | (b : Ordinal) (_ : b < a) } := by
+lemma lfp_approx_def (a : Ordinal.{u}): lfp_approx f a =
+    sSup { f (lfp_approx f b) | (b : Ordinal) (_ : b < a) } := by
   conv => left; unfold lfp_approx
 
-lemma lfp_approx_addition (a : Ordinal.{u}) :
-  f (lfp_approx f a) = lfp_approx f (a+1) := by
+lemma lfp_approx_addition (a : Ordinal.{u}) : f (lfp_approx f a) = lfp_approx f (a+1) := by
   apply le_antisymm
   . conv => right; rw[lfp_approx_def]
     apply le_sSup; simp
@@ -126,7 +130,7 @@ lemma lfp_approx_addition (a : Ordinal.{u}) :
 
 
 lemma lfp_approx_stabilizing_at_fp (a : Ordinal.{u}) (h: lfp_approx f a ∈ (fixedPoints f)):
-   ∀ b > a, lfp_approx f b = lfp_approx f a := by
+    ∀ b > a, lfp_approx f b = lfp_approx f a := by
   intro b hab; rw[mem_fixedPoints_iff] at h;
   induction b using Ordinal.induction with | h b IH =>
   apply le_antisymm
@@ -165,12 +169,15 @@ lemma lfp_approx_has_cycle : ∃ i < ord $ succ #α, ∃ j < ord $ succ #α,
   . intro h_eq; rw[Subtype.coe_inj] at h_eq; exact h_nab h_eq
   . exact h_fab
 
-lemma lfp_approx_one_fixedPoint (a b : Ordinal.{u}) (h : a < b) (h_fab : lfp_approx f a = lfp_approx f b):
+lemma lfp_approx_one_fixedPoint (a b : Ordinal.{u}) (h : a < b)
+    (h_fab : lfp_approx f a = lfp_approx f b):
     lfp_approx f a ∈ (fixedPoints f) := by
   rw[mem_fixedPoints_iff,lfp_approx_addition]
-  apply Monotone.monotone_stabilizing (lfp_approx f) (lfp_approx_monotone f) h_fab (a+1) (SuccOrder.succ_le_of_lt h) (SuccOrder.le_succ a)
+  apply Monotone.monotone_stabilizing (lfp_approx f) (lfp_approx_monotone f)
+    h_fab (a+1) (SuccOrder.succ_le_of_lt h) (SuccOrder.le_succ a)
 
-lemma lfp_approx_many_fixedPoints (a b : Ordinal.{u}) (h : a < b) (h_fab : lfp_approx f a = lfp_approx f b):
+lemma lfp_approx_many_fixedPoints (a b : Ordinal.{u}) (h : a < b)
+    (h_fab : lfp_approx f a = lfp_approx f b):
     ∀ i ≥ a, lfp_approx f i ∈ (fixedPoints f) := by
   intro i h_i;
   by_cases h_ia : i = a
@@ -183,9 +190,11 @@ lemma lfp_approx_has_fixedPoint_cardinal : lfp_approx f (ord $ succ #α) ∈ (fi
   let ⟨a, h_a, b, h_b, h_nab, h_fab⟩ := lfp_approx_has_cycle f
   cases (le_total a b) with
   | inl h_ab =>
-    exact lfp_approx_many_fixedPoints f a b (Ne.lt_of_le h_nab h_ab) h_fab (ord $ succ #α) (le_of_lt h_a)
+    exact lfp_approx_many_fixedPoints f a b (Ne.lt_of_le h_nab h_ab) h_fab
+      (ord $ succ #α) (le_of_lt h_a)
   | inr h_ba =>
-    exact lfp_approx_many_fixedPoints f b a (Ne.lt_of_le (id (Ne.symm h_nab)) h_ba) (h_fab.symm) (ord $ succ #α) (le_of_lt h_b)
+    exact lfp_approx_many_fixedPoints f b a (Ne.lt_of_le (id (Ne.symm h_nab)) h_ba)
+      (h_fab.symm) (ord $ succ #α) (le_of_lt h_b)
 
 lemma lfp_approx_le_fixedPoint : ∀ a : (fixedPoints f), ∀ i : Ordinal, lfp_approx f i ≤ a := by
   intro ⟨a, h_a⟩ i
@@ -203,12 +212,13 @@ theorem lfp_is_lfp_approx_cardinal : lfp_approx f (ord $ succ #α) = lfp f := by
   . have h_lfp : ∃ x : fixedPoints f, lfp f = x := by use ⊥; exact rfl
     let ⟨x, h_x⟩ := h_lfp; rw[h_x]
     exact lfp_approx_le_fixedPoint f x (ord $ succ #α)
-  . have h_fix : ∃ x: fixedPoints f, lfp_approx f (ord $ succ #α) = x := by {simpa using lfp_approx_has_fixedPoint_cardinal f}
+  . have h_fix : ∃ x: fixedPoints f, lfp_approx f (ord $ succ #α) = x := by
+      simpa using lfp_approx_has_fixedPoint_cardinal f
     let ⟨x, h_x⟩ := h_fix; rw[h_x]
     exact lfp_le_fixed f x.prop
 
-/-- **Constructive Knaster-Tarski Theorem**: Some ordinal approximation of the least fixed point is the least fixed point.
-  Also known as ordinal approximation of the least fixed point.-/
+/-- **Constructive Knaster-Tarski Theorem**: Some ordinal approximation of the least fixed point
+  is the least fixed point. Also known as ordinal approximation of the least fixed point.-/
 theorem lfp_is_lfp_approx : ∃ a : Ordinal, lfp_approx f a = OrderHom.lfp f := by
   use (ord $ succ #α)
   exact lfp_is_lfp_approx_cardinal f
@@ -227,11 +237,11 @@ lemma gfp_approx_antitone : Antitone (gfp_approx f) := by
   use a'; apply And.intro; exact lt_of_lt_of_le h' h
   exact rfl
 
-lemma gfp_approx_def (a : Ordinal.{u}): gfp_approx f a = sInf { f (gfp_approx f b) | (b : Ordinal) (_ : b < a) } := by
+lemma gfp_approx_def (a : Ordinal.{u}): gfp_approx f a =
+    sInf { f (gfp_approx f b) | (b : Ordinal) (_ : b < a) } := by
   conv => left; unfold gfp_approx
 
-lemma gfp_approx_addition (a : Ordinal.{u}) :
-  f (gfp_approx f a) = gfp_approx f (a+1) := by
+lemma gfp_approx_addition (a : Ordinal.{u}) : f (gfp_approx f a) = gfp_approx f (a+1) := by
   apply le_antisymm
   . conv => right; rw[gfp_approx_def]
     apply le_sInf; simp
@@ -243,7 +253,7 @@ lemma gfp_approx_addition (a : Ordinal.{u}) :
 
 
 lemma gfp_approx_stabilizing_at_fp (a : Ordinal.{u}) (h: gfp_approx f a ∈ (fixedPoints f)):
-   ∀ b > a, gfp_approx f b = gfp_approx f a := by
+    ∀ b > a, gfp_approx f b = gfp_approx f a := by
   intro b hab; rw[mem_fixedPoints_iff] at h;
   induction b using Ordinal.induction with | h b IH =>
   apply le_antisymm
@@ -282,12 +292,15 @@ lemma gfp_approx_has_cycle : ∃ i < ord $ succ #α, ∃ j < ord $ succ #α,
   . intro h_eq; rw[Subtype.coe_inj] at h_eq; exact h_nab h_eq
   . exact h_fab
 
-lemma gfp_approx_one_fixedPoint (a b : Ordinal.{u}) (h : a < b) (h_fab : gfp_approx f a = gfp_approx f b):
+lemma gfp_approx_one_fixedPoint (a b : Ordinal.{u}) (h : a < b)
+    (h_fab : gfp_approx f a = gfp_approx f b):
     gfp_approx f a ∈ (fixedPoints f) := by
   rw[mem_fixedPoints_iff,gfp_approx_addition]
-  apply Monotone.antitone_stabilizing (gfp_approx f) (gfp_approx_antitone f) h_fab (a+1) (SuccOrder.succ_le_of_lt h) (SuccOrder.le_succ a)
+  apply Monotone.antitone_stabilizing (gfp_approx f) (gfp_approx_antitone f)
+    h_fab (a+1) (SuccOrder.succ_le_of_lt h) (SuccOrder.le_succ a)
 
-lemma gfp_approx_many_fixedPoints (a b : Ordinal.{u}) (h : a < b) (h_fab : gfp_approx f a = gfp_approx f b):
+lemma gfp_approx_many_fixedPoints (a b : Ordinal.{u}) (h : a < b)
+    (h_fab : gfp_approx f a = gfp_approx f b):
     ∀ i ≥ a, gfp_approx f i ∈ (fixedPoints f) := by
   intro i h_i;
   by_cases h_ia : i = a
@@ -300,9 +313,11 @@ lemma gfp_approx_has_fixedPoint_cardinal : gfp_approx f (ord $ succ #α) ∈ (fi
   let ⟨a, h_a, b, h_b, h_nab, h_fab⟩ := gfp_approx_has_cycle f
   cases (le_total a b) with
   | inl h_ab =>
-    exact gfp_approx_many_fixedPoints f a b (Ne.lt_of_le h_nab h_ab) h_fab (ord $ succ #α) (le_of_lt h_a)
+    exact gfp_approx_many_fixedPoints f a b (Ne.lt_of_le h_nab h_ab)
+      h_fab (ord $ succ #α) (le_of_lt h_a)
   | inr h_ba =>
-    exact gfp_approx_many_fixedPoints f b a (Ne.lt_of_le (id (Ne.symm h_nab)) h_ba) (h_fab.symm) (ord $ succ #α) (le_of_lt h_b)
+    exact gfp_approx_many_fixedPoints f b a (Ne.lt_of_le (id (Ne.symm h_nab)) h_ba)
+      (h_fab.symm) (ord $ succ #α) (le_of_lt h_b)
 
 lemma gfp_approx_ge_fixedPoint : ∀ a : (fixedPoints f), ∀ i : Ordinal, gfp_approx f i ≥ a := by
   intro ⟨a, h_a⟩ i
@@ -318,7 +333,8 @@ lemma gfp_approx_ge_fixedPoint : ∀ a : (fixedPoints f), ∀ i : Ordinal, gfp_a
 
 theorem gfp_is_gfp_approx_cardinal : gfp_approx f (ord $ succ #α) = gfp f := by
   apply le_antisymm
-  . have h_fix : ∃ x: fixedPoints f, gfp_approx f (ord $ succ #α) = x := by {simpa using gfp_approx_has_fixedPoint_cardinal f}
+  . have h_fix : ∃ x: fixedPoints f, gfp_approx f (ord $ succ #α) = x := by
+      simpa using gfp_approx_has_fixedPoint_cardinal f
     let ⟨x, h_x⟩ := h_fix; rw[h_x]
     exact fixed_le_gfp f x.prop
   . have h_lfp : ∃ x : fixedPoints f, gfp f = x := by use ⊤; exact rfl
@@ -326,8 +342,9 @@ theorem gfp_is_gfp_approx_cardinal : gfp_approx f (ord $ succ #α) = gfp f := by
     exact gfp_approx_ge_fixedPoint f x (ord $ succ #α)
 
 
-/-- **Dual Constructive Knaster-Tarski Theorem**: Some ordinal approximation of the greatest fixed point is the greatest fixed point.
-  Also known as ordinal approximation of the greatest fixed point.-/
+/-- **Dual Constructive Knaster-Tarski Theorem**: Some ordinal approximation of
+  the greatest fixed point is the greatest fixed point. Also known as ordinal approximation of
+  the greatest fixed point.-/
 theorem gfp_is_gfp_approx : ∃ a : Ordinal, gfp_approx f a = gfp f := by
   use (ord $ succ #α)
   exact gfp_is_gfp_approx_cardinal f

From d1b3ae440ba9407799d61ba9258588b267b54d04 Mon Sep 17 00:00:00 2001
From: Ira Fesefeldt <fesefeldt@cs.rwth-aachen.de>
Date: Mon, 11 Dec 2023 11:34:45 +0100
Subject: [PATCH 03/31] linter fixes

---
 Mathlib.lean                                  |  1 +
 .../Order/OrdinalApproximantsFixedPoints.lean | 64 +++++++++----------
 2 files changed, 33 insertions(+), 32 deletions(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index 327ff687a1bfb..46c4d232b176b 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2892,6 +2892,7 @@ import Mathlib.Order.Monotone.Union
 import Mathlib.Order.OmegaCompletePartialOrder
 import Mathlib.Order.OrdContinuous
 import Mathlib.Order.OrderIsoNat
+import Mathlib.Order.OrdinalApproximantsFixedPoints
 import Mathlib.Order.PFilter
 import Mathlib.Order.PartialSups
 import Mathlib.Order.Partition.Equipartition
diff --git a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean b/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
index 4881e3c9b1497..128699e072d99 100644
--- a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
+++ b/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
@@ -73,15 +73,15 @@ lemma monotone_stabilizing {a₁ a₂ : α} (h_mon : Monotone f) (h_fa : f a₁
     ∀ i, a₂ ≥ i → i ≥ a₁ → f i = f a₁ := by
   intro i h₂ h₁
   apply le_antisymm
-  . rw[h_fa]; exact h_mon h₂
-  . exact h_mon h₁
+  · rw[h_fa]; exact h_mon h₂
+  · exact h_mon h₁
 
 lemma antitone_stabilizing {a₁ a₂ : α} (h_anti : Antitone f) (h_fa : f a₁ = f a₂):
     ∀ i, a₂ ≥ i → i ≥ a₁ → f i = f a₁ := by
   intro i h₂ h₁
   apply le_antisymm
-  . exact h_anti h₁
-  . rw[h_fa]; exact h_anti h₂
+  · exact h_anti h₁
+  · rw[h_fa]; exact h_anti h₂
 
 end Monotone
 
@@ -120,10 +120,10 @@ lemma lfp_approx_def (a : Ordinal.{u}): lfp_approx f a =
 
 lemma lfp_approx_addition (a : Ordinal.{u}) : f (lfp_approx f a) = lfp_approx f (a+1) := by
   apply le_antisymm
-  . conv => right; rw[lfp_approx_def]
+  · conv => right; rw[lfp_approx_def]
     apply le_sSup; simp
     use a
-  . conv => left; rw[lfp_approx_def]
+  · conv => left; rw[lfp_approx_def]
     apply sSup_le; simp
     intros a' h
     apply f.2; apply lfp_approx_monotone; exact h
@@ -134,18 +134,18 @@ lemma lfp_approx_stabilizing_at_fp (a : Ordinal.{u}) (h: lfp_approx f a ∈ (fix
   intro b hab; rw[mem_fixedPoints_iff] at h;
   induction b using Ordinal.induction with | h b IH =>
   apply le_antisymm
-  . conv => left; rw[lfp_approx_def]
+  · conv => left; rw[lfp_approx_def]
     apply sSup_le; simp
     intro a' ha'b
     by_cases haa : a' < a
-    . rw[lfp_approx_addition]
+    · rw[lfp_approx_addition]
       apply lfp_approx_monotone
       simp; exact haa
-    . simp at haa
+    · simp at haa
       cases (le_iff_lt_or_eq.mp haa) with
       | inl haa => specialize IH a' ha'b haa; rw[IH, h];
       | inr haa => rw[←haa, h];
-  . conv => right; rw[lfp_approx_def]
+  · conv => right; rw[lfp_approx_def]
     apply le_sSup; simp
     use a
 
@@ -166,8 +166,8 @@ lemma lfp_approx_has_cycle : ∃ i < ord $ succ #α, ∃ j < ord $ succ #α,
   use a.val; apply And.intro a.prop;
   use b.val; apply And.intro b.prop;
   apply And.intro
-  . intro h_eq; rw[Subtype.coe_inj] at h_eq; exact h_nab h_eq
-  . exact h_fab
+  · intro h_eq; rw[Subtype.coe_inj] at h_eq; exact h_nab h_eq
+  · exact h_fab
 
 lemma lfp_approx_one_fixedPoint (a b : Ordinal.{u}) (h : a < b)
     (h_fab : lfp_approx f a = lfp_approx f b):
@@ -181,10 +181,10 @@ lemma lfp_approx_many_fixedPoints (a b : Ordinal.{u}) (h : a < b)
     ∀ i ≥ a, lfp_approx f i ∈ (fixedPoints f) := by
   intro i h_i;
   by_cases h_ia : i = a
-  . rw[h_ia]; exact lfp_approx_one_fixedPoint f a b h h_fab
-  . apply lfp_approx_eq_fp f a
-    . exact lfp_approx_one_fixedPoint f a b h h_fab
-    . exact Ne.lt_of_le' h_ia h_i
+  · rw[h_ia]; exact lfp_approx_one_fixedPoint f a b h h_fab
+  · apply lfp_approx_eq_fp f a
+    · exact lfp_approx_one_fixedPoint f a b h h_fab
+    · exact Ne.lt_of_le' h_ia h_i
 
 lemma lfp_approx_has_fixedPoint_cardinal : lfp_approx f (ord $ succ #α) ∈ (fixedPoints f) := by
   let ⟨a, h_a, b, h_b, h_nab, h_fab⟩ := lfp_approx_has_cycle f
@@ -209,10 +209,10 @@ lemma lfp_approx_le_fixedPoint : ∀ a : (fixedPoints f), ∀ i : Ordinal, lfp_a
 
 theorem lfp_is_lfp_approx_cardinal : lfp_approx f (ord $ succ #α) = lfp f := by
   apply le_antisymm
-  . have h_lfp : ∃ x : fixedPoints f, lfp f = x := by use ⊥; exact rfl
+  · have h_lfp : ∃ x : fixedPoints f, lfp f = x := by use ⊥; exact rfl
     let ⟨x, h_x⟩ := h_lfp; rw[h_x]
     exact lfp_approx_le_fixedPoint f x (ord $ succ #α)
-  . have h_fix : ∃ x: fixedPoints f, lfp_approx f (ord $ succ #α) = x := by
+  · have h_fix : ∃ x: fixedPoints f, lfp_approx f (ord $ succ #α) = x := by
       simpa using lfp_approx_has_fixedPoint_cardinal f
     let ⟨x, h_x⟩ := h_fix; rw[h_x]
     exact lfp_le_fixed f x.prop
@@ -243,11 +243,11 @@ lemma gfp_approx_def (a : Ordinal.{u}): gfp_approx f a =
 
 lemma gfp_approx_addition (a : Ordinal.{u}) : f (gfp_approx f a) = gfp_approx f (a+1) := by
   apply le_antisymm
-  . conv => right; rw[gfp_approx_def]
+  · conv => right; rw[gfp_approx_def]
     apply le_sInf; simp
     intros a' h
     apply f.2; apply gfp_approx_antitone; exact h
-  . conv => left; rw[gfp_approx_def]
+  · conv => left; rw[gfp_approx_def]
     apply sInf_le; simp
     use a
 
@@ -257,17 +257,17 @@ lemma gfp_approx_stabilizing_at_fp (a : Ordinal.{u}) (h: gfp_approx f a ∈ (fix
   intro b hab; rw[mem_fixedPoints_iff] at h;
   induction b using Ordinal.induction with | h b IH =>
   apply le_antisymm
-  . conv => left; rw[gfp_approx_def]
+  · conv => left; rw[gfp_approx_def]
     apply sInf_le
     use a
-  . conv => right; rw[gfp_approx_def]
+  · conv => right; rw[gfp_approx_def]
     apply le_sInf; simp
     intro a' ha'b
     by_cases haa : a' < a
-    . rw[gfp_approx_addition]
+    · rw[gfp_approx_addition]
       apply gfp_approx_antitone
       simp; exact haa
-    . simp at haa
+    · simp at haa
       cases (le_iff_lt_or_eq.mp haa) with
       | inl haa => specialize IH a' ha'b haa; rw[IH, h];
       | inr haa => rw[←haa, h];
@@ -289,8 +289,8 @@ lemma gfp_approx_has_cycle : ∃ i < ord $ succ #α, ∃ j < ord $ succ #α,
   use a.val; apply And.intro a.prop;
   use b.val; apply And.intro b.prop;
   apply And.intro
-  . intro h_eq; rw[Subtype.coe_inj] at h_eq; exact h_nab h_eq
-  . exact h_fab
+  · intro h_eq; rw[Subtype.coe_inj] at h_eq; exact h_nab h_eq
+  · exact h_fab
 
 lemma gfp_approx_one_fixedPoint (a b : Ordinal.{u}) (h : a < b)
     (h_fab : gfp_approx f a = gfp_approx f b):
@@ -304,10 +304,10 @@ lemma gfp_approx_many_fixedPoints (a b : Ordinal.{u}) (h : a < b)
     ∀ i ≥ a, gfp_approx f i ∈ (fixedPoints f) := by
   intro i h_i;
   by_cases h_ia : i = a
-  . rw[h_ia]; exact gfp_approx_one_fixedPoint f a b h h_fab
-  . apply gfp_approx_eq_fp f a
-    . exact gfp_approx_one_fixedPoint f a b h h_fab
-    . exact Ne.lt_of_le' h_ia h_i
+  · rw[h_ia]; exact gfp_approx_one_fixedPoint f a b h h_fab
+  · apply gfp_approx_eq_fp f a
+    · exact gfp_approx_one_fixedPoint f a b h h_fab
+    · exact Ne.lt_of_le' h_ia h_i
 
 lemma gfp_approx_has_fixedPoint_cardinal : gfp_approx f (ord $ succ #α) ∈ (fixedPoints f) := by
   let ⟨a, h_a, b, h_b, h_nab, h_fab⟩ := gfp_approx_has_cycle f
@@ -333,11 +333,11 @@ lemma gfp_approx_ge_fixedPoint : ∀ a : (fixedPoints f), ∀ i : Ordinal, gfp_a
 
 theorem gfp_is_gfp_approx_cardinal : gfp_approx f (ord $ succ #α) = gfp f := by
   apply le_antisymm
-  . have h_fix : ∃ x: fixedPoints f, gfp_approx f (ord $ succ #α) = x := by
+  · have h_fix : ∃ x: fixedPoints f, gfp_approx f (ord $ succ #α) = x := by
       simpa using gfp_approx_has_fixedPoint_cardinal f
     let ⟨x, h_x⟩ := h_fix; rw[h_x]
     exact fixed_le_gfp f x.prop
-  . have h_lfp : ∃ x : fixedPoints f, gfp f = x := by use ⊤; exact rfl
+  · have h_lfp : ∃ x : fixedPoints f, gfp f = x := by use ⊤; exact rfl
     let ⟨x, h_x⟩ := h_lfp; rw[h_x]
     exact gfp_approx_ge_fixedPoint f x (ord $ succ #α)
 

From 8ff8b17e360202997975842f2d658f6e2aee42d8 Mon Sep 17 00:00:00 2001
From: Ira Fesefeldt <fesefeldt@cs.rwth-aachen.de>
Date: Mon, 11 Dec 2023 12:30:04 +0100
Subject: [PATCH 04/31] deactivate unusredVariables linting

---
 Mathlib/Order/OrdinalApproximantsFixedPoints.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean b/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
index 128699e072d99..74107e80fc4a3 100644
--- a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
+++ b/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
@@ -98,6 +98,7 @@ variable [CompleteLattice α] (f : α →o α)
 open Function fixedPoints Cardinal Order OrderHom
 
 /- Ordinal approximants of the least fixed points -/
+set_option linter.unusedVariables false in
 def lfp_approx (a : Ordinal.{u}) : α :=
   sSup { f (lfp_approx b) | (b : Ordinal) (h : b < a) }
 termination_by lfp_approx a => a
@@ -225,6 +226,7 @@ theorem lfp_is_lfp_approx : ∃ a : Ordinal, lfp_approx f a = OrderHom.lfp f :=
 
 
 /- Ordinal approximants of the least fixed points -/
+set_option linter.unusedVariables false in
 def gfp_approx (a : Ordinal.{u}) : α :=
   sInf { f (gfp_approx b) | (b : Ordinal) (h : b < a) }
 termination_by gfp_approx a => a

From 752d401557ad8020a6f836f4fb1e9480f4bb5c97 Mon Sep 17 00:00:00 2001
From: Ira Fesefeldt <fesefeldt@cs.rwth-aachen.de>
Date: Mon, 11 Dec 2023 14:29:30 +0100
Subject: [PATCH 05/31] made some lemmas to theorems

---
 .../Order/OrdinalApproximantsFixedPoints.lean | 60 ++++++++-----------
 1 file changed, 26 insertions(+), 34 deletions(-)

diff --git a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean b/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
index 74107e80fc4a3..b6dcb0c29d714 100644
--- a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
+++ b/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
@@ -44,13 +44,13 @@ open Cardinal Ordinal SuccOrder Function
 
 def limitation : { i : Ordinal // i < (ord $ succ #α)} → α := λ i => g i
 
-lemma limitation_eq : ∀ i, limitation g i = g i := by
+theorem limitation_def : ∀ i, limitation g i = g i := by
   intro h; unfold limitation; exact rfl
 
 lemma mk_initialSeg_Subtype (ℵ : Cardinal ): #{ i : Ordinal // i < (ord  ℵ)} = lift.{u+1, u} ℵ := by
   simpa using mk_initialSeg (ord ℵ)
 
-lemma limitation_not_injective: ¬ Injective (limitation g) := by
+theorem limitation_not_injective: ¬ Injective (limitation g) := by
   intro h_inj
   have h₁ := by apply lift_mk_le_lift_mk_of_injective h_inj;
   rw[mk_initialSeg_Subtype (succ #α), Cardinal.lift_lift, Cardinal.lift_le] at h₁
@@ -69,14 +69,14 @@ variable {α : Type u}
 variable {β : Type v}
 variable [Preorder α] [PartialOrder β] (f: α → β)
 
-lemma monotone_stabilizing {a₁ a₂ : α} (h_mon : Monotone f) (h_fa : f a₁ = f a₂):
+theorem monotone_stabilizing {a₁ a₂ : α} (h_mon : Monotone f) (h_fa : f a₁ = f a₂):
     ∀ i, a₂ ≥ i → i ≥ a₁ → f i = f a₁ := by
   intro i h₂ h₁
   apply le_antisymm
   · rw[h_fa]; exact h_mon h₂
   · exact h_mon h₁
 
-lemma antitone_stabilizing {a₁ a₂ : α} (h_anti : Antitone f) (h_fa : f a₁ = f a₂):
+theorem antitone_stabilizing {a₁ a₂ : α} (h_anti : Antitone f) (h_fa : f a₁ = f a₂):
     ∀ i, a₂ ≥ i → i ≥ a₁ → f i = f a₁ := by
   intro i h₂ h₁
   apply le_antisymm
@@ -104,7 +104,7 @@ def lfp_approx (a : Ordinal.{u}) : α :=
 termination_by lfp_approx a => a
 decreasing_by exact h
 
-lemma lfp_approx_monotone : Monotone (lfp_approx f) := by
+theorem lfp_approx_monotone : Monotone (lfp_approx f) := by
   unfold Monotone; intros a b h; unfold lfp_approx
   refine sSup_le_sSup ?h; simp
   intros a' h'
@@ -115,27 +115,23 @@ def lfp_approx_hom : Ordinal.{u} →o α where
   toFun i := lfp_approx f i
   monotone' a b h := by simp; apply lfp_approx_monotone f h
 
-lemma lfp_approx_def (a : Ordinal.{u}): lfp_approx f a =
-    sSup { f (lfp_approx f b) | (b : Ordinal) (_ : b < a) } := by
-  conv => left; unfold lfp_approx
-
-lemma lfp_approx_addition (a : Ordinal.{u}) : f (lfp_approx f a) = lfp_approx f (a+1) := by
+theorem lfp_approx_addition (a : Ordinal.{u}) : f (lfp_approx f a) = lfp_approx f (a+1) := by
   apply le_antisymm
-  · conv => right; rw[lfp_approx_def]
+  · conv => right; unfold lfp_approx
     apply le_sSup; simp
     use a
-  · conv => left; rw[lfp_approx_def]
+  · conv => left; unfold lfp_approx
     apply sSup_le; simp
     intros a' h
     apply f.2; apply lfp_approx_monotone; exact h
 
 
-lemma lfp_approx_stabilizing_at_fp (a : Ordinal.{u}) (h: lfp_approx f a ∈ (fixedPoints f)):
+theorem lfp_approx_stabilizing_at_fp (a : Ordinal.{u}) (h: lfp_approx f a ∈ (fixedPoints f)):
     ∀ b > a, lfp_approx f b = lfp_approx f a := by
   intro b hab; rw[mem_fixedPoints_iff] at h;
   induction b using Ordinal.induction with | h b IH =>
   apply le_antisymm
-  · conv => left; rw[lfp_approx_def]
+  · conv => left; unfold lfp_approx
     apply sSup_le; simp
     intro a' ha'b
     by_cases haa : a' < a
@@ -146,11 +142,11 @@ lemma lfp_approx_stabilizing_at_fp (a : Ordinal.{u}) (h: lfp_approx f a ∈ (fix
       cases (le_iff_lt_or_eq.mp haa) with
       | inl haa => specialize IH a' ha'b haa; rw[IH, h];
       | inr haa => rw[←haa, h];
-  · conv => right; rw[lfp_approx_def]
+  · conv => right; unfold lfp_approx
     apply le_sSup; simp
     use a
 
-lemma lfp_approx_eq_fp (a : Ordinal.{u}) (h: lfp_approx f a ∈ (fixedPoints f)):
+theorem lfp_approx_eq_fp (a : Ordinal.{u}) (h: lfp_approx f a ∈ (fixedPoints f)):
     ∀ b > a, lfp_approx f b ∈ (fixedPoints f)  := by
   intro b h_ab;
   rw[mem_fixedPoints_iff]
@@ -159,11 +155,11 @@ lemma lfp_approx_eq_fp (a : Ordinal.{u}) (h: lfp_approx f a ∈ (fixedPoints f))
   exact mem_fixedPoints_iff.mp h
 
 
-lemma lfp_approx_has_cycle : ∃ i < ord $ succ #α, ∃ j < ord $ succ #α,
+theorem lfp_approx_has_cycle : ∃ i < ord $ succ #α, ∃ j < ord $ succ #α,
     i ≠ j ∧ lfp_approx f i = lfp_approx f j := by
   have h_ninj := Function.Injective.not_exists_equal (limitation_not_injective $ lfp_approx f)
   let ⟨a, b, h_nab, h_fab⟩ := h_ninj
-  rw[limitation_eq, limitation_eq] at h_fab
+  rw[limitation_def, limitation_def] at h_fab
   use a.val; apply And.intro a.prop;
   use b.val; apply And.intro b.prop;
   apply And.intro
@@ -201,7 +197,7 @@ lemma lfp_approx_le_fixedPoint : ∀ a : (fixedPoints f), ∀ i : Ordinal, lfp_a
   intro ⟨a, h_a⟩ i
   induction i using Ordinal.induction with
   | h i IH =>
-    rw[lfp_approx_def]
+    unfold lfp_approx
     apply sSup_le; simp
     intro j h_j
     rw[←h_a]
@@ -232,37 +228,33 @@ def gfp_approx (a : Ordinal.{u}) : α :=
 termination_by gfp_approx a => a
 decreasing_by exact h
 
-lemma gfp_approx_antitone : Antitone (gfp_approx f) := by
+theorem gfp_approx_antitone : Antitone (gfp_approx f) := by
   unfold Antitone; intros a b h; unfold gfp_approx
   refine sInf_le_sInf ?h; simp
   intros a' h'
   use a'; apply And.intro; exact lt_of_lt_of_le h' h
   exact rfl
 
-lemma gfp_approx_def (a : Ordinal.{u}): gfp_approx f a =
-    sInf { f (gfp_approx f b) | (b : Ordinal) (_ : b < a) } := by
-  conv => left; unfold gfp_approx
-
-lemma gfp_approx_addition (a : Ordinal.{u}) : f (gfp_approx f a) = gfp_approx f (a+1) := by
+theorem gfp_approx_addition (a : Ordinal.{u}) : f (gfp_approx f a) = gfp_approx f (a+1) := by
   apply le_antisymm
-  · conv => right; rw[gfp_approx_def]
+  · conv => right; unfold gfp_approx
     apply le_sInf; simp
     intros a' h
     apply f.2; apply gfp_approx_antitone; exact h
-  · conv => left; rw[gfp_approx_def]
+  · conv => left; unfold gfp_approx
     apply sInf_le; simp
     use a
 
 
-lemma gfp_approx_stabilizing_at_fp (a : Ordinal.{u}) (h: gfp_approx f a ∈ (fixedPoints f)):
+theorem gfp_approx_stabilizing_at_fp (a : Ordinal.{u}) (h: gfp_approx f a ∈ (fixedPoints f)):
     ∀ b > a, gfp_approx f b = gfp_approx f a := by
   intro b hab; rw[mem_fixedPoints_iff] at h;
   induction b using Ordinal.induction with | h b IH =>
   apply le_antisymm
-  · conv => left; rw[gfp_approx_def]
+  · conv => left; unfold gfp_approx
     apply sInf_le
     use a
-  · conv => right; rw[gfp_approx_def]
+  · conv => right; unfold gfp_approx
     apply le_sInf; simp
     intro a' ha'b
     by_cases haa : a' < a
@@ -274,7 +266,7 @@ lemma gfp_approx_stabilizing_at_fp (a : Ordinal.{u}) (h: gfp_approx f a ∈ (fix
       | inl haa => specialize IH a' ha'b haa; rw[IH, h];
       | inr haa => rw[←haa, h];
 
-lemma gfp_approx_eq_fp (a : Ordinal.{u}) (h: gfp_approx f a ∈ (fixedPoints f)):
+theorem gfp_approx_eq_fp (a : Ordinal.{u}) (h: gfp_approx f a ∈ (fixedPoints f)):
     ∀ b > a, gfp_approx f b ∈ (fixedPoints f)  := by
   intro b h_ab;
   rw[mem_fixedPoints_iff]
@@ -283,11 +275,11 @@ lemma gfp_approx_eq_fp (a : Ordinal.{u}) (h: gfp_approx f a ∈ (fixedPoints f))
   exact mem_fixedPoints_iff.mp h
 
 
-lemma gfp_approx_has_cycle : ∃ i < ord $ succ #α, ∃ j < ord $ succ #α,
+theorem gfp_approx_has_cycle : ∃ i < ord $ succ #α, ∃ j < ord $ succ #α,
     i ≠ j ∧ gfp_approx f i = gfp_approx f j := by
   have h_ninj := Function.Injective.not_exists_equal (limitation_not_injective $ gfp_approx f)
   let ⟨a, b, h_nab, h_fab⟩ := h_ninj
-  rw[limitation_eq, limitation_eq] at h_fab
+  rw[limitation_def, limitation_def] at h_fab
   use a.val; apply And.intro a.prop;
   use b.val; apply And.intro b.prop;
   apply And.intro
@@ -325,7 +317,7 @@ lemma gfp_approx_ge_fixedPoint : ∀ a : (fixedPoints f), ∀ i : Ordinal, gfp_a
   intro ⟨a, h_a⟩ i
   induction i using Ordinal.induction with
   | h i IH =>
-    rw[gfp_approx_def]
+    unfold gfp_approx
     apply le_sInf; simp
     intro j h_j
     rw[←h_a]

From a1ef93a56d6922b631ac3a04e99b3df9d1ade84d Mon Sep 17 00:00:00 2001
From: Ira Fesefeldt <fesefeldt@cs.rwth-aachen.de>
Date: Mon, 11 Dec 2023 16:16:30 +0100
Subject: [PATCH 06/31] documentation and formatting

---
 .../Order/OrdinalApproximantsFixedPoints.lean | 65 ++++++++++++-------
 1 file changed, 42 insertions(+), 23 deletions(-)

diff --git a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean b/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
index b6dcb0c29d714..d32dc35bc8cc9 100644
--- a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
+++ b/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
@@ -42,6 +42,7 @@ variable (g: Ordinal → α)
 
 open Cardinal Ordinal SuccOrder Function
 
+/-- Limiation of an ordinal defined function to an initial segment -/
 def limitation : { i : Ordinal // i < (ord $ succ #α)} → α := λ i => g i
 
 theorem limitation_def : ∀ i, limitation g i = g i := by
@@ -69,6 +70,7 @@ variable {α : Type u}
 variable {β : Type v}
 variable [Preorder α] [PartialOrder β] (f: α → β)
 
+/-- If a monotone function is equal at two points, it is equal between all of them -/
 theorem monotone_stabilizing {a₁ a₂ : α} (h_mon : Monotone f) (h_fa : f a₁ = f a₂):
     ∀ i, a₂ ≥ i → i ≥ a₁ → f i = f a₁ := by
   intro i h₂ h₁
@@ -76,6 +78,7 @@ theorem monotone_stabilizing {a₁ a₂ : α} (h_mon : Monotone f) (h_fa : f a
   · rw[h_fa]; exact h_mon h₂
   · exact h_mon h₁
 
+/-- If an antitone function is equal at two points, it is equal between all of them -/
 theorem antitone_stabilizing {a₁ a₂ : α} (h_anti : Antitone f) (h_fa : f a₁ = f a₂):
     ∀ i, a₂ ≥ i → i ≥ a₁ → f i = f a₁ := by
   intro i h₂ h₁
@@ -97,8 +100,8 @@ variable [CompleteLattice α] (f : α →o α)
 
 open Function fixedPoints Cardinal Order OrderHom
 
-/- Ordinal approximants of the least fixed points -/
 set_option linter.unusedVariables false in
+/-- Ordinal approximants of the least fixed points -/
 def lfp_approx (a : Ordinal.{u}) : α :=
   sSup { f (lfp_approx b) | (b : Ordinal) (h : b < a) }
 termination_by lfp_approx a => a
@@ -111,6 +114,7 @@ theorem lfp_approx_monotone : Monotone (lfp_approx f) := by
   use a'; apply And.intro; exact lt_of_lt_of_le h' h
   exact rfl
 
+/-- Ordinal approximants of the least fixed points as an order homomorphism -/
 def lfp_approx_hom : Ordinal.{u} →o α where
   toFun i := lfp_approx f i
   monotone' a b h := by simp; apply lfp_approx_monotone f h
@@ -125,7 +129,8 @@ theorem lfp_approx_addition (a : Ordinal.{u}) : f (lfp_approx f a) = lfp_approx
     intros a' h
     apply f.2; apply lfp_approx_monotone; exact h
 
-
+/-- The ordinal approximants of the least fixed points are stabilizing
+  when reaching a fixed point of f -/
 theorem lfp_approx_stabilizing_at_fp (a : Ordinal.{u}) (h: lfp_approx f a ∈ (fixedPoints f)):
     ∀ b > a, lfp_approx f b = lfp_approx f a := by
   intro b hab; rw[mem_fixedPoints_iff] at h;
@@ -141,11 +146,12 @@ theorem lfp_approx_stabilizing_at_fp (a : Ordinal.{u}) (h: lfp_approx f a ∈ (f
     · simp at haa
       cases (le_iff_lt_or_eq.mp haa) with
       | inl haa => specialize IH a' ha'b haa; rw[IH, h];
-      | inr haa => rw[←haa, h];
+      | inr haa => rw[← haa, h];
   · conv => right; unfold lfp_approx
     apply le_sSup; simp
     use a
 
+/-- Every value after a fixed point of f is also a fixed point of f -/
 theorem lfp_approx_eq_fp (a : Ordinal.{u}) (h: lfp_approx f a ∈ (fixedPoints f)):
     ∀ b > a, lfp_approx f b ∈ (fixedPoints f)  := by
   intro b h_ab;
@@ -154,8 +160,8 @@ theorem lfp_approx_eq_fp (a : Ordinal.{u}) (h: lfp_approx f a ∈ (fixedPoints f
   rw[h_stab]
   exact mem_fixedPoints_iff.mp h
 
-
-theorem lfp_approx_has_cycle : ∃ i < ord $ succ #α, ∃ j < ord $ succ #α,
+/-- There are ordinals smaller than the successor of the domains cardinals with equal value -/
+theorem lfp_approx_equal_value : ∃ i < ord $ succ #α, ∃ j < ord $ succ #α,
     i ≠ j ∧ lfp_approx f i = lfp_approx f j := by
   have h_ninj := Function.Injective.not_exists_equal (limitation_not_injective $ lfp_approx f)
   let ⟨a, b, h_nab, h_fab⟩ := h_ninj
@@ -166,6 +172,7 @@ theorem lfp_approx_has_cycle : ∃ i < ord $ succ #α, ∃ j < ord $ succ #α,
   · intro h_eq; rw[Subtype.coe_inj] at h_eq; exact h_nab h_eq
   · exact h_fab
 
+/-- If there are ordinals with equal value then the values are fixed points of f -/
 lemma lfp_approx_one_fixedPoint (a b : Ordinal.{u}) (h : a < b)
     (h_fab : lfp_approx f a = lfp_approx f b):
     lfp_approx f a ∈ (fixedPoints f) := by
@@ -173,6 +180,8 @@ lemma lfp_approx_one_fixedPoint (a b : Ordinal.{u}) (h : a < b)
   apply Monotone.monotone_stabilizing (lfp_approx f) (lfp_approx_monotone f)
     h_fab (a+1) (SuccOrder.succ_le_of_lt h) (SuccOrder.le_succ a)
 
+/-- If there are ordinals with equal value then
+  every value follwing the smaller ordinal are fixed points of -/
 lemma lfp_approx_many_fixedPoints (a b : Ordinal.{u}) (h : a < b)
     (h_fab : lfp_approx f a = lfp_approx f b):
     ∀ i ≥ a, lfp_approx f i ∈ (fixedPoints f) := by
@@ -183,8 +192,9 @@ lemma lfp_approx_many_fixedPoints (a b : Ordinal.{u}) (h : a < b)
     · exact lfp_approx_one_fixedPoint f a b h h_fab
     · exact Ne.lt_of_le' h_ia h_i
 
-lemma lfp_approx_has_fixedPoint_cardinal : lfp_approx f (ord $ succ #α) ∈ (fixedPoints f) := by
-  let ⟨a, h_a, b, h_b, h_nab, h_fab⟩ := lfp_approx_has_cycle f
+/-- A fixed point of f is reached after the successor of the domains cardinality -/
+theorem lfp_approx_has_fixedPoint_cardinal : lfp_approx f (ord $ succ #α) ∈ (fixedPoints f) := by
+  let ⟨a, h_a, b, h_b, h_nab, h_fab⟩ := lfp_approx_equal_value f
   cases (le_total a b) with
   | inl h_ab =>
     exact lfp_approx_many_fixedPoints f a b (Ne.lt_of_le h_nab h_ab) h_fab
@@ -193,18 +203,20 @@ lemma lfp_approx_has_fixedPoint_cardinal : lfp_approx f (ord $ succ #α) ∈ (fi
     exact lfp_approx_many_fixedPoints f b a (Ne.lt_of_le (id (Ne.symm h_nab)) h_ba)
       (h_fab.symm) (ord $ succ #α) (le_of_lt h_b)
 
-lemma lfp_approx_le_fixedPoint : ∀ a : (fixedPoints f), ∀ i : Ordinal, lfp_approx f i ≤ a := by
+/-- Every value of the ordinal approximants are less or equal than every fixed point of f -/
+theorem lfp_approx_le_fixedPoint : ∀ a : (fixedPoints f), ∀ i : Ordinal, lfp_approx f i ≤ a := by
   intro ⟨a, h_a⟩ i
   induction i using Ordinal.induction with
   | h i IH =>
     unfold lfp_approx
     apply sSup_le; simp
     intro j h_j
-    rw[←h_a]
+    rw[← h_a]
     apply f.monotone'
     exact IH j h_j
 
-theorem lfp_is_lfp_approx_cardinal : lfp_approx f (ord $ succ #α) = lfp f := by
+/-- The least fixed point of f is reached after the successor of the domains cardinality -/
+theorem lfp_approx_cardinal_is_lfp : lfp_approx f (ord $ succ #α) = lfp f := by
   apply le_antisymm
   · have h_lfp : ∃ x : fixedPoints f, lfp f = x := by use ⊥; exact rfl
     let ⟨x, h_x⟩ := h_lfp; rw[h_x]
@@ -216,13 +228,13 @@ theorem lfp_is_lfp_approx_cardinal : lfp_approx f (ord $ succ #α) = lfp f := by
 
 /-- **Constructive Knaster-Tarski Theorem**: Some ordinal approximation of the least fixed point
   is the least fixed point. Also known as ordinal approximation of the least fixed point.-/
-theorem lfp_is_lfp_approx : ∃ a : Ordinal, lfp_approx f a = OrderHom.lfp f := by
+theorem lfp_approx_is_lfp : ∃ a : Ordinal, lfp_approx f a = lfp f := by
   use (ord $ succ #α)
-  exact lfp_is_lfp_approx_cardinal f
+  exact lfp_approx_cardinal_is_lfp f
 
 
-/- Ordinal approximants of the least fixed points -/
 set_option linter.unusedVariables false in
+/-- Ordinal approximants of the least fixed points -/
 def gfp_approx (a : Ordinal.{u}) : α :=
   sInf { f (gfp_approx b) | (b : Ordinal) (h : b < a) }
 termination_by gfp_approx a => a
@@ -245,7 +257,8 @@ theorem gfp_approx_addition (a : Ordinal.{u}) : f (gfp_approx f a) = gfp_approx
     apply sInf_le; simp
     use a
 
-
+/-- The ordinal approximants of the least fixed points are stabilizing
+  when reaching a fixed point of f -/
 theorem gfp_approx_stabilizing_at_fp (a : Ordinal.{u}) (h: gfp_approx f a ∈ (fixedPoints f)):
     ∀ b > a, gfp_approx f b = gfp_approx f a := by
   intro b hab; rw[mem_fixedPoints_iff] at h;
@@ -264,8 +277,9 @@ theorem gfp_approx_stabilizing_at_fp (a : Ordinal.{u}) (h: gfp_approx f a ∈ (f
     · simp at haa
       cases (le_iff_lt_or_eq.mp haa) with
       | inl haa => specialize IH a' ha'b haa; rw[IH, h];
-      | inr haa => rw[←haa, h];
+      | inr haa => rw[← haa, h];
 
+/-- Every value after a fixed point of f is also a fixed point of f -/
 theorem gfp_approx_eq_fp (a : Ordinal.{u}) (h: gfp_approx f a ∈ (fixedPoints f)):
     ∀ b > a, gfp_approx f b ∈ (fixedPoints f)  := by
   intro b h_ab;
@@ -274,8 +288,8 @@ theorem gfp_approx_eq_fp (a : Ordinal.{u}) (h: gfp_approx f a ∈ (fixedPoints f
   rw[h_stab]
   exact mem_fixedPoints_iff.mp h
 
-
-theorem gfp_approx_has_cycle : ∃ i < ord $ succ #α, ∃ j < ord $ succ #α,
+/-- There are ordinals smaller than the successor of the domains cardinals with equal value -/
+theorem gfp_approx_equal_value : ∃ i < ord $ succ #α, ∃ j < ord $ succ #α,
     i ≠ j ∧ gfp_approx f i = gfp_approx f j := by
   have h_ninj := Function.Injective.not_exists_equal (limitation_not_injective $ gfp_approx f)
   let ⟨a, b, h_nab, h_fab⟩ := h_ninj
@@ -286,6 +300,7 @@ theorem gfp_approx_has_cycle : ∃ i < ord $ succ #α, ∃ j < ord $ succ #α,
   · intro h_eq; rw[Subtype.coe_inj] at h_eq; exact h_nab h_eq
   · exact h_fab
 
+/-- If there are ordinals with equal value then the values are fixed points of f -/
 lemma gfp_approx_one_fixedPoint (a b : Ordinal.{u}) (h : a < b)
     (h_fab : gfp_approx f a = gfp_approx f b):
     gfp_approx f a ∈ (fixedPoints f) := by
@@ -293,6 +308,8 @@ lemma gfp_approx_one_fixedPoint (a b : Ordinal.{u}) (h : a < b)
   apply Monotone.antitone_stabilizing (gfp_approx f) (gfp_approx_antitone f)
     h_fab (a+1) (SuccOrder.succ_le_of_lt h) (SuccOrder.le_succ a)
 
+/-- If there are ordinals with equal value then
+  every value follwing the smaller ordinal are fixed points of -/
 lemma gfp_approx_many_fixedPoints (a b : Ordinal.{u}) (h : a < b)
     (h_fab : gfp_approx f a = gfp_approx f b):
     ∀ i ≥ a, gfp_approx f i ∈ (fixedPoints f) := by
@@ -303,8 +320,9 @@ lemma gfp_approx_many_fixedPoints (a b : Ordinal.{u}) (h : a < b)
     · exact gfp_approx_one_fixedPoint f a b h h_fab
     · exact Ne.lt_of_le' h_ia h_i
 
+/-- A fixed point of f is reached after the successor of the domains cardinality -/
 lemma gfp_approx_has_fixedPoint_cardinal : gfp_approx f (ord $ succ #α) ∈ (fixedPoints f) := by
-  let ⟨a, h_a, b, h_b, h_nab, h_fab⟩ := gfp_approx_has_cycle f
+  let ⟨a, h_a, b, h_b, h_nab, h_fab⟩ := gfp_approx_equal_value f
   cases (le_total a b) with
   | inl h_ab =>
     exact gfp_approx_many_fixedPoints f a b (Ne.lt_of_le h_nab h_ab)
@@ -313,6 +331,7 @@ lemma gfp_approx_has_fixedPoint_cardinal : gfp_approx f (ord $ succ #α) ∈ (fi
     exact gfp_approx_many_fixedPoints f b a (Ne.lt_of_le (id (Ne.symm h_nab)) h_ba)
       (h_fab.symm) (ord $ succ #α) (le_of_lt h_b)
 
+/-- Every value of the ordinal approximants are greater or equal than every fixed point of f -/
 lemma gfp_approx_ge_fixedPoint : ∀ a : (fixedPoints f), ∀ i : Ordinal, gfp_approx f i ≥ a := by
   intro ⟨a, h_a⟩ i
   induction i using Ordinal.induction with
@@ -320,12 +339,12 @@ lemma gfp_approx_ge_fixedPoint : ∀ a : (fixedPoints f), ∀ i : Ordinal, gfp_a
     unfold gfp_approx
     apply le_sInf; simp
     intro j h_j
-    rw[←h_a]
+    rw[← h_a]
     apply f.monotone'
     exact IH j h_j
 
-
-theorem gfp_is_gfp_approx_cardinal : gfp_approx f (ord $ succ #α) = gfp f := by
+/-- The greatest fixed point of f is reached after the successor of the domains cardinality -/
+theorem gfp_approx_cardinal_is_gfp : gfp_approx f (ord $ succ #α) = gfp f := by
   apply le_antisymm
   · have h_fix : ∃ x: fixedPoints f, gfp_approx f (ord $ succ #α) = x := by
       simpa using gfp_approx_has_fixedPoint_cardinal f
@@ -339,8 +358,8 @@ theorem gfp_is_gfp_approx_cardinal : gfp_approx f (ord $ succ #α) = gfp f := by
 /-- **Dual Constructive Knaster-Tarski Theorem**: Some ordinal approximation of
   the greatest fixed point is the greatest fixed point. Also known as ordinal approximation of
   the greatest fixed point.-/
-theorem gfp_is_gfp_approx : ∃ a : Ordinal, gfp_approx f a = gfp f := by
+theorem gfp_approx_is_gfp : ∃ a : Ordinal, gfp_approx f a = gfp f := by
   use (ord $ succ #α)
-  exact gfp_is_gfp_approx_cardinal f
+  exact gfp_approx_cardinal_is_gfp f
 
 end OrdinalApprox

From 645df6714908587fcff9be2d42f12e64f3f7959f Mon Sep 17 00:00:00 2001
From: Ira Fesefeldt <fesefeldt@cs.rwth-aachen.de>
Date: Sat, 2 Mar 2024 15:34:45 +0100
Subject: [PATCH 07/31] review changes

---
 Mathlib/Logic/Function/Basic.lean             |   4 +-
 Mathlib/Order/Monotone/Basic.lean             |  16 +
 .../Order/OrdinalApproximantsFixedPoints.lean | 309 ++++++------------
 Mathlib/SetTheory/Cardinal/Basic.lean         |   9 +-
 docs/references.bib                           |  21 ++
 5 files changed, 142 insertions(+), 217 deletions(-)

diff --git a/Mathlib/Logic/Function/Basic.lean b/Mathlib/Logic/Function/Basic.lean
index 49195a1dd9c0e..8b79f8c3e516a 100644
--- a/Mathlib/Logic/Function/Basic.lean
+++ b/Mathlib/Logic/Function/Basic.lean
@@ -107,8 +107,8 @@ theorem Injective.ne_iff' (hf : Injective f) {x y : α} {z : β} (h : f y = z) :
   h ▸ hf.ne_iff
 #align function.injective.ne_iff' Function.Injective.ne_iff'
 
-theorem Injective.not_exists_equal (h: ¬ Injective f): ∃ a b, a ≠ b ∧ f a = f b := by
-  unfold Injective at h; simp at h
+theorem Injective.exists_ne_of_not_injective (h: ¬ Injective f): ∃ a b, a ≠ b ∧ f a = f b := by
+  unfold Injective at h; simp only [not_forall, exists_prop] at h
   let ⟨a, b, h_f, h_ab⟩ := h
   exact ⟨a, b, h_ab, h_f⟩
 
diff --git a/Mathlib/Order/Monotone/Basic.lean b/Mathlib/Order/Monotone/Basic.lean
index 566f68b05f58c..ded53d9f59844 100644
--- a/Mathlib/Order/Monotone/Basic.lean
+++ b/Mathlib/Order/Monotone/Basic.lean
@@ -919,6 +919,22 @@ theorem Antitone.strictAnti_iff_injective (hf : Antitone f) : StrictAnti f ↔ I
   ⟨fun h ↦ h.injective, hf.strictAnti_of_injective⟩
 #align antitone.strict_anti_iff_injective Antitone.strictAnti_iff_injective
 
+/-- If a monotone function is equal at two points, it is equal between all of them -/
+theorem Monotone.stabilizing {a₁ a₂ : α} (h_mon : Monotone f) (h_fa : f a₁ = f a₂):
+    ∀ i, a₂ ≥ i → i ≥ a₁ → f i = f a₁ := by
+  intro i h₂ h₁
+  apply le_antisymm
+  · rw[h_fa]; exact h_mon h₂
+  · exact h_mon h₁
+
+/-- If an antitone function is equal at two points, it is equal between all of them -/
+theorem Antitone.stabilizing {a₁ a₂ : α} (h_anti : Antitone f) (h_fa : f a₁ = f a₂):
+    ∀ i, a₂ ≥ i → i ≥ a₁ → f i = f a₁ := by
+  intro i h₂ h₁
+  apply le_antisymm
+  · exact h_anti h₁
+  · rw[h_fa]; exact h_anti h₂
+
 end PartialOrder
 
 variable [LinearOrder β] {f : α → β} {s : Set α} {x y : α}
diff --git a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean b/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
index d32dc35bc8cc9..d19ce8baf316f 100644
--- a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
+++ b/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
@@ -14,7 +14,9 @@ import Mathlib.SetTheory.Ordinal.Arithmetic
 # Ordinal Approximants for the Fixed points on complete lattices
 
 This file sets up the ordinal approximation theory of fixed points
-of a monotone function in a complete lattice.
+of a monotone function in a complete lattice [CousotCousot1979].
+
+We loosly follow the proof from [Echenique2005].
 
 ## Main definitions
 
@@ -29,6 +31,10 @@ of a monotone function in a complete lattice.
 * `OrdinalApprox.gfp_is_gfp_approx`: The approximation of
   the greatest fixed point eventually reaches the greatest fixed point
 
+## References
+* [Federico Echenique, *A short and constructive proof of Tarski’s fixed-point theorem*][Echenique2005]
+* [Patrick Cousot & Radhia Cousot, *Constructive Versions of Tarski's Fixed Point Theorems*][CousotCousot1979]
+
 ## Tags
 
 fixed point, complete lattice, monotone function, ordinals, approximation
@@ -42,56 +48,24 @@ variable (g: Ordinal → α)
 
 open Cardinal Ordinal SuccOrder Function
 
-/-- Limiation of an ordinal defined function to an initial segment -/
-def limitation : { i : Ordinal // i < (ord $ succ #α)} → α := λ i => g i
+/-- Limitation of an ordinal defined function to the initial segment
+  containing the codomains cardinality -/
+def limitation : { i : Ordinal // i < (ord <| succ #α) } → α := fun i => g i
 
-theorem limitation_def : ∀ i, limitation g i = g i := by
-  intro h; unfold limitation; exact rfl
+theorem limitation_def (i : { i : Ordinal // i < (ord <| succ #α) }) : limitation g i = g i := rfl
 
-lemma mk_initialSeg_Subtype (ℵ : Cardinal ): #{ i : Ordinal // i < (ord  ℵ)} = lift.{u+1, u} ℵ := by
-  simpa using mk_initialSeg (ord ℵ)
-
-theorem limitation_not_injective: ¬ Injective (limitation g) := by
+theorem not_injective_limitation: ¬ Injective (limitation g) := by
   intro h_inj
-  have h₁ := by apply lift_mk_le_lift_mk_of_injective h_inj;
-  rw[mk_initialSeg_Subtype (succ #α), Cardinal.lift_lift, Cardinal.lift_le] at h₁
+  have h₁ := by apply lift_mk_le_lift_mk_of_injective h_inj
+  have mk_initialSeg_subtype :
+      #{ i : Ordinal // i < (ord <| succ #α) } = lift.{u+1, u} (succ #α) := by
+    simpa using mk_initialSeg (ord <| succ #α)
+  rw[mk_initialSeg_subtype, Cardinal.lift_lift, Cardinal.lift_le] at h₁
   have h₂ := not_le_of_lt (Cardinal.succ_lt #α)
   exact h₂ h₁
 
 end Cardinal
 
-
-
-namespace Monotone
-
-
-universe u v
-variable {α : Type u}
-variable {β : Type v}
-variable [Preorder α] [PartialOrder β] (f: α → β)
-
-/-- If a monotone function is equal at two points, it is equal between all of them -/
-theorem monotone_stabilizing {a₁ a₂ : α} (h_mon : Monotone f) (h_fa : f a₁ = f a₂):
-    ∀ i, a₂ ≥ i → i ≥ a₁ → f i = f a₁ := by
-  intro i h₂ h₁
-  apply le_antisymm
-  · rw[h_fa]; exact h_mon h₂
-  · exact h_mon h₁
-
-/-- If an antitone function is equal at two points, it is equal between all of them -/
-theorem antitone_stabilizing {a₁ a₂ : α} (h_anti : Antitone f) (h_fa : f a₁ = f a₂):
-    ∀ i, a₂ ≥ i → i ≥ a₁ → f i = f a₁ := by
-  intro i h₂ h₁
-  apply le_antisymm
-  · exact h_anti h₁
-  · rw[h_fa]; exact h_anti h₂
-
-end Monotone
-
-/-We loosly follow the proof from Frederico Enchenique in A Short and Constructive Proof of
-  Tarski's fixed-point theorem published in the International Journal of Game Theory Volume 33(2),
-  June 2005, pages 215-218. -/
-
 namespace OrdinalApprox
 
 universe u
@@ -102,68 +76,64 @@ open Function fixedPoints Cardinal Order OrderHom
 
 set_option linter.unusedVariables false in
 /-- Ordinal approximants of the least fixed points -/
-def lfp_approx (a : Ordinal.{u}) : α :=
-  sSup { f (lfp_approx b) | (b : Ordinal) (h : b < a) }
-termination_by lfp_approx a => a
+def lfpApprox (a : Ordinal.{u}) : α :=
+  sSup { f (lfpApprox b) | (b : Ordinal) (h : b < a) }
+termination_by a
 decreasing_by exact h
 
-theorem lfp_approx_monotone : Monotone (lfp_approx f) := by
-  unfold Monotone; intros a b h; unfold lfp_approx
+theorem lfpApprox_monotone : Monotone (lfpApprox f) := by
+  unfold Monotone; intros a b h; unfold lfpApprox
   refine sSup_le_sSup ?h; simp
   intros a' h'
   use a'; apply And.intro; exact lt_of_lt_of_le h' h
   exact rfl
 
-/-- Ordinal approximants of the least fixed points as an order homomorphism -/
-def lfp_approx_hom : Ordinal.{u} →o α where
-  toFun i := lfp_approx f i
-  monotone' a b h := by simp; apply lfp_approx_monotone f h
-
-theorem lfp_approx_addition (a : Ordinal.{u}) : f (lfp_approx f a) = lfp_approx f (a+1) := by
+theorem lfpApprox_addition (a : Ordinal.{u}) : f (lfpApprox f a) = lfpApprox f (a+1) := by
   apply le_antisymm
-  · conv => right; unfold lfp_approx
+  · conv => right; unfold lfpApprox
     apply le_sSup; simp
     use a
-  · conv => left; unfold lfp_approx
+  · conv => left; unfold lfpApprox
     apply sSup_le; simp
     intros a' h
-    apply f.2; apply lfp_approx_monotone; exact h
+    apply f.2; apply lfpApprox_monotone; exact h
 
 /-- The ordinal approximants of the least fixed points are stabilizing
   when reaching a fixed point of f -/
-theorem lfp_approx_stabilizing_at_fp (a : Ordinal.{u}) (h: lfp_approx f a ∈ (fixedPoints f)):
-    ∀ b > a, lfp_approx f b = lfp_approx f a := by
+theorem lfpApprox_stabilizing_at_fp (a : Ordinal.{u}) (h: lfpApprox f a ∈ fixedPoints f):
+    ∀ b > a, lfpApprox f b = lfpApprox f a := by
   intro b hab; rw[mem_fixedPoints_iff] at h;
   induction b using Ordinal.induction with | h b IH =>
   apply le_antisymm
-  · conv => left; unfold lfp_approx
+  · conv => left; unfold lfpApprox
     apply sSup_le; simp
     intro a' ha'b
     by_cases haa : a' < a
-    · rw[lfp_approx_addition]
-      apply lfp_approx_monotone
+    · rw[lfpApprox_addition]
+      apply lfpApprox_monotone
       simp; exact haa
     · simp at haa
       cases (le_iff_lt_or_eq.mp haa) with
-      | inl haa => specialize IH a' ha'b haa; rw[IH, h];
-      | inr haa => rw[← haa, h];
-  · conv => right; unfold lfp_approx
+      | inl haa => specialize IH a' ha'b haa; rw[IH, h]
+      | inr haa => rw[← haa, h]
+  · conv => right; unfold lfpApprox
     apply le_sSup; simp
     use a
 
 /-- Every value after a fixed point of f is also a fixed point of f -/
-theorem lfp_approx_eq_fp (a : Ordinal.{u}) (h: lfp_approx f a ∈ (fixedPoints f)):
-    ∀ b > a, lfp_approx f b ∈ (fixedPoints f)  := by
+theorem lfpApprox_eq_fp (a : Ordinal.{u}) (h: lfpApprox f a ∈ fixedPoints f):
+    ∀ b > a, lfpApprox f b ∈ fixedPoints f  := by
   intro b h_ab;
   rw[mem_fixedPoints_iff]
-  have h_stab := lfp_approx_stabilizing_at_fp f a h b h_ab
+  have h_stab := lfpApprox_stabilizing_at_fp f a h b h_ab
   rw[h_stab]
   exact mem_fixedPoints_iff.mp h
 
 /-- There are ordinals smaller than the successor of the domains cardinals with equal value -/
-theorem lfp_approx_equal_value : ∃ i < ord $ succ #α, ∃ j < ord $ succ #α,
-    i ≠ j ∧ lfp_approx f i = lfp_approx f j := by
-  have h_ninj := Function.Injective.not_exists_equal (limitation_not_injective $ lfp_approx f)
+theorem lfpApprox_equal_value : ∃ i < ord <| succ #α, ∃ j < ord <| succ #α,
+    i ≠ j ∧ lfpApprox f i = lfpApprox f j := by
+  have h_ninj := Function.Injective.exists_ne_of_not_injective
+    (not_injective_limitation <| lfpApprox f)
   let ⟨a, b, h_nab, h_fab⟩ := h_ninj
   rw[limitation_def, limitation_def] at h_fab
   use a.val; apply And.intro a.prop;
@@ -172,43 +142,43 @@ theorem lfp_approx_equal_value : ∃ i < ord $ succ #α, ∃ j < ord $ succ #α,
   · intro h_eq; rw[Subtype.coe_inj] at h_eq; exact h_nab h_eq
   · exact h_fab
 
-/-- If there are ordinals with equal value then the values are fixed points of f -/
-lemma lfp_approx_one_fixedPoint (a b : Ordinal.{u}) (h : a < b)
-    (h_fab : lfp_approx f a = lfp_approx f b):
-    lfp_approx f a ∈ (fixedPoints f) := by
-  rw[mem_fixedPoints_iff,lfp_approx_addition]
-  apply Monotone.monotone_stabilizing (lfp_approx f) (lfp_approx_monotone f)
+/-- If there are distinct ordinals with equal value then the values are fixed points -/
+lemma lfpApprox_one_fixedPoint (a b : Ordinal.{u}) (h : a < b)
+    (h_fab : lfpApprox f a = lfpApprox f b):
+    lfpApprox f a ∈ fixedPoints f := by
+  rw[mem_fixedPoints_iff,lfpApprox_addition]
+  apply Monotone.stabilizing (lfpApprox_monotone f)
     h_fab (a+1) (SuccOrder.succ_le_of_lt h) (SuccOrder.le_succ a)
 
-/-- If there are ordinals with equal value then
-  every value follwing the smaller ordinal are fixed points of -/
-lemma lfp_approx_many_fixedPoints (a b : Ordinal.{u}) (h : a < b)
-    (h_fab : lfp_approx f a = lfp_approx f b):
-    ∀ i ≥ a, lfp_approx f i ∈ (fixedPoints f) := by
-  intro i h_i;
-  by_cases h_ia : i = a
-  · rw[h_ia]; exact lfp_approx_one_fixedPoint f a b h h_fab
-  · apply lfp_approx_eq_fp f a
-    · exact lfp_approx_one_fixedPoint f a b h h_fab
+/-- If there are disctinct ordinals with equal value then
+  every value succeding the smaller ordinal are fixed points -/
+lemma lfpApprox_many_fixedPoints (a b : Ordinal.{u}) (h : a < b)
+    (h_fab : lfpApprox f a = lfpApprox f b):
+    ∀ i ≥ a, lfpApprox f i ∈ fixedPoints f := by
+  intro i h_i
+  obtain rfl | h_ia := eq_or_ne i a
+  · exact lfpApprox_one_fixedPoint f i b h h_fab
+  · apply lfpApprox_eq_fp f a
+    · exact lfpApprox_one_fixedPoint f a b h h_fab
     · exact Ne.lt_of_le' h_ia h_i
 
 /-- A fixed point of f is reached after the successor of the domains cardinality -/
-theorem lfp_approx_has_fixedPoint_cardinal : lfp_approx f (ord $ succ #α) ∈ (fixedPoints f) := by
-  let ⟨a, h_a, b, h_b, h_nab, h_fab⟩ := lfp_approx_equal_value f
-  cases (le_total a b) with
+theorem lfpApprox_has_fixedPoint_cardinal : lfpApprox f (ord <| succ #α) ∈ fixedPoints f := by
+  let ⟨a, h_a, b, h_b, h_nab, h_fab⟩ := lfpApprox_equal_value f
+  cases le_total a b with
   | inl h_ab =>
-    exact lfp_approx_many_fixedPoints f a b (Ne.lt_of_le h_nab h_ab) h_fab
-      (ord $ succ #α) (le_of_lt h_a)
+    exact lfpApprox_many_fixedPoints f a b (h_nab.lt_of_le h_ab) h_fab
+      (ord <| succ #α) (le_of_lt h_a)
   | inr h_ba =>
-    exact lfp_approx_many_fixedPoints f b a (Ne.lt_of_le (id (Ne.symm h_nab)) h_ba)
-      (h_fab.symm) (ord $ succ #α) (le_of_lt h_b)
+    exact lfpApprox_many_fixedPoints f b a (h_nab.symm.lt_of_le h_ba)
+      (h_fab.symm) (ord <| succ #α) (le_of_lt h_b)
 
 /-- Every value of the ordinal approximants are less or equal than every fixed point of f -/
-theorem lfp_approx_le_fixedPoint : ∀ a : (fixedPoints f), ∀ i : Ordinal, lfp_approx f i ≤ a := by
+theorem lfpApprox_le_fixedPoint : ∀ a : fixedPoints f, ∀ i : Ordinal, lfpApprox f i ≤ a := by
   intro ⟨a, h_a⟩ i
   induction i using Ordinal.induction with
   | h i IH =>
-    unfold lfp_approx
+    unfold lfpApprox
     apply sSup_le; simp
     intro j h_j
     rw[← h_a]
@@ -216,150 +186,67 @@ theorem lfp_approx_le_fixedPoint : ∀ a : (fixedPoints f), ∀ i : Ordinal, lfp
     exact IH j h_j
 
 /-- The least fixed point of f is reached after the successor of the domains cardinality -/
-theorem lfp_approx_cardinal_is_lfp : lfp_approx f (ord $ succ #α) = lfp f := by
+theorem lfpApprox_cardinal_is_lfp : lfpApprox f (ord <| succ #α) = lfp f := by
   apply le_antisymm
   · have h_lfp : ∃ x : fixedPoints f, lfp f = x := by use ⊥; exact rfl
     let ⟨x, h_x⟩ := h_lfp; rw[h_x]
-    exact lfp_approx_le_fixedPoint f x (ord $ succ #α)
-  · have h_fix : ∃ x: fixedPoints f, lfp_approx f (ord $ succ #α) = x := by
-      simpa using lfp_approx_has_fixedPoint_cardinal f
+    exact lfpApprox_le_fixedPoint f x (ord <| succ #α)
+  · have h_fix : ∃ x: fixedPoints f, lfpApprox f (ord <| succ #α) = x := by
+      simpa using lfpApprox_has_fixedPoint_cardinal f
     let ⟨x, h_x⟩ := h_fix; rw[h_x]
     exact lfp_le_fixed f x.prop
 
 /-- **Constructive Knaster-Tarski Theorem**: Some ordinal approximation of the least fixed point
   is the least fixed point. Also known as ordinal approximation of the least fixed point.-/
-theorem lfp_approx_is_lfp : ∃ a : Ordinal, lfp_approx f a = lfp f := by
-  use (ord $ succ #α)
-  exact lfp_approx_cardinal_is_lfp f
-
+theorem lfpApprox_is_lfp : ∃ a : Ordinal, lfpApprox f a = lfp f := by
+  use (ord <| succ #α)
+  exact lfpApprox_cardinal_is_lfp f
 
 set_option linter.unusedVariables false in
-/-- Ordinal approximants of the least fixed points -/
-def gfp_approx (a : Ordinal.{u}) : α :=
-  sInf { f (gfp_approx b) | (b : Ordinal) (h : b < a) }
-termination_by gfp_approx a => a
+/-- Ordinal approximants of the greatest fixed points -/
+def gfpApprox (a : Ordinal.{u}) : α :=
+  sInf { f (gfpApprox b) | (b : Ordinal) (h : b < a) }
+termination_by a
 decreasing_by exact h
 
-theorem gfp_approx_antitone : Antitone (gfp_approx f) := by
-  unfold Antitone; intros a b h; unfold gfp_approx
-  refine sInf_le_sInf ?h; simp
-  intros a' h'
-  use a'; apply And.intro; exact lt_of_lt_of_le h' h
-  exact rfl
+theorem gfpApprox_antitone : Antitone (gfpApprox f) :=
+  lfpApprox_monotone (OrderHom.dual f)
 
-theorem gfp_approx_addition (a : Ordinal.{u}) : f (gfp_approx f a) = gfp_approx f (a+1) := by
-  apply le_antisymm
-  · conv => right; unfold gfp_approx
-    apply le_sInf; simp
-    intros a' h
-    apply f.2; apply gfp_approx_antitone; exact h
-  · conv => left; unfold gfp_approx
-    apply sInf_le; simp
-    use a
+theorem gfpApprox_addition (a : Ordinal.{u}) : f (gfpApprox f a) = gfpApprox f (a+1) :=
+  lfpApprox_addition (OrderHom.dual f) a
 
 /-- The ordinal approximants of the least fixed points are stabilizing
   when reaching a fixed point of f -/
-theorem gfp_approx_stabilizing_at_fp (a : Ordinal.{u}) (h: gfp_approx f a ∈ (fixedPoints f)):
-    ∀ b > a, gfp_approx f b = gfp_approx f a := by
-  intro b hab; rw[mem_fixedPoints_iff] at h;
-  induction b using Ordinal.induction with | h b IH =>
-  apply le_antisymm
-  · conv => left; unfold gfp_approx
-    apply sInf_le
-    use a
-  · conv => right; unfold gfp_approx
-    apply le_sInf; simp
-    intro a' ha'b
-    by_cases haa : a' < a
-    · rw[gfp_approx_addition]
-      apply gfp_approx_antitone
-      simp; exact haa
-    · simp at haa
-      cases (le_iff_lt_or_eq.mp haa) with
-      | inl haa => specialize IH a' ha'b haa; rw[IH, h];
-      | inr haa => rw[← haa, h];
+theorem gfpApprox_stabilizing_at_fp (a : Ordinal.{u}) (h: gfpApprox f a ∈ fixedPoints f):
+    ∀ b > a, gfpApprox f b = gfpApprox f a :=
+  lfpApprox_stabilizing_at_fp (OrderHom.dual f) a h
 
 /-- Every value after a fixed point of f is also a fixed point of f -/
-theorem gfp_approx_eq_fp (a : Ordinal.{u}) (h: gfp_approx f a ∈ (fixedPoints f)):
-    ∀ b > a, gfp_approx f b ∈ (fixedPoints f)  := by
-  intro b h_ab;
-  rw[mem_fixedPoints_iff]
-  have h_stab := gfp_approx_stabilizing_at_fp f a h b h_ab
-  rw[h_stab]
-  exact mem_fixedPoints_iff.mp h
+theorem gfpApprox_eq_fp (a : Ordinal.{u}) (h: gfpApprox f a ∈ fixedPoints f):
+    ∀ b > a, gfpApprox f b ∈ (fixedPoints f) :=
+  lfpApprox_eq_fp (OrderHom.dual f) a h
 
 /-- There are ordinals smaller than the successor of the domains cardinals with equal value -/
-theorem gfp_approx_equal_value : ∃ i < ord $ succ #α, ∃ j < ord $ succ #α,
-    i ≠ j ∧ gfp_approx f i = gfp_approx f j := by
-  have h_ninj := Function.Injective.not_exists_equal (limitation_not_injective $ gfp_approx f)
-  let ⟨a, b, h_nab, h_fab⟩ := h_ninj
-  rw[limitation_def, limitation_def] at h_fab
-  use a.val; apply And.intro a.prop;
-  use b.val; apply And.intro b.prop;
-  apply And.intro
-  · intro h_eq; rw[Subtype.coe_inj] at h_eq; exact h_nab h_eq
-  · exact h_fab
-
-/-- If there are ordinals with equal value then the values are fixed points of f -/
-lemma gfp_approx_one_fixedPoint (a b : Ordinal.{u}) (h : a < b)
-    (h_fab : gfp_approx f a = gfp_approx f b):
-    gfp_approx f a ∈ (fixedPoints f) := by
-  rw[mem_fixedPoints_iff,gfp_approx_addition]
-  apply Monotone.antitone_stabilizing (gfp_approx f) (gfp_approx_antitone f)
-    h_fab (a+1) (SuccOrder.succ_le_of_lt h) (SuccOrder.le_succ a)
-
-/-- If there are ordinals with equal value then
-  every value follwing the smaller ordinal are fixed points of -/
-lemma gfp_approx_many_fixedPoints (a b : Ordinal.{u}) (h : a < b)
-    (h_fab : gfp_approx f a = gfp_approx f b):
-    ∀ i ≥ a, gfp_approx f i ∈ (fixedPoints f) := by
-  intro i h_i;
-  by_cases h_ia : i = a
-  · rw[h_ia]; exact gfp_approx_one_fixedPoint f a b h h_fab
-  · apply gfp_approx_eq_fp f a
-    · exact gfp_approx_one_fixedPoint f a b h h_fab
-    · exact Ne.lt_of_le' h_ia h_i
+theorem gfpApprox_equal_value : ∃ i < ord <| succ #α, ∃ j < ord <| succ #α,
+    i ≠ j ∧ gfpApprox f i = gfpApprox f j :=
+  lfpApprox_equal_value (OrderHom.dual f)
 
 /-- A fixed point of f is reached after the successor of the domains cardinality -/
-lemma gfp_approx_has_fixedPoint_cardinal : gfp_approx f (ord $ succ #α) ∈ (fixedPoints f) := by
-  let ⟨a, h_a, b, h_b, h_nab, h_fab⟩ := gfp_approx_equal_value f
-  cases (le_total a b) with
-  | inl h_ab =>
-    exact gfp_approx_many_fixedPoints f a b (Ne.lt_of_le h_nab h_ab)
-      h_fab (ord $ succ #α) (le_of_lt h_a)
-  | inr h_ba =>
-    exact gfp_approx_many_fixedPoints f b a (Ne.lt_of_le (id (Ne.symm h_nab)) h_ba)
-      (h_fab.symm) (ord $ succ #α) (le_of_lt h_b)
+lemma gfpApprox_has_fixedPoint_cardinal : gfpApprox f (ord <| succ #α) ∈ fixedPoints f :=
+  lfpApprox_has_fixedPoint_cardinal (OrderHom.dual f)
 
 /-- Every value of the ordinal approximants are greater or equal than every fixed point of f -/
-lemma gfp_approx_ge_fixedPoint : ∀ a : (fixedPoints f), ∀ i : Ordinal, gfp_approx f i ≥ a := by
-  intro ⟨a, h_a⟩ i
-  induction i using Ordinal.induction with
-  | h i IH =>
-    unfold gfp_approx
-    apply le_sInf; simp
-    intro j h_j
-    rw[← h_a]
-    apply f.monotone'
-    exact IH j h_j
+lemma gfpApprox_ge_fixedPoint : ∀ a : (fixedPoints f), ∀ i : Ordinal, gfpApprox f i ≥ a :=
+  lfpApprox_le_fixedPoint (OrderHom.dual f)
 
 /-- The greatest fixed point of f is reached after the successor of the domains cardinality -/
-theorem gfp_approx_cardinal_is_gfp : gfp_approx f (ord $ succ #α) = gfp f := by
-  apply le_antisymm
-  · have h_fix : ∃ x: fixedPoints f, gfp_approx f (ord $ succ #α) = x := by
-      simpa using gfp_approx_has_fixedPoint_cardinal f
-    let ⟨x, h_x⟩ := h_fix; rw[h_x]
-    exact fixed_le_gfp f x.prop
-  · have h_lfp : ∃ x : fixedPoints f, gfp f = x := by use ⊤; exact rfl
-    let ⟨x, h_x⟩ := h_lfp; rw[h_x]
-    exact gfp_approx_ge_fixedPoint f x (ord $ succ #α)
-
+theorem gfpApprox_cardinal_is_gfp : gfpApprox f (ord <| succ #α) = gfp f :=
+  lfpApprox_cardinal_is_lfp (OrderHom.dual f)
 
 /-- **Dual Constructive Knaster-Tarski Theorem**: Some ordinal approximation of
   the greatest fixed point is the greatest fixed point. Also known as ordinal approximation of
   the greatest fixed point.-/
-theorem gfp_approx_is_gfp : ∃ a : Ordinal, gfp_approx f a = gfp f := by
-  use (ord $ succ #α)
-  exact gfp_approx_cardinal_is_gfp f
+theorem gfpApprox_is_gfp : ∃ a : Ordinal, gfpApprox f a = gfp f :=
+  lfpApprox_is_lfp (OrderHom.dual f)
 
 end OrdinalApprox
diff --git a/Mathlib/SetTheory/Cardinal/Basic.lean b/Mathlib/SetTheory/Cardinal/Basic.lean
index 2e6aae64dcb89..04dff94ecf1a3 100644
--- a/Mathlib/SetTheory/Cardinal/Basic.lean
+++ b/Mathlib/SetTheory/Cardinal/Basic.lean
@@ -830,12 +830,13 @@ theorem add_one_le_succ (c : Cardinal.{u}) : c + 1 ≤ succ c := by
     _ ≤ #β := (f.optionElim b hb).cardinal_le
 #align cardinal.add_one_le_succ Cardinal.add_one_le_succ
 
-theorem no_max : ∀ ℵ : Cardinal, ¬ IsMax ℵ := by
-  intro ℵ h
-  unfold IsMax at h; specialize h (le_of_lt $ cantor ℵ)
+theorem not_isMax (ℵ : Cardinal): ¬ IsMax ℵ := by
+  intro h
+  unfold IsMax at h
+  specialize h (le_of_lt $ cantor ℵ)
   exact not_lt_of_le h (cantor ℵ)
 
-theorem succ_lt : ∀ ℵ : Cardinal, ℵ < succ ℵ := λ ℵ => Order.lt_succ_of_not_isMax (no_max ℵ)
+theorem succ_lt (ℵ : Cardinal): ℵ < succ ℵ := Order.lt_succ_of_not_isMax (not_isMax ℵ)
 
 /-- A cardinal is a limit if it is not zero or a successor cardinal. Note that `ℵ₀` is a limit
   cardinal by this definition, but `0` isn't.
diff --git a/docs/references.bib b/docs/references.bib
index f1729b815991f..ea4ed23933b51 100644
--- a/docs/references.bib
+++ b/docs/references.bib
@@ -803,6 +803,16 @@ @Book{            conway2001
   mrnumber      = {1803095}
 }
 
+@article{         CousotCousot1979,
+  author        = {Cousot, P{.} and Cousot, R{.}},
+  title         = {Constructive Versions of {T}arski's Fixed Point Theorems},
+  journal       = {Pacific Journal of Mathematics},
+  volume        = 81,
+  number        = 1,
+  pages         = {43--57},
+  year          = 1979,
+}
+
 @Book{            coxlittleoshea1997,
   author        = {David A. Cox and John Little and Donal O'Shea},
   title         = {Ideals, varieties, and algorithms - an introduction to
@@ -977,6 +987,17 @@ @Article{         elliott2006binomial
   doi           = {10.1016/j.jpaa.2005.09.003}
 }
 
+@article{         Echenique2005,
+  author        = {Echenique, Federico},
+  title         = {A short and constructive proof of Tarski’s fixed-point theorem},
+  journal       = {International Journal of Game Theory},
+  volume        = {33},
+  number        = {2},
+  year          = {2005},
+  pages         = {215–218},
+  publisher     = {Springer},
+  doi           = {10.1007/s001820400192}
+}
 @Book{            engel1997,
   title         = {Sperner theory},
   author        = {Engel, Konrad},

From 32ada0dcda8e3fc285cc051fdbe386d12a7d92db Mon Sep 17 00:00:00 2001
From: Ira Fesefeldt <fesefeldt@cs.rwth-aachen.de>
Date: Sat, 2 Mar 2024 16:00:41 +0100
Subject: [PATCH 08/31] fixed multiple typos and overseen issues

---
 Mathlib/Order/Monotone/Basic.lean             |  4 +--
 .../Order/OrdinalApproximantsFixedPoints.lean | 32 ++++++++++---------
 Mathlib/SetTheory/Cardinal/Basic.lean         |  6 ++--
 docs/references.bib                           |  6 ++--
 4 files changed, 25 insertions(+), 23 deletions(-)

diff --git a/Mathlib/Order/Monotone/Basic.lean b/Mathlib/Order/Monotone/Basic.lean
index ded53d9f59844..61f7d8bcd5661 100644
--- a/Mathlib/Order/Monotone/Basic.lean
+++ b/Mathlib/Order/Monotone/Basic.lean
@@ -920,7 +920,7 @@ theorem Antitone.strictAnti_iff_injective (hf : Antitone f) : StrictAnti f ↔ I
 #align antitone.strict_anti_iff_injective Antitone.strictAnti_iff_injective
 
 /-- If a monotone function is equal at two points, it is equal between all of them -/
-theorem Monotone.stabilizing {a₁ a₂ : α} (h_mon : Monotone f) (h_fa : f a₁ = f a₂):
+theorem Monotone.stabilizing {a₁ a₂ : α} (h_mon : Monotone f) (h_fa : f a₁ = f a₂) :
     ∀ i, a₂ ≥ i → i ≥ a₁ → f i = f a₁ := by
   intro i h₂ h₁
   apply le_antisymm
@@ -928,7 +928,7 @@ theorem Monotone.stabilizing {a₁ a₂ : α} (h_mon : Monotone f) (h_fa : f a
   · exact h_mon h₁
 
 /-- If an antitone function is equal at two points, it is equal between all of them -/
-theorem Antitone.stabilizing {a₁ a₂ : α} (h_anti : Antitone f) (h_fa : f a₁ = f a₂):
+theorem Antitone.stabilizing {a₁ a₂ : α} (h_anti : Antitone f) (h_fa : f a₁ = f a₂) :
     ∀ i, a₂ ≥ i → i ≥ a₁ → f i = f a₁ := by
   intro i h₂ h₁
   apply le_antisymm
diff --git a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean b/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
index d19ce8baf316f..a2050ce43a6a6 100644
--- a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
+++ b/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
@@ -14,7 +14,7 @@ import Mathlib.SetTheory.Ordinal.Arithmetic
 # Ordinal Approximants for the Fixed points on complete lattices
 
 This file sets up the ordinal approximation theory of fixed points
-of a monotone function in a complete lattice [CousotCousot1979].
+of a monotone function in a complete lattice [Cousot1979].
 
 We loosly follow the proof from [Echenique2005].
 
@@ -32,8 +32,8 @@ We loosly follow the proof from [Echenique2005].
   the greatest fixed point eventually reaches the greatest fixed point
 
 ## References
-* [Federico Echenique, *A short and constructive proof of Tarski’s fixed-point theorem*][Echenique2005]
-* [Patrick Cousot & Radhia Cousot, *Constructive Versions of Tarski's Fixed Point Theorems*][CousotCousot1979]
+* [F. Echenique, *A short and constructive proof of Tarski’s fixed-point theorem*][Echenique2005]
+* [P. Cousot & R. Cousot, *Constructive Versions of Tarski's Fixed Point Theorems*][Cousot1979]
 
 ## Tags
 
@@ -54,7 +54,7 @@ def limitation : { i : Ordinal // i < (ord <| succ #α) } → α := fun i => g i
 
 theorem limitation_def (i : { i : Ordinal // i < (ord <| succ #α) }) : limitation g i = g i := rfl
 
-theorem not_injective_limitation: ¬ Injective (limitation g) := by
+theorem not_injective_limitation : ¬ Injective (limitation g) := by
   intro h_inj
   have h₁ := by apply lift_mk_le_lift_mk_of_injective h_inj
   have mk_initialSeg_subtype :
@@ -85,8 +85,8 @@ theorem lfpApprox_monotone : Monotone (lfpApprox f) := by
   unfold Monotone; intros a b h; unfold lfpApprox
   refine sSup_le_sSup ?h; simp
   intros a' h'
-  use a'; apply And.intro; exact lt_of_lt_of_le h' h
-  exact rfl
+  use a'
+  exact ⟨lt_of_lt_of_le h' h, rfl⟩
 
 theorem lfpApprox_addition (a : Ordinal.{u}) : f (lfpApprox f a) = lfpApprox f (a+1) := by
   apply le_antisymm
@@ -102,7 +102,7 @@ theorem lfpApprox_addition (a : Ordinal.{u}) : f (lfpApprox f a) = lfpApprox f (
   when reaching a fixed point of f -/
 theorem lfpApprox_stabilizing_at_fp (a : Ordinal.{u}) (h: lfpApprox f a ∈ fixedPoints f):
     ∀ b > a, lfpApprox f b = lfpApprox f a := by
-  intro b hab; rw[mem_fixedPoints_iff] at h;
+  intro b hab; rw[mem_fixedPoints_iff] at h
   induction b using Ordinal.induction with | h b IH =>
   apply le_antisymm
   · conv => left; unfold lfpApprox
@@ -113,7 +113,7 @@ theorem lfpApprox_stabilizing_at_fp (a : Ordinal.{u}) (h: lfpApprox f a ∈ fixe
       apply lfpApprox_monotone
       simp; exact haa
     · simp at haa
-      cases (le_iff_lt_or_eq.mp haa) with
+      cases le_iff_lt_or_eq.mp haa with
       | inl haa => specialize IH a' ha'b haa; rw[IH, h]
       | inr haa => rw[← haa, h]
   · conv => right; unfold lfpApprox
@@ -123,21 +123,22 @@ theorem lfpApprox_stabilizing_at_fp (a : Ordinal.{u}) (h: lfpApprox f a ∈ fixe
 /-- Every value after a fixed point of f is also a fixed point of f -/
 theorem lfpApprox_eq_fp (a : Ordinal.{u}) (h: lfpApprox f a ∈ fixedPoints f):
     ∀ b > a, lfpApprox f b ∈ fixedPoints f  := by
-  intro b h_ab;
+  intro b h_ab
   rw[mem_fixedPoints_iff]
   have h_stab := lfpApprox_stabilizing_at_fp f a h b h_ab
   rw[h_stab]
   exact mem_fixedPoints_iff.mp h
 
-/-- There are ordinals smaller than the successor of the domains cardinals with equal value -/
+/-- There are distinct ordinals smaller than the successor of the domains cardinals
+  with equal value -/
 theorem lfpApprox_equal_value : ∃ i < ord <| succ #α, ∃ j < ord <| succ #α,
     i ≠ j ∧ lfpApprox f i = lfpApprox f j := by
   have h_ninj := Function.Injective.exists_ne_of_not_injective
     (not_injective_limitation <| lfpApprox f)
   let ⟨a, b, h_nab, h_fab⟩ := h_ninj
   rw[limitation_def, limitation_def] at h_fab
-  use a.val; apply And.intro a.prop;
-  use b.val; apply And.intro b.prop;
+  use a.val; apply And.intro a.prop
+  use b.val; apply And.intro b.prop
   apply And.intro
   · intro h_eq; rw[Subtype.coe_inj] at h_eq; exact h_nab h_eq
   · exact h_fab
@@ -223,10 +224,11 @@ theorem gfpApprox_stabilizing_at_fp (a : Ordinal.{u}) (h: gfpApprox f a ∈ fixe
 
 /-- Every value after a fixed point of f is also a fixed point of f -/
 theorem gfpApprox_eq_fp (a : Ordinal.{u}) (h: gfpApprox f a ∈ fixedPoints f):
-    ∀ b > a, gfpApprox f b ∈ (fixedPoints f) :=
+    ∀ b > a, gfpApprox f b ∈ fixedPoints f :=
   lfpApprox_eq_fp (OrderHom.dual f) a h
 
-/-- There are ordinals smaller than the successor of the domains cardinals with equal value -/
+/-- There are distinct ordinals smaller than the successor of the domains cardinals with
+  equal value -/
 theorem gfpApprox_equal_value : ∃ i < ord <| succ #α, ∃ j < ord <| succ #α,
     i ≠ j ∧ gfpApprox f i = gfpApprox f j :=
   lfpApprox_equal_value (OrderHom.dual f)
@@ -236,7 +238,7 @@ lemma gfpApprox_has_fixedPoint_cardinal : gfpApprox f (ord <| succ #α) ∈ fixe
   lfpApprox_has_fixedPoint_cardinal (OrderHom.dual f)
 
 /-- Every value of the ordinal approximants are greater or equal than every fixed point of f -/
-lemma gfpApprox_ge_fixedPoint : ∀ a : (fixedPoints f), ∀ i : Ordinal, gfpApprox f i ≥ a :=
+lemma gfpApprox_ge_fixedPoint : ∀ a : fixedPoints f, ∀ i : Ordinal, gfpApprox f i ≥ a :=
   lfpApprox_le_fixedPoint (OrderHom.dual f)
 
 /-- The greatest fixed point of f is reached after the successor of the domains cardinality -/
diff --git a/Mathlib/SetTheory/Cardinal/Basic.lean b/Mathlib/SetTheory/Cardinal/Basic.lean
index 04dff94ecf1a3..99a6949a73a1b 100644
--- a/Mathlib/SetTheory/Cardinal/Basic.lean
+++ b/Mathlib/SetTheory/Cardinal/Basic.lean
@@ -830,13 +830,13 @@ theorem add_one_le_succ (c : Cardinal.{u}) : c + 1 ≤ succ c := by
     _ ≤ #β := (f.optionElim b hb).cardinal_le
 #align cardinal.add_one_le_succ Cardinal.add_one_le_succ
 
-theorem not_isMax (ℵ : Cardinal): ¬ IsMax ℵ := by
+theorem not_isMax (ℵ : Cardinal) : ¬ IsMax ℵ := by
   intro h
   unfold IsMax at h
-  specialize h (le_of_lt $ cantor ℵ)
+  specialize h (cantor ℵ).le
   exact not_lt_of_le h (cantor ℵ)
 
-theorem succ_lt (ℵ : Cardinal): ℵ < succ ℵ := Order.lt_succ_of_not_isMax (not_isMax ℵ)
+theorem succ_lt (ℵ : Cardinal) : ℵ < succ ℵ := Order.lt_succ_of_not_isMax (not_isMax ℵ)
 
 /-- A cardinal is a limit if it is not zero or a successor cardinal. Note that `ℵ₀` is a limit
   cardinal by this definition, but `0` isn't.
diff --git a/docs/references.bib b/docs/references.bib
index ea4ed23933b51..b492a067ef176 100644
--- a/docs/references.bib
+++ b/docs/references.bib
@@ -803,14 +803,14 @@ @Book{            conway2001
   mrnumber      = {1803095}
 }
 
-@article{         CousotCousot1979,
+@Article{         Cousot1979,
   author        = {Cousot, P{.} and Cousot, R{.}},
   title         = {Constructive Versions of {T}arski's Fixed Point Theorems},
   journal       = {Pacific Journal of Mathematics},
   volume        = 81,
   number        = 1,
   pages         = {43--57},
-  year          = 1979,
+  year          = 1979
 }
 
 @Book{            coxlittleoshea1997,
@@ -987,7 +987,7 @@ @Article{         elliott2006binomial
   doi           = {10.1016/j.jpaa.2005.09.003}
 }
 
-@article{         Echenique2005,
+@Article{         Echenique2005,
   author        = {Echenique, Federico},
   title         = {A short and constructive proof of Tarski’s fixed-point theorem},
   journal       = {International Journal of Game Theory},

From 625d29488e6636b3252b3a4f8130e41e6e07ec72 Mon Sep 17 00:00:00 2001
From: Ira Fesefeldt <fesefeldt@cs.rwth-aachen.de>
Date: Sat, 2 Mar 2024 16:08:55 +0100
Subject: [PATCH 09/31] fixed linting issues

---
 Mathlib/Logic/Function/Basic.lean             |  2 +-
 Mathlib/Order/FixedPoints.lean                |  3 ---
 .../Order/OrdinalApproximantsFixedPoints.lean | 12 +++++-----
 docs/references.bib                           | 22 +++++++++----------
 4 files changed, 18 insertions(+), 21 deletions(-)

diff --git a/Mathlib/Logic/Function/Basic.lean b/Mathlib/Logic/Function/Basic.lean
index 8b79f8c3e516a..f0aab4138733f 100644
--- a/Mathlib/Logic/Function/Basic.lean
+++ b/Mathlib/Logic/Function/Basic.lean
@@ -107,7 +107,7 @@ theorem Injective.ne_iff' (hf : Injective f) {x y : α} {z : β} (h : f y = z) :
   h ▸ hf.ne_iff
 #align function.injective.ne_iff' Function.Injective.ne_iff'
 
-theorem Injective.exists_ne_of_not_injective (h: ¬ Injective f): ∃ a b, a ≠ b ∧ f a = f b := by
+theorem Injective.exists_ne_of_not_injective (h: ¬ Injective f) : ∃ a b, a ≠ b ∧ f a = f b := by
   unfold Injective at h; simp only [not_forall, exists_prop] at h
   let ⟨a, b, h_f, h_ab⟩ := h
   exact ⟨a, b, h_ab, h_f⟩
diff --git a/Mathlib/Order/FixedPoints.lean b/Mathlib/Order/FixedPoints.lean
index 4a04d99fbd119..2369cd7b09476 100644
--- a/Mathlib/Order/FixedPoints.lean
+++ b/Mathlib/Order/FixedPoints.lean
@@ -111,9 +111,6 @@ theorem le_gfp {a : α} (h : a ≤ f a) : a ≤ gfp f :=
   le_sSup h
 #align order_hom.le_gfp OrderHom.le_gfp
 
-theorem fixed_le_gfp {a : α} (h : f a = a) : a ≤ gfp f  :=
-  f.le_gfp h.ge
-
 theorem gfp_le {a : α} (h : ∀ b, b ≤ f b → b ≤ a) : gfp f ≤ a :=
   sSup_le h
 #align order_hom.gfp_le OrderHom.gfp_le
diff --git a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean b/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
index a2050ce43a6a6..e6872cfd924b7 100644
--- a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
+++ b/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
@@ -100,7 +100,7 @@ theorem lfpApprox_addition (a : Ordinal.{u}) : f (lfpApprox f a) = lfpApprox f (
 
 /-- The ordinal approximants of the least fixed points are stabilizing
   when reaching a fixed point of f -/
-theorem lfpApprox_stabilizing_at_fp (a : Ordinal.{u}) (h: lfpApprox f a ∈ fixedPoints f):
+theorem lfpApprox_stabilizing_at_fp (a : Ordinal.{u}) (h: lfpApprox f a ∈ fixedPoints f) :
     ∀ b > a, lfpApprox f b = lfpApprox f a := by
   intro b hab; rw[mem_fixedPoints_iff] at h
   induction b using Ordinal.induction with | h b IH =>
@@ -121,7 +121,7 @@ theorem lfpApprox_stabilizing_at_fp (a : Ordinal.{u}) (h: lfpApprox f a ∈ fixe
     use a
 
 /-- Every value after a fixed point of f is also a fixed point of f -/
-theorem lfpApprox_eq_fp (a : Ordinal.{u}) (h: lfpApprox f a ∈ fixedPoints f):
+theorem lfpApprox_eq_fp (a : Ordinal.{u}) (h: lfpApprox f a ∈ fixedPoints f) :
     ∀ b > a, lfpApprox f b ∈ fixedPoints f  := by
   intro b h_ab
   rw[mem_fixedPoints_iff]
@@ -145,7 +145,7 @@ theorem lfpApprox_equal_value : ∃ i < ord <| succ #α, ∃ j < ord <| succ #α
 
 /-- If there are distinct ordinals with equal value then the values are fixed points -/
 lemma lfpApprox_one_fixedPoint (a b : Ordinal.{u}) (h : a < b)
-    (h_fab : lfpApprox f a = lfpApprox f b):
+    (h_fab : lfpApprox f a = lfpApprox f b) :
     lfpApprox f a ∈ fixedPoints f := by
   rw[mem_fixedPoints_iff,lfpApprox_addition]
   apply Monotone.stabilizing (lfpApprox_monotone f)
@@ -154,7 +154,7 @@ lemma lfpApprox_one_fixedPoint (a b : Ordinal.{u}) (h : a < b)
 /-- If there are disctinct ordinals with equal value then
   every value succeding the smaller ordinal are fixed points -/
 lemma lfpApprox_many_fixedPoints (a b : Ordinal.{u}) (h : a < b)
-    (h_fab : lfpApprox f a = lfpApprox f b):
+    (h_fab : lfpApprox f a = lfpApprox f b) :
     ∀ i ≥ a, lfpApprox f i ∈ fixedPoints f := by
   intro i h_i
   obtain rfl | h_ia := eq_or_ne i a
@@ -218,12 +218,12 @@ theorem gfpApprox_addition (a : Ordinal.{u}) : f (gfpApprox f a) = gfpApprox f (
 
 /-- The ordinal approximants of the least fixed points are stabilizing
   when reaching a fixed point of f -/
-theorem gfpApprox_stabilizing_at_fp (a : Ordinal.{u}) (h: gfpApprox f a ∈ fixedPoints f):
+theorem gfpApprox_stabilizing_at_fp (a : Ordinal.{u}) (h: gfpApprox f a ∈ fixedPoints f) :
     ∀ b > a, gfpApprox f b = gfpApprox f a :=
   lfpApprox_stabilizing_at_fp (OrderHom.dual f) a h
 
 /-- Every value after a fixed point of f is also a fixed point of f -/
-theorem gfpApprox_eq_fp (a : Ordinal.{u}) (h: gfpApprox f a ∈ fixedPoints f):
+theorem gfpApprox_eq_fp (a : Ordinal.{u}) (h: gfpApprox f a ∈ fixedPoints f) :
     ∀ b > a, gfpApprox f b ∈ fixedPoints f :=
   lfpApprox_eq_fp (OrderHom.dual f) a h
 
diff --git a/docs/references.bib b/docs/references.bib
index b492a067ef176..3f82147bf770a 100644
--- a/docs/references.bib
+++ b/docs/references.bib
@@ -937,6 +937,17 @@ @Article{         dyckhoff_1992
   doi           = {10.2307/2275431}
 }
 
+@Article{         Echenique2005,
+  author        = {Echenique, Federico},
+  title         = {A short and constructive proof of Tarski’s fixed-point theorem},
+  journal       = {International Journal of Game Theory},
+  volume        = {33},
+  number        = {2},
+  year          = {2005},
+  pages         = {215–218},
+  publisher     = {Springer},
+  doi           = {10.1007/s001820400192}
+}
 @Book{            egno15,
   author        = {Etingof, Pavel and Gelaki, Shlomo and Nikshych, Dmitri and
                   Ostrik, Victor},
@@ -987,17 +998,6 @@ @Article{         elliott2006binomial
   doi           = {10.1016/j.jpaa.2005.09.003}
 }
 
-@Article{         Echenique2005,
-  author        = {Echenique, Federico},
-  title         = {A short and constructive proof of Tarski’s fixed-point theorem},
-  journal       = {International Journal of Game Theory},
-  volume        = {33},
-  number        = {2},
-  year          = {2005},
-  pages         = {215–218},
-  publisher     = {Springer},
-  doi           = {10.1007/s001820400192}
-}
 @Book{            engel1997,
   title         = {Sperner theory},
   author        = {Engel, Konrad},

From 43e1e6127f7cad4d0618fa9f966a0b32ba5ce02b Mon Sep 17 00:00:00 2001
From: Ira Fesefeldt <fesefeldt@cs.rwth-aachen.de>
Date: Sat, 2 Mar 2024 16:12:18 +0100
Subject: [PATCH 10/31] squeezed simps

---
 .../Order/OrdinalApproximantsFixedPoints.lean | 32 +++++++++++++------
 1 file changed, 22 insertions(+), 10 deletions(-)

diff --git a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean b/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
index e6872cfd924b7..fb53bf423cd4b 100644
--- a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
+++ b/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
@@ -59,7 +59,7 @@ theorem not_injective_limitation : ¬ Injective (limitation g) := by
   have h₁ := by apply lift_mk_le_lift_mk_of_injective h_inj
   have mk_initialSeg_subtype :
       #{ i : Ordinal // i < (ord <| succ #α) } = lift.{u+1, u} (succ #α) := by
-    simpa using mk_initialSeg (ord <| succ #α)
+    simpa only [card_typein, Set.coe_setOf, card_ord] using mk_initialSeg (ord <| succ #α)
   rw[mk_initialSeg_subtype, Cardinal.lift_lift, Cardinal.lift_le] at h₁
   have h₂ := not_le_of_lt (Cardinal.succ_lt #α)
   exact h₂ h₁
@@ -83,7 +83,9 @@ decreasing_by exact h
 
 theorem lfpApprox_monotone : Monotone (lfpApprox f) := by
   unfold Monotone; intros a b h; unfold lfpApprox
-  refine sSup_le_sSup ?h; simp
+  refine sSup_le_sSup ?h
+  simp only [exists_prop, Set.setOf_subset_setOf, forall_exists_index,
+    and_imp, forall_apply_eq_imp_iff₂]
   intros a' h'
   use a'
   exact ⟨lt_of_lt_of_le h' h, rfl⟩
@@ -91,10 +93,13 @@ theorem lfpApprox_monotone : Monotone (lfpApprox f) := by
 theorem lfpApprox_addition (a : Ordinal.{u}) : f (lfpApprox f a) = lfpApprox f (a+1) := by
   apply le_antisymm
   · conv => right; unfold lfpApprox
-    apply le_sSup; simp
+    apply le_sSup
+    simp only [Ordinal.add_one_eq_succ, lt_succ_iff, exists_prop, Set.mem_setOf_eq]
     use a
   · conv => left; unfold lfpApprox
-    apply sSup_le; simp
+    apply sSup_le
+    simp only [Ordinal.add_one_eq_succ, lt_succ_iff, exists_prop, Set.mem_setOf_eq,
+      forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
     intros a' h
     apply f.2; apply lfpApprox_monotone; exact h
 
@@ -106,18 +111,22 @@ theorem lfpApprox_stabilizing_at_fp (a : Ordinal.{u}) (h: lfpApprox f a ∈ fixe
   induction b using Ordinal.induction with | h b IH =>
   apply le_antisymm
   · conv => left; unfold lfpApprox
-    apply sSup_le; simp
+    apply sSup_le
+    simp only [exists_prop, Set.mem_setOf_eq, forall_exists_index, and_imp,
+      forall_apply_eq_imp_iff₂]
     intro a' ha'b
     by_cases haa : a' < a
     · rw[lfpApprox_addition]
       apply lfpApprox_monotone
-      simp; exact haa
-    · simp at haa
+      simp only [Ordinal.add_one_eq_succ, succ_le_iff]
+      exact haa
+    · simp only [not_lt] at haa
       cases le_iff_lt_or_eq.mp haa with
       | inl haa => specialize IH a' ha'b haa; rw[IH, h]
       | inr haa => rw[← haa, h]
   · conv => right; unfold lfpApprox
-    apply le_sSup; simp
+    apply le_sSup
+    simp only [exists_prop, Set.mem_setOf_eq]
     use a
 
 /-- Every value after a fixed point of f is also a fixed point of f -/
@@ -180,7 +189,9 @@ theorem lfpApprox_le_fixedPoint : ∀ a : fixedPoints f, ∀ i : Ordinal, lfpApp
   induction i using Ordinal.induction with
   | h i IH =>
     unfold lfpApprox
-    apply sSup_le; simp
+    apply sSup_le
+    simp only [exists_prop, Set.mem_setOf_eq, forall_exists_index, and_imp,
+      forall_apply_eq_imp_iff₂]
     intro j h_j
     rw[← h_a]
     apply f.monotone'
@@ -193,7 +204,8 @@ theorem lfpApprox_cardinal_is_lfp : lfpApprox f (ord <| succ #α) = lfp f := by
     let ⟨x, h_x⟩ := h_lfp; rw[h_x]
     exact lfpApprox_le_fixedPoint f x (ord <| succ #α)
   · have h_fix : ∃ x: fixedPoints f, lfpApprox f (ord <| succ #α) = x := by
-      simpa using lfpApprox_has_fixedPoint_cardinal f
+      simpa only [Subtype.exists, mem_fixedPoints, exists_prop, exists_eq_right'] using
+        lfpApprox_has_fixedPoint_cardinal f
     let ⟨x, h_x⟩ := h_fix; rw[h_x]
     exact lfp_le_fixed f x.prop
 

From 41c79dae962823f7e34a1e9cc5ee76fdaeb4db5d Mon Sep 17 00:00:00 2001
From: Ira Fesefeldt <fesefeldt@cs.rwth-aachen.de>
Date: Sat, 2 Mar 2024 16:15:33 +0100
Subject: [PATCH 11/31] references linting and changed year in license

---
 Mathlib/Order/OrdinalApproximantsFixedPoints.lean | 2 +-
 docs/references.bib                               | 4 +++-
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean b/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
index fb53bf423cd4b..ed584f2fe25a6 100644
--- a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
+++ b/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2023 Ira Fesefeldt. All rights reserved.
+Copyright (c) 2024 Ira Fesefeldt. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ira Fesefeldt
 -/
diff --git a/docs/references.bib b/docs/references.bib
index 3f82147bf770a..e01aff6e5a86b 100644
--- a/docs/references.bib
+++ b/docs/references.bib
@@ -939,7 +939,8 @@ @Article{         dyckhoff_1992
 
 @Article{         Echenique2005,
   author        = {Echenique, Federico},
-  title         = {A short and constructive proof of Tarski’s fixed-point theorem},
+  title         = {A short and constructive proof of Tarski’s fixed-point
+                  theorem},
   journal       = {International Journal of Game Theory},
   volume        = {33},
   number        = {2},
@@ -948,6 +949,7 @@ @Article{         Echenique2005
   publisher     = {Springer},
   doi           = {10.1007/s001820400192}
 }
+
 @Book{            egno15,
   author        = {Etingof, Pavel and Gelaki, Shlomo and Nikshych, Dmitri and
                   Ostrik, Victor},

From 8f8f4d4a4612c7818f4f7168c7da2d116b192800 Mon Sep 17 00:00:00 2001
From: Ira Fesefeldt <fesefeldt@cs.rwth-aachen.de>
Date: Sun, 3 Mar 2024 05:58:02 +0100
Subject: [PATCH 12/31] indeed missed renaming the documentation

---
 Mathlib/Order/OrdinalApproximantsFixedPoints.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean b/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
index ed584f2fe25a6..4e8cbad5c517a 100644
--- a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
+++ b/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
@@ -20,15 +20,15 @@ We loosly follow the proof from [Echenique2005].
 
 ## Main definitions
 
-* `OrdinalApprox.lfp_approx`: The ordinal approximation of
+* `OrdinalApprox.lfpApprox`: The ordinal approximation of
   the least fixed point of a bundled monotone function.
-* `OrdinalApprox.gfp_approx`: The ordinal approximation of
+* `OrdinalApprox.gfpApprox`: The ordinal approximation of
   the greatest fixed point of a bundled monotone function.
 
 ## Main theorems
-* `OrdinalApprox.lfp_is_lfp_approx`: The approximation of
+* `OrdinalApprox.lfp_is_lfpApprox`: The approximation of
   the least fixed point eventually reaches the least fixed point
-* `OrdinalApprox.gfp_is_gfp_approx`: The approximation of
+* `OrdinalApprox.gfp_is_gfpApprox`: The approximation of
   the greatest fixed point eventually reaches the greatest fixed point
 
 ## References

From 77b2fd82322adc0b56b8ab7ff43fa8fdb96b236c Mon Sep 17 00:00:00 2001
From: Ira Fesefeldt <fesefeldt@cs.rwth-aachen.de>
Date: Sun, 3 Mar 2024 06:24:57 +0100
Subject: [PATCH 13/31] changed some of the theorem names

---
 .../Order/OrdinalApproximantsFixedPoints.lean | 40 +++++++++----------
 1 file changed, 20 insertions(+), 20 deletions(-)

diff --git a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean b/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
index 4e8cbad5c517a..8807eefded16b 100644
--- a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
+++ b/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
@@ -105,7 +105,7 @@ theorem lfpApprox_addition (a : Ordinal.{u}) : f (lfpApprox f a) = lfpApprox f (
 
 /-- The ordinal approximants of the least fixed points are stabilizing
   when reaching a fixed point of f -/
-theorem lfpApprox_stabilizing_at_fp (a : Ordinal.{u}) (h: lfpApprox f a ∈ fixedPoints f) :
+theorem lfpApprox_stabilizing_at_fixedPoint (a : Ordinal.{u}) (h: lfpApprox f a ∈ fixedPoints f) :
     ∀ b > a, lfpApprox f b = lfpApprox f a := by
   intro b hab; rw[mem_fixedPoints_iff] at h
   induction b using Ordinal.induction with | h b IH =>
@@ -130,17 +130,17 @@ theorem lfpApprox_stabilizing_at_fp (a : Ordinal.{u}) (h: lfpApprox f a ∈ fixe
     use a
 
 /-- Every value after a fixed point of f is also a fixed point of f -/
-theorem lfpApprox_eq_fp (a : Ordinal.{u}) (h: lfpApprox f a ∈ fixedPoints f) :
-    ∀ b > a, lfpApprox f b ∈ fixedPoints f  := by
+theorem lfpApprox_ordinals_after_fixed_are_fixed (a : Ordinal.{u})
+    (h: lfpApprox f a ∈ fixedPoints f) : ∀ b > a, lfpApprox f b ∈ fixedPoints f  := by
   intro b h_ab
   rw[mem_fixedPoints_iff]
-  have h_stab := lfpApprox_stabilizing_at_fp f a h b h_ab
+  have h_stab := lfpApprox_stabilizing_at_fixedPoint f a h b h_ab
   rw[h_stab]
   exact mem_fixedPoints_iff.mp h
 
 /-- There are distinct ordinals smaller than the successor of the domains cardinals
   with equal value -/
-theorem lfpApprox_equal_value : ∃ i < ord <| succ #α, ∃ j < ord <| succ #α,
+theorem disctinct_ordinal_eq_lfpApprox : ∃ i < ord <| succ #α, ∃ j < ord <| succ #α,
     i ≠ j ∧ lfpApprox f i = lfpApprox f j := by
   have h_ninj := Function.Injective.exists_ne_of_not_injective
     (not_injective_limitation <| lfpApprox f)
@@ -153,7 +153,7 @@ theorem lfpApprox_equal_value : ∃ i < ord <| succ #α, ∃ j < ord <| succ #α
   · exact h_fab
 
 /-- If there are distinct ordinals with equal value then the values are fixed points -/
-lemma lfpApprox_one_fixedPoint (a b : Ordinal.{u}) (h : a < b)
+lemma lfpApprox_has_one_fixedPoint (a b : Ordinal.{u}) (h : a < b)
     (h_fab : lfpApprox f a = lfpApprox f b) :
     lfpApprox f a ∈ fixedPoints f := by
   rw[mem_fixedPoints_iff,lfpApprox_addition]
@@ -162,25 +162,25 @@ lemma lfpApprox_one_fixedPoint (a b : Ordinal.{u}) (h : a < b)
 
 /-- If there are disctinct ordinals with equal value then
   every value succeding the smaller ordinal are fixed points -/
-lemma lfpApprox_many_fixedPoints (a b : Ordinal.{u}) (h : a < b)
+lemma lfpApprox_has_many_fixedPoints (a b : Ordinal.{u}) (h : a < b)
     (h_fab : lfpApprox f a = lfpApprox f b) :
     ∀ i ≥ a, lfpApprox f i ∈ fixedPoints f := by
   intro i h_i
   obtain rfl | h_ia := eq_or_ne i a
-  · exact lfpApprox_one_fixedPoint f i b h h_fab
-  · apply lfpApprox_eq_fp f a
-    · exact lfpApprox_one_fixedPoint f a b h h_fab
+  · exact lfpApprox_has_one_fixedPoint f i b h h_fab
+  · apply ordinals_after_fixed_are_fixed f a
+    · exact lfpApprox_has_one_fixedPoint f a b h h_fab
     · exact Ne.lt_of_le' h_ia h_i
 
 /-- A fixed point of f is reached after the successor of the domains cardinality -/
 theorem lfpApprox_has_fixedPoint_cardinal : lfpApprox f (ord <| succ #α) ∈ fixedPoints f := by
-  let ⟨a, h_a, b, h_b, h_nab, h_fab⟩ := lfpApprox_equal_value f
+  let ⟨a, h_a, b, h_b, h_nab, h_fab⟩ := disctinct_ordinal_eq_lfpApprox f
   cases le_total a b with
   | inl h_ab =>
-    exact lfpApprox_many_fixedPoints f a b (h_nab.lt_of_le h_ab) h_fab
+    exact lfpApprox_has_many_fixedPoints f a b (h_nab.lt_of_le h_ab) h_fab
       (ord <| succ #α) (le_of_lt h_a)
   | inr h_ba =>
-    exact lfpApprox_many_fixedPoints f b a (h_nab.symm.lt_of_le h_ba)
+    exact lfpApprox_has_many_fixedPoints f b a (h_nab.symm.lt_of_le h_ba)
       (h_fab.symm) (ord <| succ #α) (le_of_lt h_b)
 
 /-- Every value of the ordinal approximants are less or equal than every fixed point of f -/
@@ -230,20 +230,20 @@ theorem gfpApprox_addition (a : Ordinal.{u}) : f (gfpApprox f a) = gfpApprox f (
 
 /-- The ordinal approximants of the least fixed points are stabilizing
   when reaching a fixed point of f -/
-theorem gfpApprox_stabilizing_at_fp (a : Ordinal.{u}) (h: gfpApprox f a ∈ fixedPoints f) :
+theorem gfpApprox_stabilizing_at_fixedPoint (a : Ordinal.{u}) (h: gfpApprox f a ∈ fixedPoints f) :
     ∀ b > a, gfpApprox f b = gfpApprox f a :=
-  lfpApprox_stabilizing_at_fp (OrderHom.dual f) a h
+  lfpApprox_stabilizing_at_fixedPoint (OrderHom.dual f) a h
 
 /-- Every value after a fixed point of f is also a fixed point of f -/
-theorem gfpApprox_eq_fp (a : Ordinal.{u}) (h: gfpApprox f a ∈ fixedPoints f) :
-    ∀ b > a, gfpApprox f b ∈ fixedPoints f :=
-  lfpApprox_eq_fp (OrderHom.dual f) a h
+theorem gfpApprox_ordinals_after_fixed_are_fixed (a : Ordinal.{u})
+    (h: gfpApprox f a ∈ fixedPoints f) : ∀ b > a, gfpApprox f b ∈ fixedPoints f :=
+  lfpApprox_ordinals_after_fixed_are_fixed (OrderHom.dual f) a h
 
 /-- There are distinct ordinals smaller than the successor of the domains cardinals with
   equal value -/
-theorem gfpApprox_equal_value : ∃ i < ord <| succ #α, ∃ j < ord <| succ #α,
+theorem disctinct_ordinal_eq_gfpApprox : ∃ i < ord <| succ #α, ∃ j < ord <| succ #α,
     i ≠ j ∧ gfpApprox f i = gfpApprox f j :=
-  lfpApprox_equal_value (OrderHom.dual f)
+  disctinct_ordinal_eq_lfpApprox (OrderHom.dual f)
 
 /-- A fixed point of f is reached after the successor of the domains cardinality -/
 lemma gfpApprox_has_fixedPoint_cardinal : gfpApprox f (ord <| succ #α) ∈ fixedPoints f :=

From f4094342e4236843491ddc790912753157e5fc69 Mon Sep 17 00:00:00 2001
From: Ira Fesefeldt <fesefeldt@cs.rwth-aachen.de>
Date: Tue, 5 Mar 2024 09:21:11 +0100
Subject: [PATCH 14/31] fixed wrong name

---
 Mathlib/Order/OrdinalApproximantsFixedPoints.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean b/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
index 8807eefded16b..75791fff5847a 100644
--- a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
+++ b/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
@@ -168,7 +168,7 @@ lemma lfpApprox_has_many_fixedPoints (a b : Ordinal.{u}) (h : a < b)
   intro i h_i
   obtain rfl | h_ia := eq_or_ne i a
   · exact lfpApprox_has_one_fixedPoint f i b h h_fab
-  · apply ordinals_after_fixed_are_fixed f a
+  · apply lfpApprox_ordinals_after_fixed_are_fixed f a
     · exact lfpApprox_has_one_fixedPoint f a b h h_fab
     · exact Ne.lt_of_le' h_ia h_i
 

From 951ec456c3c73a92c1ae7387ab72dad2e36da643 Mon Sep 17 00:00:00 2001
From: Ira Fesefeldt <fesefeldt@cs.rwth-aachen.de>
Date: Thu, 7 Mar 2024 09:48:58 +0100
Subject: [PATCH 15/31] removed uncessary theorems and fixed documentation

---
 Mathlib/Order/OrdinalApproximantsFixedPoints.lean | 6 +++---
 Mathlib/SetTheory/Cardinal/Basic.lean             | 8 --------
 2 files changed, 3 insertions(+), 11 deletions(-)

diff --git a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean b/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
index 75791fff5847a..39bff8949a80e 100644
--- a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
+++ b/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
@@ -26,9 +26,9 @@ We loosly follow the proof from [Echenique2005].
   the greatest fixed point of a bundled monotone function.
 
 ## Main theorems
-* `OrdinalApprox.lfp_is_lfpApprox`: The approximation of
+* `OrdinalApprox.lfpApprox_is_lfp`: The approximation of
   the least fixed point eventually reaches the least fixed point
-* `OrdinalApprox.gfp_is_gfpApprox`: The approximation of
+* `OrdinalApprox.gfpApprox_is_gfp`: The approximation of
   the greatest fixed point eventually reaches the greatest fixed point
 
 ## References
@@ -61,7 +61,7 @@ theorem not_injective_limitation : ¬ Injective (limitation g) := by
       #{ i : Ordinal // i < (ord <| succ #α) } = lift.{u+1, u} (succ #α) := by
     simpa only [card_typein, Set.coe_setOf, card_ord] using mk_initialSeg (ord <| succ #α)
   rw[mk_initialSeg_subtype, Cardinal.lift_lift, Cardinal.lift_le] at h₁
-  have h₂ := not_le_of_lt (Cardinal.succ_lt #α)
+  have h₂ := not_le_of_lt (Order.lt_succ #α)
   exact h₂ h₁
 
 end Cardinal
diff --git a/Mathlib/SetTheory/Cardinal/Basic.lean b/Mathlib/SetTheory/Cardinal/Basic.lean
index 99a6949a73a1b..427c309750f38 100644
--- a/Mathlib/SetTheory/Cardinal/Basic.lean
+++ b/Mathlib/SetTheory/Cardinal/Basic.lean
@@ -830,14 +830,6 @@ theorem add_one_le_succ (c : Cardinal.{u}) : c + 1 ≤ succ c := by
     _ ≤ #β := (f.optionElim b hb).cardinal_le
 #align cardinal.add_one_le_succ Cardinal.add_one_le_succ
 
-theorem not_isMax (ℵ : Cardinal) : ¬ IsMax ℵ := by
-  intro h
-  unfold IsMax at h
-  specialize h (cantor ℵ).le
-  exact not_lt_of_le h (cantor ℵ)
-
-theorem succ_lt (ℵ : Cardinal) : ℵ < succ ℵ := Order.lt_succ_of_not_isMax (not_isMax ℵ)
-
 /-- A cardinal is a limit if it is not zero or a successor cardinal. Note that `ℵ₀` is a limit
   cardinal by this definition, but `0` isn't.
 

From e78b0046ec137d46eb91767fa7be5709e8f26251 Mon Sep 17 00:00:00 2001
From: Ira Fesefeldt <public@feuervogel.me>
Date: Mon, 18 Mar 2024 09:50:01 +0100
Subject: [PATCH 16/31] style and not_injective_iff enhanced

---
 Mathlib/Logic/Function/Basic.lean             |  6 +--
 Mathlib/Order/Monotone/Basic.lean             | 14 +++---
 .../Order/OrdinalApproximantsFixedPoints.lean | 47 ++++++++++---------
 3 files changed, 32 insertions(+), 35 deletions(-)

diff --git a/Mathlib/Logic/Function/Basic.lean b/Mathlib/Logic/Function/Basic.lean
index f0aab4138733f..ebb9f39c82a0a 100644
--- a/Mathlib/Logic/Function/Basic.lean
+++ b/Mathlib/Logic/Function/Basic.lean
@@ -107,10 +107,8 @@ theorem Injective.ne_iff' (hf : Injective f) {x y : α} {z : β} (h : f y = z) :
   h ▸ hf.ne_iff
 #align function.injective.ne_iff' Function.Injective.ne_iff'
 
-theorem Injective.exists_ne_of_not_injective (h: ¬ Injective f) : ∃ a b, a ≠ b ∧ f a = f b := by
-  unfold Injective at h; simp only [not_forall, exists_prop] at h
-  let ⟨a, b, h_f, h_ab⟩ := h
-  exact ⟨a, b, h_ab, h_f⟩
+theorem not_injective_iff : ¬ Injective f ↔ ∃ a b, f a = f b ∧ a ≠ b := by
+  simp only [Injective, not_forall, exists_prop]
 
 /-- If the co-domain `β` of an injective function `f : α → β` has decidable equality, then
 the domain `α` also has decidable equality. -/
diff --git a/Mathlib/Order/Monotone/Basic.lean b/Mathlib/Order/Monotone/Basic.lean
index 61f7d8bcd5661..4d3fa546e69eb 100644
--- a/Mathlib/Order/Monotone/Basic.lean
+++ b/Mathlib/Order/Monotone/Basic.lean
@@ -920,20 +920,18 @@ theorem Antitone.strictAnti_iff_injective (hf : Antitone f) : StrictAnti f ↔ I
 #align antitone.strict_anti_iff_injective Antitone.strictAnti_iff_injective
 
 /-- If a monotone function is equal at two points, it is equal between all of them -/
-theorem Monotone.stabilizing {a₁ a₂ : α} (h_mon : Monotone f) (h_fa : f a₁ = f a₂) :
-    ∀ i, a₂ ≥ i → i ≥ a₁ → f i = f a₁ := by
-  intro i h₂ h₁
+theorem Monotone.eq_of_le_of_le {a₁ a₂ : α} (h_mon : Monotone f) (h_fa : f a₁ = f a₂) {i : α}
+    (h₁ : a₁ ≤ i) (h₂ : i ≤ a₂) : f i = f a₁ := by
   apply le_antisymm
-  · rw[h_fa]; exact h_mon h₂
+  · rw [h_fa]; exact h_mon h₂
   · exact h_mon h₁
 
 /-- If an antitone function is equal at two points, it is equal between all of them -/
-theorem Antitone.stabilizing {a₁ a₂ : α} (h_anti : Antitone f) (h_fa : f a₁ = f a₂) :
-    ∀ i, a₂ ≥ i → i ≥ a₁ → f i = f a₁ := by
-  intro i h₂ h₁
+theorem Antitone.eq_of_le_of_le {a₁ a₂ : α} (h_anti : Antitone f) (h_fa : f a₁ = f a₂) {i : α}
+   (h₁ : a₁ ≤ i) (h₂ : i ≤ a₂) : f i = f a₁ := by
   apply le_antisymm
   · exact h_anti h₁
-  · rw[h_fa]; exact h_anti h₂
+  · rw [h_fa]; exact h_anti h₂
 
 end PartialOrder
 
diff --git a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean b/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
index 39bff8949a80e..c3b87fd829c6a 100644
--- a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
+++ b/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
@@ -15,8 +15,10 @@ import Mathlib.SetTheory.Ordinal.Arithmetic
 
 This file sets up the ordinal approximation theory of fixed points
 of a monotone function in a complete lattice [Cousot1979].
+The proof follows loosely the one from [Echenique2005].
 
-We loosly follow the proof from [Echenique2005].
+However, the proof given here is not constructive as we use the non-constructive axiomatization of
+ordinals from mathlib. It still allows an approximation scheme indexed over the ordinals.
 
 ## Main definitions
 
@@ -44,7 +46,7 @@ namespace Cardinal
 
 universe u
 variable {α : Type u}
-variable (g: Ordinal → α)
+variable (g : Ordinal → α)
 
 open Cardinal Ordinal SuccOrder Function
 
@@ -60,7 +62,7 @@ theorem not_injective_limitation : ¬ Injective (limitation g) := by
   have mk_initialSeg_subtype :
       #{ i : Ordinal // i < (ord <| succ #α) } = lift.{u+1, u} (succ #α) := by
     simpa only [card_typein, Set.coe_setOf, card_ord] using mk_initialSeg (ord <| succ #α)
-  rw[mk_initialSeg_subtype, Cardinal.lift_lift, Cardinal.lift_le] at h₁
+  rw [mk_initialSeg_subtype, Cardinal.lift_lift, Cardinal.lift_le] at h₁
   have h₂ := not_le_of_lt (Order.lt_succ #α)
   exact h₂ h₁
 
@@ -107,7 +109,7 @@ theorem lfpApprox_addition (a : Ordinal.{u}) : f (lfpApprox f a) = lfpApprox f (
   when reaching a fixed point of f -/
 theorem lfpApprox_stabilizing_at_fixedPoint (a : Ordinal.{u}) (h: lfpApprox f a ∈ fixedPoints f) :
     ∀ b > a, lfpApprox f b = lfpApprox f a := by
-  intro b hab; rw[mem_fixedPoints_iff] at h
+  intro b hab; rw [mem_fixedPoints_iff] at h
   induction b using Ordinal.induction with | h b IH =>
   apply le_antisymm
   · conv => left; unfold lfpApprox
@@ -116,14 +118,14 @@ theorem lfpApprox_stabilizing_at_fixedPoint (a : Ordinal.{u}) (h: lfpApprox f a
       forall_apply_eq_imp_iff₂]
     intro a' ha'b
     by_cases haa : a' < a
-    · rw[lfpApprox_addition]
+    · rw [lfpApprox_addition]
       apply lfpApprox_monotone
       simp only [Ordinal.add_one_eq_succ, succ_le_iff]
       exact haa
     · simp only [not_lt] at haa
       cases le_iff_lt_or_eq.mp haa with
-      | inl haa => specialize IH a' ha'b haa; rw[IH, h]
-      | inr haa => rw[← haa, h]
+      | inl haa => specialize IH a' ha'b haa; rw [IH, h]
+      | inr haa => rw [← haa, h]
   · conv => right; unfold lfpApprox
     apply le_sSup
     simp only [exists_prop, Set.mem_setOf_eq]
@@ -131,11 +133,11 @@ theorem lfpApprox_stabilizing_at_fixedPoint (a : Ordinal.{u}) (h: lfpApprox f a
 
 /-- Every value after a fixed point of f is also a fixed point of f -/
 theorem lfpApprox_ordinals_after_fixed_are_fixed (a : Ordinal.{u})
-    (h: lfpApprox f a ∈ fixedPoints f) : ∀ b > a, lfpApprox f b ∈ fixedPoints f  := by
+    (h : lfpApprox f a ∈ fixedPoints f) : ∀ b > a, lfpApprox f b ∈ fixedPoints f  := by
   intro b h_ab
-  rw[mem_fixedPoints_iff]
+  rw [mem_fixedPoints_iff]
   have h_stab := lfpApprox_stabilizing_at_fixedPoint f a h b h_ab
-  rw[h_stab]
+  rw [h_stab]
   exact mem_fixedPoints_iff.mp h
 
 /-- There are distinct ordinals smaller than the successor of the domains cardinals
@@ -145,18 +147,18 @@ theorem disctinct_ordinal_eq_lfpApprox : ∃ i < ord <| succ #α, ∃ j < ord <|
   have h_ninj := Function.Injective.exists_ne_of_not_injective
     (not_injective_limitation <| lfpApprox f)
   let ⟨a, b, h_nab, h_fab⟩ := h_ninj
-  rw[limitation_def, limitation_def] at h_fab
+  rw [limitation_def, limitation_def] at h_fab
   use a.val; apply And.intro a.prop
   use b.val; apply And.intro b.prop
   apply And.intro
-  · intro h_eq; rw[Subtype.coe_inj] at h_eq; exact h_nab h_eq
+  · intro h_eq; rw [Subtype.coe_inj] at h_eq; exact h_nab h_eq
   · exact h_fab
 
 /-- If there are distinct ordinals with equal value then the values are fixed points -/
 lemma lfpApprox_has_one_fixedPoint (a b : Ordinal.{u}) (h : a < b)
     (h_fab : lfpApprox f a = lfpApprox f b) :
     lfpApprox f a ∈ fixedPoints f := by
-  rw[mem_fixedPoints_iff,lfpApprox_addition]
+  rw [mem_fixedPoints_iff,lfpApprox_addition]
   apply Monotone.stabilizing (lfpApprox_monotone f)
     h_fab (a+1) (SuccOrder.succ_le_of_lt h) (SuccOrder.le_succ a)
 
@@ -193,7 +195,7 @@ theorem lfpApprox_le_fixedPoint : ∀ a : fixedPoints f, ∀ i : Ordinal, lfpApp
     simp only [exists_prop, Set.mem_setOf_eq, forall_exists_index, and_imp,
       forall_apply_eq_imp_iff₂]
     intro j h_j
-    rw[← h_a]
+    rw [← h_a]
     apply f.monotone'
     exact IH j h_j
 
@@ -201,16 +203,16 @@ theorem lfpApprox_le_fixedPoint : ∀ a : fixedPoints f, ∀ i : Ordinal, lfpApp
 theorem lfpApprox_cardinal_is_lfp : lfpApprox f (ord <| succ #α) = lfp f := by
   apply le_antisymm
   · have h_lfp : ∃ x : fixedPoints f, lfp f = x := by use ⊥; exact rfl
-    let ⟨x, h_x⟩ := h_lfp; rw[h_x]
+    let ⟨x, h_x⟩ := h_lfp; rw [h_x]
     exact lfpApprox_le_fixedPoint f x (ord <| succ #α)
-  · have h_fix : ∃ x: fixedPoints f, lfpApprox f (ord <| succ #α) = x := by
+  · have h_fix : ∃ x : fixedPoints f, lfpApprox f (ord <| succ #α) = x := by
       simpa only [Subtype.exists, mem_fixedPoints, exists_prop, exists_eq_right'] using
         lfpApprox_has_fixedPoint_cardinal f
-    let ⟨x, h_x⟩ := h_fix; rw[h_x]
+    let ⟨x, h_x⟩ := h_fix; rw [h_x]
     exact lfp_le_fixed f x.prop
 
-/-- **Constructive Knaster-Tarski Theorem**: Some ordinal approximation of the least fixed point
-  is the least fixed point. Also known as ordinal approximation of the least fixed point.-/
+/-- Some ordinal approximation of the least fixed point is the least fixed point.
+  Also known as ordinal approximation of the least fixed point.-/
 theorem lfpApprox_is_lfp : ∃ a : Ordinal, lfpApprox f a = lfp f := by
   use (ord <| succ #α)
   exact lfpApprox_cardinal_is_lfp f
@@ -230,7 +232,7 @@ theorem gfpApprox_addition (a : Ordinal.{u}) : f (gfpApprox f a) = gfpApprox f (
 
 /-- The ordinal approximants of the least fixed points are stabilizing
   when reaching a fixed point of f -/
-theorem gfpApprox_stabilizing_at_fixedPoint (a : Ordinal.{u}) (h: gfpApprox f a ∈ fixedPoints f) :
+theorem gfpApprox_stabilizing_at_fixedPoint (a : Ordinal.{u}) (h : gfpApprox f a ∈ fixedPoints f) :
     ∀ b > a, gfpApprox f b = gfpApprox f a :=
   lfpApprox_stabilizing_at_fixedPoint (OrderHom.dual f) a h
 
@@ -257,9 +259,8 @@ lemma gfpApprox_ge_fixedPoint : ∀ a : fixedPoints f, ∀ i : Ordinal, gfpAppro
 theorem gfpApprox_cardinal_is_gfp : gfpApprox f (ord <| succ #α) = gfp f :=
   lfpApprox_cardinal_is_lfp (OrderHom.dual f)
 
-/-- **Dual Constructive Knaster-Tarski Theorem**: Some ordinal approximation of
-  the greatest fixed point is the greatest fixed point. Also known as ordinal approximation of
-  the greatest fixed point.-/
+/-- Some ordinal approximation of the greatest fixed point is the greatest fixed point.
+  Also known as ordinal approximation of the greatest fixed point.-/
 theorem gfpApprox_is_gfp : ∃ a : Ordinal, gfpApprox f a = gfp f :=
   lfpApprox_is_lfp (OrderHom.dual f)
 

From a5b9bb238f12aa1abf92659e006cefce9fc32929 Mon Sep 17 00:00:00 2001
From: Ira Fesefeldt <public@feuervogel.me>
Date: Mon, 18 Mar 2024 13:29:40 +0100
Subject: [PATCH 17/31] changed limitation to Set.InjOn

---
 .../Order/OrdinalApproximantsFixedPoints.lean | 56 +++++++++----------
 1 file changed, 25 insertions(+), 31 deletions(-)

diff --git a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean b/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
index c3b87fd829c6a..79eb49cb8794e 100644
--- a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
+++ b/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
@@ -48,23 +48,18 @@ universe u
 variable {α : Type u}
 variable (g : Ordinal → α)
 
-open Cardinal Ordinal SuccOrder Function
+open Cardinal Ordinal SuccOrder Function Set
 
-/-- Limitation of an ordinal defined function to the initial segment
-  containing the codomains cardinality -/
-def limitation : { i : Ordinal // i < (ord <| succ #α) } → α := fun i => g i
-
-theorem limitation_def (i : { i : Ordinal // i < (ord <| succ #α) }) : limitation g i = g i := rfl
-
-theorem not_injective_limitation : ¬ Injective (limitation g) := by
+theorem not_injective_limitation_set : ¬ Set.InjOn g (Set.Iio (ord <| succ #α)) := by
   intro h_inj
-  have h₁ := by apply lift_mk_le_lift_mk_of_injective h_inj
+  have h := lift_mk_le_lift_mk_of_injective <| Set.injOn_iff_injective.1 h_inj
   have mk_initialSeg_subtype :
-      #{ i : Ordinal // i < (ord <| succ #α) } = lift.{u+1, u} (succ #α) := by
-    simpa only [card_typein, Set.coe_setOf, card_ord] using mk_initialSeg (ord <| succ #α)
-  rw [mk_initialSeg_subtype, Cardinal.lift_lift, Cardinal.lift_le] at h₁
-  have h₂ := not_le_of_lt (Order.lt_succ #α)
-  exact h₂ h₁
+      #(Iio (ord <| succ #α)) = lift.{u+1, u} (succ #α) := by
+    simpa only [coe_setOf, card_typein, card_ord] using mk_initialSeg (ord <| succ #α)
+  rw [mk_initialSeg_subtype, Cardinal.lift_lift, Cardinal.lift_le] at h
+  exact not_le_of_lt (Order.lt_succ #α) h
+
+
 
 end Cardinal
 
@@ -144,34 +139,33 @@ theorem lfpApprox_ordinals_after_fixed_are_fixed (a : Ordinal.{u})
   with equal value -/
 theorem disctinct_ordinal_eq_lfpApprox : ∃ i < ord <| succ #α, ∃ j < ord <| succ #α,
     i ≠ j ∧ lfpApprox f i = lfpApprox f j := by
-  have h_ninj := Function.Injective.exists_ne_of_not_injective
-    (not_injective_limitation <| lfpApprox f)
-  let ⟨a, b, h_nab, h_fab⟩ := h_ninj
-  rw [limitation_def, limitation_def] at h_fab
+  -- have h_ninj := Function.not_injective_iff.1
+  --   ( Set.injOn_iff_injective.1 <| not_injective_limitation_set <| lfpApprox f)
+  have h_ninj := not_injective_limitation_set <| lfpApprox f
+  rw [Set.injOn_iff_injective, Function.not_injective_iff] at h_ninj
+  let ⟨a, b, h_fab, h_nab⟩ := h_ninj
   use a.val; apply And.intro a.prop
   use b.val; apply And.intro b.prop
   apply And.intro
   · intro h_eq; rw [Subtype.coe_inj] at h_eq; exact h_nab h_eq
   · exact h_fab
 
-/-- If there are distinct ordinals with equal value then the values are fixed points -/
-lemma lfpApprox_has_one_fixedPoint (a b : Ordinal.{u}) (h : a < b)
-    (h_fab : lfpApprox f a = lfpApprox f b) :
-    lfpApprox f a ∈ fixedPoints f := by
-  rw [mem_fixedPoints_iff,lfpApprox_addition]
-  apply Monotone.stabilizing (lfpApprox_monotone f)
-    h_fab (a+1) (SuccOrder.succ_le_of_lt h) (SuccOrder.le_succ a)
-
 /-- If there are disctinct ordinals with equal value then
   every value succeding the smaller ordinal are fixed points -/
-lemma lfpApprox_has_many_fixedPoints (a b : Ordinal.{u}) (h : a < b)
+lemma lfpApprox_mem_fixedPoints_of_eq (a b : Ordinal.{u}) (h : a < b)
     (h_fab : lfpApprox f a = lfpApprox f b) :
     ∀ i ≥ a, lfpApprox f i ∈ fixedPoints f := by
   intro i h_i
+  have lfpApprox_has_one_fixedPoint (c d : Ordinal.{u}) (h : c < d)
+      (h_fab : lfpApprox f c = lfpApprox f d) :
+      lfpApprox f c ∈ fixedPoints f := by
+    rw [mem_fixedPoints_iff, lfpApprox_addition]
+    exact Monotone.eq_of_le_of_le (lfpApprox_monotone f)
+      h_fab (SuccOrder.le_succ c) (SuccOrder.succ_le_of_lt h)
   obtain rfl | h_ia := eq_or_ne i a
-  · exact lfpApprox_has_one_fixedPoint f i b h h_fab
+  · exact lfpApprox_has_one_fixedPoint i b h h_fab
   · apply lfpApprox_ordinals_after_fixed_are_fixed f a
-    · exact lfpApprox_has_one_fixedPoint f a b h h_fab
+    · exact lfpApprox_has_one_fixedPoint a b h h_fab
     · exact Ne.lt_of_le' h_ia h_i
 
 /-- A fixed point of f is reached after the successor of the domains cardinality -/
@@ -179,10 +173,10 @@ theorem lfpApprox_has_fixedPoint_cardinal : lfpApprox f (ord <| succ #α) ∈ fi
   let ⟨a, h_a, b, h_b, h_nab, h_fab⟩ := disctinct_ordinal_eq_lfpApprox f
   cases le_total a b with
   | inl h_ab =>
-    exact lfpApprox_has_many_fixedPoints f a b (h_nab.lt_of_le h_ab) h_fab
+    exact lfpApprox_mem_fixedPoints_of_eq f a b (h_nab.lt_of_le h_ab) h_fab
       (ord <| succ #α) (le_of_lt h_a)
   | inr h_ba =>
-    exact lfpApprox_has_many_fixedPoints f b a (h_nab.symm.lt_of_le h_ba)
+    exact lfpApprox_mem_fixedPoints_of_eq f b a (h_nab.symm.lt_of_le h_ba)
       (h_fab.symm) (ord <| succ #α) (le_of_lt h_b)
 
 /-- Every value of the ordinal approximants are less or equal than every fixed point of f -/

From 483c2831e1526263fdbdc87fc6ef7cacf25ed189 Mon Sep 17 00:00:00 2001
From: Ira Fesefeldt <public@feuervogel.me>
Date: Mon, 18 Mar 2024 14:31:11 +0100
Subject: [PATCH 18/31] pr comments

---
 .../Order/OrdinalApproximantsFixedPoints.lean | 106 ++++++++----------
 1 file changed, 45 insertions(+), 61 deletions(-)

diff --git a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean b/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
index 79eb49cb8794e..38e2ad1ab7919 100644
--- a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
+++ b/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
@@ -87,24 +87,24 @@ theorem lfpApprox_monotone : Monotone (lfpApprox f) := by
   use a'
   exact ⟨lt_of_lt_of_le h' h, rfl⟩
 
-theorem lfpApprox_addition (a : Ordinal.{u}) : f (lfpApprox f a) = lfpApprox f (a+1) := by
+theorem lfpApprox_add_one (a : Ordinal.{u}) : lfpApprox f (a+1) = f (lfpApprox f a) := by
   apply le_antisymm
-  · conv => right; unfold lfpApprox
-    apply le_sSup
-    simp only [Ordinal.add_one_eq_succ, lt_succ_iff, exists_prop, Set.mem_setOf_eq]
-    use a
   · conv => left; unfold lfpApprox
     apply sSup_le
     simp only [Ordinal.add_one_eq_succ, lt_succ_iff, exists_prop, Set.mem_setOf_eq,
       forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
     intros a' h
     apply f.2; apply lfpApprox_monotone; exact h
+  · conv => right; unfold lfpApprox
+    apply le_sSup
+    simp only [Ordinal.add_one_eq_succ, lt_succ_iff, exists_prop, Set.mem_setOf_eq]
+    use a
 
 /-- The ordinal approximants of the least fixed points are stabilizing
   when reaching a fixed point of f -/
-theorem lfpApprox_stabilizing_at_fixedPoint (a : Ordinal.{u}) (h: lfpApprox f a ∈ fixedPoints f) :
-    ∀ b > a, lfpApprox f b = lfpApprox f a := by
-  intro b hab; rw [mem_fixedPoints_iff] at h
+theorem lfpApprox_eq_of_mem_fixedPoint {a b : Ordinal.{u}} (h_ab : a < b)
+    (h: lfpApprox f a ∈ fixedPoints f) : lfpApprox f b = lfpApprox f a := by
+  rw [mem_fixedPoints_iff] at h
   induction b using Ordinal.induction with | h b IH =>
   apply le_antisymm
   · conv => left; unfold lfpApprox
@@ -113,7 +113,7 @@ theorem lfpApprox_stabilizing_at_fixedPoint (a : Ordinal.{u}) (h: lfpApprox f a
       forall_apply_eq_imp_iff₂]
     intro a' ha'b
     by_cases haa : a' < a
-    · rw [lfpApprox_addition]
+    · rw [← lfpApprox_add_one]
       apply lfpApprox_monotone
       simp only [Ordinal.add_one_eq_succ, succ_le_iff]
       exact haa
@@ -121,26 +121,12 @@ theorem lfpApprox_stabilizing_at_fixedPoint (a : Ordinal.{u}) (h: lfpApprox f a
       cases le_iff_lt_or_eq.mp haa with
       | inl haa => specialize IH a' ha'b haa; rw [IH, h]
       | inr haa => rw [← haa, h]
-  · conv => right; unfold lfpApprox
-    apply le_sSup
-    simp only [exists_prop, Set.mem_setOf_eq]
-    use a
-
-/-- Every value after a fixed point of f is also a fixed point of f -/
-theorem lfpApprox_ordinals_after_fixed_are_fixed (a : Ordinal.{u})
-    (h : lfpApprox f a ∈ fixedPoints f) : ∀ b > a, lfpApprox f b ∈ fixedPoints f  := by
-  intro b h_ab
-  rw [mem_fixedPoints_iff]
-  have h_stab := lfpApprox_stabilizing_at_fixedPoint f a h b h_ab
-  rw [h_stab]
-  exact mem_fixedPoints_iff.mp h
+  · exact lfpApprox_monotone f (le_of_lt h_ab)
 
 /-- There are distinct ordinals smaller than the successor of the domains cardinals
   with equal value -/
-theorem disctinct_ordinal_eq_lfpApprox : ∃ i < ord <| succ #α, ∃ j < ord <| succ #α,
-    i ≠ j ∧ lfpApprox f i = lfpApprox f j := by
-  -- have h_ninj := Function.not_injective_iff.1
-  --   ( Set.injOn_iff_injective.1 <| not_injective_limitation_set <| lfpApprox f)
+theorem distinct_ordinal_eq_lfpApprox : ∃ a < ord <| succ #α, ∃ b < ord <| succ #α,
+    a ≠ b ∧ lfpApprox f a = lfpApprox f b := by
   have h_ninj := not_injective_limitation_set <| lfpApprox f
   rw [Set.injOn_iff_injective, Function.not_injective_iff] at h_ninj
   let ⟨a, b, h_fab, h_nab⟩ := h_ninj
@@ -150,38 +136,36 @@ theorem disctinct_ordinal_eq_lfpApprox : ∃ i < ord <| succ #α, ∃ j < ord <|
   · intro h_eq; rw [Subtype.coe_inj] at h_eq; exact h_nab h_eq
   · exact h_fab
 
-/-- If there are disctinct ordinals with equal value then
+/-- If there are distinct ordinals with equal value then
   every value succeding the smaller ordinal are fixed points -/
-lemma lfpApprox_mem_fixedPoints_of_eq (a b : Ordinal.{u}) (h : a < b)
+lemma lfpApprox_mem_fixedPoints_of_eq {a b c : Ordinal.{u}} (h_ab : a < b) (h_ac : a ≤ c)
     (h_fab : lfpApprox f a = lfpApprox f b) :
-    ∀ i ≥ a, lfpApprox f i ∈ fixedPoints f := by
-  intro i h_i
-  have lfpApprox_has_one_fixedPoint (c d : Ordinal.{u}) (h : c < d)
-      (h_fab : lfpApprox f c = lfpApprox f d) :
-      lfpApprox f c ∈ fixedPoints f := by
-    rw [mem_fixedPoints_iff, lfpApprox_addition]
+    lfpApprox f c ∈ fixedPoints f := by
+  have lfpApprox_has_one_fixedPoint {d e : Ordinal.{u}} (h : d < e)
+      (h_fab : lfpApprox f d = lfpApprox f e) :
+      lfpApprox f d ∈ fixedPoints f := by
+    rw [mem_fixedPoints_iff, ← lfpApprox_add_one]
     exact Monotone.eq_of_le_of_le (lfpApprox_monotone f)
-      h_fab (SuccOrder.le_succ c) (SuccOrder.succ_le_of_lt h)
-  obtain rfl | h_ia := eq_or_ne i a
-  · exact lfpApprox_has_one_fixedPoint i b h h_fab
-  · apply lfpApprox_ordinals_after_fixed_are_fixed f a
-    · exact lfpApprox_has_one_fixedPoint a b h h_fab
-    · exact Ne.lt_of_le' h_ia h_i
+      h_fab (SuccOrder.le_succ d) (SuccOrder.succ_le_of_lt h)
+  obtain rfl | h_eq_ne := eq_or_ne c a
+  · exact lfpApprox_has_one_fixedPoint h_ab h_fab
+  · rw [lfpApprox_eq_of_mem_fixedPoint f]
+    · exact lfpApprox_has_one_fixedPoint h_ab h_fab
+    · exact Ne.lt_of_le' h_eq_ne h_ac
+    · exact lfpApprox_has_one_fixedPoint h_ab h_fab
 
 /-- A fixed point of f is reached after the successor of the domains cardinality -/
 theorem lfpApprox_has_fixedPoint_cardinal : lfpApprox f (ord <| succ #α) ∈ fixedPoints f := by
-  let ⟨a, h_a, b, h_b, h_nab, h_fab⟩ := disctinct_ordinal_eq_lfpApprox f
+  let ⟨a, h_a, b, h_b, h_nab, h_fab⟩ := distinct_ordinal_eq_lfpApprox f
   cases le_total a b with
   | inl h_ab =>
-    exact lfpApprox_mem_fixedPoints_of_eq f a b (h_nab.lt_of_le h_ab) h_fab
-      (ord <| succ #α) (le_of_lt h_a)
+    exact lfpApprox_mem_fixedPoints_of_eq f (h_nab.lt_of_le h_ab) (le_of_lt h_a) h_fab
   | inr h_ba =>
-    exact lfpApprox_mem_fixedPoints_of_eq f b a (h_nab.symm.lt_of_le h_ba)
-      (h_fab.symm) (ord <| succ #α) (le_of_lt h_b)
+    exact lfpApprox_mem_fixedPoints_of_eq f (h_nab.symm.lt_of_le h_ba) (le_of_lt h_b) (h_fab.symm)
 
 /-- Every value of the ordinal approximants are less or equal than every fixed point of f -/
-theorem lfpApprox_le_fixedPoint : ∀ a : fixedPoints f, ∀ i : Ordinal, lfpApprox f i ≤ a := by
-  intro ⟨a, h_a⟩ i
+theorem lfpApprox_le_fixedPoint : ∀ a ∈ fixedPoints f, ∀ i : Ordinal, lfpApprox f i ≤ a := by
+  intro a h_a i
   induction i using Ordinal.induction with
   | h i IH =>
     unfold lfpApprox
@@ -198,7 +182,7 @@ theorem lfpApprox_cardinal_is_lfp : lfpApprox f (ord <| succ #α) = lfp f := by
   apply le_antisymm
   · have h_lfp : ∃ x : fixedPoints f, lfp f = x := by use ⊥; exact rfl
     let ⟨x, h_x⟩ := h_lfp; rw [h_x]
-    exact lfpApprox_le_fixedPoint f x (ord <| succ #α)
+    exact lfpApprox_le_fixedPoint f x x.2 (ord <| succ #α)
   · have h_fix : ∃ x : fixedPoints f, lfpApprox f (ord <| succ #α) = x := by
       simpa only [Subtype.exists, mem_fixedPoints, exists_prop, exists_eq_right'] using
         lfpApprox_has_fixedPoint_cardinal f
@@ -221,32 +205,32 @@ decreasing_by exact h
 theorem gfpApprox_antitone : Antitone (gfpApprox f) :=
   lfpApprox_monotone (OrderHom.dual f)
 
-theorem gfpApprox_addition (a : Ordinal.{u}) : f (gfpApprox f a) = gfpApprox f (a+1) :=
-  lfpApprox_addition (OrderHom.dual f) a
+theorem gfpApprox_add_one (a : Ordinal.{u}) : gfpApprox f (a+1) = f (gfpApprox f a) :=
+  lfpApprox_add_one (OrderHom.dual f) a
 
 /-- The ordinal approximants of the least fixed points are stabilizing
   when reaching a fixed point of f -/
-theorem gfpApprox_stabilizing_at_fixedPoint (a : Ordinal.{u}) (h : gfpApprox f a ∈ fixedPoints f) :
-    ∀ b > a, gfpApprox f b = gfpApprox f a :=
-  lfpApprox_stabilizing_at_fixedPoint (OrderHom.dual f) a h
+theorem gfpApprox_eq_of_mem_fixedPoint {a b : Ordinal.{u}} (h_ab : a < b)
+    (h: gfpApprox f a ∈ fixedPoints f) : gfpApprox f b = gfpApprox f a :=
+  lfpApprox_eq_of_mem_fixedPoint (OrderHom.dual f) h_ab h
 
-/-- Every value after a fixed point of f is also a fixed point of f -/
-theorem gfpApprox_ordinals_after_fixed_are_fixed (a : Ordinal.{u})
-    (h: gfpApprox f a ∈ fixedPoints f) : ∀ b > a, gfpApprox f b ∈ fixedPoints f :=
-  lfpApprox_ordinals_after_fixed_are_fixed (OrderHom.dual f) a h
+-- Every value after a fixed point of f is also a fixed point of f -/
+-- theorem gfpApprox_ordinals_after_fixed_are_fixed (a : Ordinal.{u})
+--     (h: gfpApprox f a ∈ fixedPoints f) : ∀ b > a, gfpApprox f b ∈ fixedPoints f :=
+--   lfpApprox_ordinals_after_fixed_are_fixed (OrderHom.dual f) a h
 
 /-- There are distinct ordinals smaller than the successor of the domains cardinals with
   equal value -/
-theorem disctinct_ordinal_eq_gfpApprox : ∃ i < ord <| succ #α, ∃ j < ord <| succ #α,
-    i ≠ j ∧ gfpApprox f i = gfpApprox f j :=
-  disctinct_ordinal_eq_lfpApprox (OrderHom.dual f)
+theorem distinct_ordinal_eq_gfpApprox : ∃ a < ord <| succ #α, ∃ b < ord <| succ #α,
+    a ≠ b ∧ gfpApprox f a = gfpApprox f b :=
+  distinct_ordinal_eq_lfpApprox (OrderHom.dual f)
 
 /-- A fixed point of f is reached after the successor of the domains cardinality -/
 lemma gfpApprox_has_fixedPoint_cardinal : gfpApprox f (ord <| succ #α) ∈ fixedPoints f :=
   lfpApprox_has_fixedPoint_cardinal (OrderHom.dual f)
 
 /-- Every value of the ordinal approximants are greater or equal than every fixed point of f -/
-lemma gfpApprox_ge_fixedPoint : ∀ a : fixedPoints f, ∀ i : Ordinal, gfpApprox f i ≥ a :=
+lemma gfpApprox_ge_fixedPoint : ∀ a ∈ fixedPoints f, ∀ i : Ordinal, gfpApprox f i ≥ a :=
   lfpApprox_le_fixedPoint (OrderHom.dual f)
 
 /-- The greatest fixed point of f is reached after the successor of the domains cardinality -/

From fab0ade9ebad87b767d2b71b6a0419b3499d79c4 Mon Sep 17 00:00:00 2001
From: Ira Fesefeldt <public@feuervogel.me>
Date: Mon, 18 Mar 2024 14:38:29 +0100
Subject: [PATCH 19/31] linter

---
 Mathlib/Order/Monotone/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Order/Monotone/Basic.lean b/Mathlib/Order/Monotone/Basic.lean
index 4d3fa546e69eb..a8c34223569b5 100644
--- a/Mathlib/Order/Monotone/Basic.lean
+++ b/Mathlib/Order/Monotone/Basic.lean
@@ -928,7 +928,7 @@ theorem Monotone.eq_of_le_of_le {a₁ a₂ : α} (h_mon : Monotone f) (h_fa : f
 
 /-- If an antitone function is equal at two points, it is equal between all of them -/
 theorem Antitone.eq_of_le_of_le {a₁ a₂ : α} (h_anti : Antitone f) (h_fa : f a₁ = f a₂) {i : α}
-   (h₁ : a₁ ≤ i) (h₂ : i ≤ a₂) : f i = f a₁ := by
+    (h₁ : a₁ ≤ i) (h₂ : i ≤ a₂) : f i = f a₁ := by
   apply le_antisymm
   · exact h_anti h₁
   · rw [h_fa]; exact h_anti h₂

From 378591c2d9e7c1b7ff3013d0bb8374e74ae68c91 Mon Sep 17 00:00:00 2001
From: Ira Fesefeldt <public@feuervogel.me>
Date: Mon, 18 Mar 2024 14:53:41 +0100
Subject: [PATCH 20/31] inlined lemma made nicer

---
 Mathlib/Order/OrdinalApproximantsFixedPoints.lean | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

diff --git a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean b/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
index 38e2ad1ab7919..d2c437cc90e91 100644
--- a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
+++ b/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
@@ -141,18 +141,17 @@ theorem distinct_ordinal_eq_lfpApprox : ∃ a < ord <| succ #α, ∃ b < ord <|
 lemma lfpApprox_mem_fixedPoints_of_eq {a b c : Ordinal.{u}} (h_ab : a < b) (h_ac : a ≤ c)
     (h_fab : lfpApprox f a = lfpApprox f b) :
     lfpApprox f c ∈ fixedPoints f := by
-  have lfpApprox_has_one_fixedPoint {d e : Ordinal.{u}} (h : d < e)
-      (h_fab : lfpApprox f d = lfpApprox f e) :
-      lfpApprox f d ∈ fixedPoints f := by
+  have lfpApprox_has_one_fixedPoint :
+      lfpApprox f a ∈ fixedPoints f := by
     rw [mem_fixedPoints_iff, ← lfpApprox_add_one]
     exact Monotone.eq_of_le_of_le (lfpApprox_monotone f)
-      h_fab (SuccOrder.le_succ d) (SuccOrder.succ_le_of_lt h)
+      h_fab (SuccOrder.le_succ a) (SuccOrder.succ_le_of_lt h_ab)
   obtain rfl | h_eq_ne := eq_or_ne c a
-  · exact lfpApprox_has_one_fixedPoint h_ab h_fab
+  · exact lfpApprox_has_one_fixedPoint
   · rw [lfpApprox_eq_of_mem_fixedPoint f]
-    · exact lfpApprox_has_one_fixedPoint h_ab h_fab
+    · exact lfpApprox_has_one_fixedPoint
     · exact Ne.lt_of_le' h_eq_ne h_ac
-    · exact lfpApprox_has_one_fixedPoint h_ab h_fab
+    · exact lfpApprox_has_one_fixedPoint
 
 /-- A fixed point of f is reached after the successor of the domains cardinality -/
 theorem lfpApprox_has_fixedPoint_cardinal : lfpApprox f (ord <| succ #α) ∈ fixedPoints f := by

From 27b3b60a1648a7f53ac4f2936a7c96d47f06b6f4 Mon Sep 17 00:00:00 2001
From: Ira Fesefeldt <public@feuervogel.me>
Date: Mon, 18 Mar 2024 16:31:46 +0100
Subject: [PATCH 21/31] renamed file and changed documentation

---
 Mathlib.lean                                          |  2 +-
 ...sFixedPoints.lean => ApproximantsFixedPoints.lean} | 11 ++---------
 2 files changed, 3 insertions(+), 10 deletions(-)
 rename Mathlib/Order/{OrdinalApproximantsFixedPoints.lean => ApproximantsFixedPoints.lean} (95%)

diff --git a/Mathlib.lean b/Mathlib.lean
index 24c12ae35ded7..912157d73ce78 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3100,7 +3100,7 @@ import Mathlib.Order.Notation
 import Mathlib.Order.OmegaCompletePartialOrder
 import Mathlib.Order.OrdContinuous
 import Mathlib.Order.OrderIsoNat
-import Mathlib.Order.OrdinalApproximantsFixedPoints
+import Mathlib.Order.ApproximantsFixedPoints
 import Mathlib.Order.PFilter
 import Mathlib.Order.PartialSups
 import Mathlib.Order.Partition.Equipartition
diff --git a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean b/Mathlib/Order/ApproximantsFixedPoints.lean
similarity index 95%
rename from Mathlib/Order/OrdinalApproximantsFixedPoints.lean
rename to Mathlib/Order/ApproximantsFixedPoints.lean
index d2c437cc90e91..627911b98e775 100644
--- a/Mathlib/Order/OrdinalApproximantsFixedPoints.lean
+++ b/Mathlib/Order/ApproximantsFixedPoints.lean
@@ -188,8 +188,7 @@ theorem lfpApprox_cardinal_is_lfp : lfpApprox f (ord <| succ #α) = lfp f := by
     let ⟨x, h_x⟩ := h_fix; rw [h_x]
     exact lfp_le_fixed f x.prop
 
-/-- Some ordinal approximation of the least fixed point is the least fixed point.
-  Also known as ordinal approximation of the least fixed point.-/
+/-- Some ordinal approximation of the least fixed point is the least fixed point. -/
 theorem lfpApprox_is_lfp : ∃ a : Ordinal, lfpApprox f a = lfp f := by
   use (ord <| succ #α)
   exact lfpApprox_cardinal_is_lfp f
@@ -213,11 +212,6 @@ theorem gfpApprox_eq_of_mem_fixedPoint {a b : Ordinal.{u}} (h_ab : a < b)
     (h: gfpApprox f a ∈ fixedPoints f) : gfpApprox f b = gfpApprox f a :=
   lfpApprox_eq_of_mem_fixedPoint (OrderHom.dual f) h_ab h
 
--- Every value after a fixed point of f is also a fixed point of f -/
--- theorem gfpApprox_ordinals_after_fixed_are_fixed (a : Ordinal.{u})
---     (h: gfpApprox f a ∈ fixedPoints f) : ∀ b > a, gfpApprox f b ∈ fixedPoints f :=
---   lfpApprox_ordinals_after_fixed_are_fixed (OrderHom.dual f) a h
-
 /-- There are distinct ordinals smaller than the successor of the domains cardinals with
   equal value -/
 theorem distinct_ordinal_eq_gfpApprox : ∃ a < ord <| succ #α, ∃ b < ord <| succ #α,
@@ -236,8 +230,7 @@ lemma gfpApprox_ge_fixedPoint : ∀ a ∈ fixedPoints f, ∀ i : Ordinal, gfpApp
 theorem gfpApprox_cardinal_is_gfp : gfpApprox f (ord <| succ #α) = gfp f :=
   lfpApprox_cardinal_is_lfp (OrderHom.dual f)
 
-/-- Some ordinal approximation of the greatest fixed point is the greatest fixed point.
-  Also known as ordinal approximation of the greatest fixed point.-/
+/-- Some ordinal approximation of the greatest fixed point is the greatest fixed point. -/
 theorem gfpApprox_is_gfp : ∃ a : Ordinal, gfpApprox f a = gfp f :=
   lfpApprox_is_lfp (OrderHom.dual f)
 

From 204e6adb8804a78b8a67e6696865126c94cae4eb Mon Sep 17 00:00:00 2001
From: Ira Fesefeldt <public@feuervogel.me>
Date: Mon, 18 Mar 2024 16:39:22 +0100
Subject: [PATCH 22/31] changed file to correct order in Mathlib.lean

---
 Mathlib.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index 912157d73ce78..836924e85d17f 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2981,6 +2981,7 @@ import Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
 import Mathlib.NumberTheory.Zsqrtd.ToReal
 import Mathlib.Order.Antichain
 import Mathlib.Order.Antisymmetrization
+import Mathlib.Order.ApproximantsFixedPoints
 import Mathlib.Order.Atoms
 import Mathlib.Order.Atoms.Finite
 import Mathlib.Order.Basic
@@ -3100,7 +3101,6 @@ import Mathlib.Order.Notation
 import Mathlib.Order.OmegaCompletePartialOrder
 import Mathlib.Order.OrdContinuous
 import Mathlib.Order.OrderIsoNat
-import Mathlib.Order.ApproximantsFixedPoints
 import Mathlib.Order.PFilter
 import Mathlib.Order.PartialSups
 import Mathlib.Order.Partition.Equipartition

From 06e58a41001356ae21083266e06031104ad10309 Mon Sep 17 00:00:00 2001
From: Ira Fesefeldt <public@feuervogel.me>
Date: Mon, 18 Mar 2024 17:26:53 +0100
Subject: [PATCH 23/31] make Set defs and lemmas shorter

---
 Mathlib/Order/ApproximantsFixedPoints.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Order/ApproximantsFixedPoints.lean b/Mathlib/Order/ApproximantsFixedPoints.lean
index 627911b98e775..ae131d5849a71 100644
--- a/Mathlib/Order/ApproximantsFixedPoints.lean
+++ b/Mathlib/Order/ApproximantsFixedPoints.lean
@@ -50,13 +50,13 @@ variable (g : Ordinal → α)
 
 open Cardinal Ordinal SuccOrder Function Set
 
-theorem not_injective_limitation_set : ¬ Set.InjOn g (Set.Iio (ord <| succ #α)) := by
+theorem not_injective_limitation_set : ¬ InjOn g (Iio (ord <| succ #α)) := by
   intro h_inj
-  have h := lift_mk_le_lift_mk_of_injective <| Set.injOn_iff_injective.1 h_inj
+  have h := lift_mk_le_lift_mk_of_injective <| injOn_iff_injective.1 h_inj
   have mk_initialSeg_subtype :
       #(Iio (ord <| succ #α)) = lift.{u+1, u} (succ #α) := by
     simpa only [coe_setOf, card_typein, card_ord] using mk_initialSeg (ord <| succ #α)
-  rw [mk_initialSeg_subtype, Cardinal.lift_lift, Cardinal.lift_le] at h
+  rw [mk_initialSeg_subtype, lift_lift, lift_le] at h
   exact not_le_of_lt (Order.lt_succ #α) h
 
 

From 7af7501812da7e0d8432a7ec6f1410550a1aebfb Mon Sep 17 00:00:00 2001
From: Ira Fesefeldt <public@feuervogel.me>
Date: Mon, 18 Mar 2024 17:37:03 +0100
Subject: [PATCH 24/31] made more variables implicit

---
 Mathlib/Order/ApproximantsFixedPoints.lean | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/Mathlib/Order/ApproximantsFixedPoints.lean b/Mathlib/Order/ApproximantsFixedPoints.lean
index ae131d5849a71..d0dc3b8d12740 100644
--- a/Mathlib/Order/ApproximantsFixedPoints.lean
+++ b/Mathlib/Order/ApproximantsFixedPoints.lean
@@ -163,8 +163,8 @@ theorem lfpApprox_has_fixedPoint_cardinal : lfpApprox f (ord <| succ #α) ∈ fi
     exact lfpApprox_mem_fixedPoints_of_eq f (h_nab.symm.lt_of_le h_ba) (le_of_lt h_b) (h_fab.symm)
 
 /-- Every value of the ordinal approximants are less or equal than every fixed point of f -/
-theorem lfpApprox_le_fixedPoint : ∀ a ∈ fixedPoints f, ∀ i : Ordinal, lfpApprox f i ≤ a := by
-  intro a h_a i
+theorem lfpApprox_le_fixedPoint {a : α} (h_a : a ∈ fixedPoints f) (i : Ordinal) :
+    lfpApprox f i ≤ a := by
   induction i using Ordinal.induction with
   | h i IH =>
     unfold lfpApprox
@@ -181,7 +181,7 @@ theorem lfpApprox_cardinal_is_lfp : lfpApprox f (ord <| succ #α) = lfp f := by
   apply le_antisymm
   · have h_lfp : ∃ x : fixedPoints f, lfp f = x := by use ⊥; exact rfl
     let ⟨x, h_x⟩ := h_lfp; rw [h_x]
-    exact lfpApprox_le_fixedPoint f x x.2 (ord <| succ #α)
+    exact lfpApprox_le_fixedPoint f x.2 (ord <| succ #α)
   · have h_fix : ∃ x : fixedPoints f, lfpApprox f (ord <| succ #α) = x := by
       simpa only [Subtype.exists, mem_fixedPoints, exists_prop, exists_eq_right'] using
         lfpApprox_has_fixedPoint_cardinal f
@@ -223,8 +223,8 @@ lemma gfpApprox_has_fixedPoint_cardinal : gfpApprox f (ord <| succ #α) ∈ fixe
   lfpApprox_has_fixedPoint_cardinal (OrderHom.dual f)
 
 /-- Every value of the ordinal approximants are greater or equal than every fixed point of f -/
-lemma gfpApprox_ge_fixedPoint : ∀ a ∈ fixedPoints f, ∀ i : Ordinal, gfpApprox f i ≥ a :=
-  lfpApprox_le_fixedPoint (OrderHom.dual f)
+lemma gfpApprox_ge_fixedPoint {a : α} (h_a : a ∈ fixedPoints f) (i : Ordinal) : gfpApprox f i ≥ a :=
+  lfpApprox_le_fixedPoint (OrderHom.dual f) h_a i
 
 /-- The greatest fixed point of f is reached after the successor of the domains cardinality -/
 theorem gfpApprox_cardinal_is_gfp : gfpApprox f (ord <| succ #α) = gfp f :=

From 2b6c98099f6a929cca7cc50a68f57bed1991e298 Mon Sep 17 00:00:00 2001
From: Ira Fesefeldt <public@feuervogel.me>
Date: Mon, 18 Mar 2024 17:47:29 +0100
Subject: [PATCH 25/31] simplified lfpApprox_eq_of_mem_fixedPoint

---
 Mathlib/Order/ApproximantsFixedPoints.lean | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

diff --git a/Mathlib/Order/ApproximantsFixedPoints.lean b/Mathlib/Order/ApproximantsFixedPoints.lean
index d0dc3b8d12740..43cc51e4baa49 100644
--- a/Mathlib/Order/ApproximantsFixedPoints.lean
+++ b/Mathlib/Order/ApproximantsFixedPoints.lean
@@ -102,7 +102,7 @@ theorem lfpApprox_add_one (a : Ordinal.{u}) : lfpApprox f (a+1) = f (lfpApprox f
 
 /-- The ordinal approximants of the least fixed points are stabilizing
   when reaching a fixed point of f -/
-theorem lfpApprox_eq_of_mem_fixedPoint {a b : Ordinal.{u}} (h_ab : a < b)
+theorem lfpApprox_eq_of_mem_fixedPoint {a b : Ordinal.{u}} (h_ab : a ≤ b)
     (h: lfpApprox f a ∈ fixedPoints f) : lfpApprox f b = lfpApprox f a := by
   rw [mem_fixedPoints_iff] at h
   induction b using Ordinal.induction with | h b IH =>
@@ -119,9 +119,9 @@ theorem lfpApprox_eq_of_mem_fixedPoint {a b : Ordinal.{u}} (h_ab : a < b)
       exact haa
     · simp only [not_lt] at haa
       cases le_iff_lt_or_eq.mp haa with
-      | inl haa => specialize IH a' ha'b haa; rw [IH, h]
+      | inl haa => specialize IH a' ha'b (le_of_lt haa); rw [IH, h]
       | inr haa => rw [← haa, h]
-  · exact lfpApprox_monotone f (le_of_lt h_ab)
+  · exact lfpApprox_monotone f h_ab
 
 /-- There are distinct ordinals smaller than the successor of the domains cardinals
   with equal value -/
@@ -146,12 +146,10 @@ lemma lfpApprox_mem_fixedPoints_of_eq {a b c : Ordinal.{u}} (h_ab : a < b) (h_ac
     rw [mem_fixedPoints_iff, ← lfpApprox_add_one]
     exact Monotone.eq_of_le_of_le (lfpApprox_monotone f)
       h_fab (SuccOrder.le_succ a) (SuccOrder.succ_le_of_lt h_ab)
-  obtain rfl | h_eq_ne := eq_or_ne c a
+  rw [lfpApprox_eq_of_mem_fixedPoint f]
+  · exact lfpApprox_has_one_fixedPoint
+  · exact h_ac
   · exact lfpApprox_has_one_fixedPoint
-  · rw [lfpApprox_eq_of_mem_fixedPoint f]
-    · exact lfpApprox_has_one_fixedPoint
-    · exact Ne.lt_of_le' h_eq_ne h_ac
-    · exact lfpApprox_has_one_fixedPoint
 
 /-- A fixed point of f is reached after the successor of the domains cardinality -/
 theorem lfpApprox_has_fixedPoint_cardinal : lfpApprox f (ord <| succ #α) ∈ fixedPoints f := by

From 5f8965003a2dd4a0a2870538ec2394c500a4f6b3 Mon Sep 17 00:00:00 2001
From: Ira Fesefeldt <public@feuervogel.me>
Date: Mon, 18 Mar 2024 17:54:12 +0100
Subject: [PATCH 26/31] fixed build error

---
 Mathlib/Order/ApproximantsFixedPoints.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Order/ApproximantsFixedPoints.lean b/Mathlib/Order/ApproximantsFixedPoints.lean
index 43cc51e4baa49..6c1d4f3535262 100644
--- a/Mathlib/Order/ApproximantsFixedPoints.lean
+++ b/Mathlib/Order/ApproximantsFixedPoints.lean
@@ -206,7 +206,7 @@ theorem gfpApprox_add_one (a : Ordinal.{u}) : gfpApprox f (a+1) = f (gfpApprox f
 
 /-- The ordinal approximants of the least fixed points are stabilizing
   when reaching a fixed point of f -/
-theorem gfpApprox_eq_of_mem_fixedPoint {a b : Ordinal.{u}} (h_ab : a < b)
+theorem gfpApprox_eq_of_mem_fixedPoint {a b : Ordinal.{u}} (h_ab : a ≤ b)
     (h: gfpApprox f a ∈ fixedPoints f) : gfpApprox f b = gfpApprox f a :=
   lfpApprox_eq_of_mem_fixedPoint (OrderHom.dual f) h_ab h
 

From ef44b56a673c251a47af963b8baca9579171e8b8 Mon Sep 17 00:00:00 2001
From: Ira Fesefeldt <fesefeldt@cs.rwth-aachen.de>
Date: Tue, 9 Apr 2024 14:15:20 +0200
Subject: [PATCH 27/31] review comments

---
 Mathlib.lean                                  |   2 +-
 .../Ordinal/FixedPointApproximants.lean}      | 181 ++++++++++--------
 2 files changed, 104 insertions(+), 79 deletions(-)
 rename Mathlib/{Order/ApproximantsFixedPoints.lean => SetTheory/Ordinal/FixedPointApproximants.lean} (50%)

diff --git a/Mathlib.lean b/Mathlib.lean
index 836924e85d17f..320a83e915bc0 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -2981,7 +2981,6 @@ import Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity
 import Mathlib.NumberTheory.Zsqrtd.ToReal
 import Mathlib.Order.Antichain
 import Mathlib.Order.Antisymmetrization
-import Mathlib.Order.ApproximantsFixedPoints
 import Mathlib.Order.Atoms
 import Mathlib.Order.Atoms.Finite
 import Mathlib.Order.Basic
@@ -3443,6 +3442,7 @@ import Mathlib.SetTheory.Ordinal.Basic
 import Mathlib.SetTheory.Ordinal.CantorNormalForm
 import Mathlib.SetTheory.Ordinal.Exponential
 import Mathlib.SetTheory.Ordinal.FixedPoint
+import Mathlib.SetTheory.Ordinal.FixedPointApproximants
 import Mathlib.SetTheory.Ordinal.NaturalOps
 import Mathlib.SetTheory.Ordinal.Notation
 import Mathlib.SetTheory.Ordinal.Principal
diff --git a/Mathlib/Order/ApproximantsFixedPoints.lean b/Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean
similarity index 50%
rename from Mathlib/Order/ApproximantsFixedPoints.lean
rename to Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean
index 6c1d4f3535262..8b11f5cfac231 100644
--- a/Mathlib/Order/ApproximantsFixedPoints.lean
+++ b/Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean
@@ -3,10 +3,6 @@ Copyright (c) 2024 Ira Fesefeldt. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ira Fesefeldt
 -/
-import Mathlib.Order.FixedPoints
-import Mathlib.Logic.Function.Basic
-import Mathlib.SetTheory.Ordinal.Basic
-import Mathlib.SetTheory.Cardinal.Basic
 import Mathlib.SetTheory.Ordinal.Arithmetic
 
 
@@ -67,67 +63,81 @@ namespace OrdinalApprox
 
 universe u
 variable {α : Type u}
-variable [CompleteLattice α] (f : α →o α)
+variable [CompleteLattice α] (f : α →o α) (x : α)
 
 open Function fixedPoints Cardinal Order OrderHom
 
 set_option linter.unusedVariables false in
-/-- Ordinal approximants of the least fixed points -/
+/-- Ordinal approximants of the least fixed points greater then an initial value x -/
 def lfpApprox (a : Ordinal.{u}) : α :=
-  sSup { f (lfpApprox b) | (b : Ordinal) (h : b < a) }
+  sSup ({ f (lfpApprox b) | (b : Ordinal) (h : b < a) } ∪ {x})
 termination_by a
 decreasing_by exact h
 
-theorem lfpApprox_monotone : Monotone (lfpApprox f) := by
+theorem lfpApprox_monotone : Monotone (lfpApprox f x) := by
   unfold Monotone; intros a b h; unfold lfpApprox
   refine sSup_le_sSup ?h
-  simp only [exists_prop, Set.setOf_subset_setOf, forall_exists_index,
-    and_imp, forall_apply_eq_imp_iff₂]
+  apply sup_le_sup_right
+  simp only [exists_prop, Set.le_eq_subset, Set.setOf_subset_setOf, forall_exists_index, and_imp,
+    forall_apply_eq_imp_iff₂]
   intros a' h'
   use a'
   exact ⟨lt_of_lt_of_le h' h, rfl⟩
 
-theorem lfpApprox_add_one (a : Ordinal.{u}) : lfpApprox f (a+1) = f (lfpApprox f a) := by
+theorem init_le_lfpApprox {a : Ordinal}: x ≤ (lfpApprox f x a) := by
+  unfold lfpApprox
+  apply le_sSup
+  simp only [exists_prop, Set.union_singleton, Set.mem_insert_iff, Set.mem_setOf_eq, true_or]
+
+
+theorem lfpApprox_add_one (h : x ≤ f x) (a : Ordinal) :
+    lfpApprox f x (a+1) = f (lfpApprox f x a) := by
   apply le_antisymm
   · conv => left; unfold lfpApprox
     apply sSup_le
-    simp only [Ordinal.add_one_eq_succ, lt_succ_iff, exists_prop, Set.mem_setOf_eq,
-      forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
-    intros a' h
-    apply f.2; apply lfpApprox_monotone; exact h
+    simp only [Ordinal.add_one_eq_succ, lt_succ_iff, exists_prop, Set.union_singleton,
+      Set.mem_insert_iff, Set.mem_setOf_eq, forall_eq_or_imp, forall_exists_index, and_imp,
+      forall_apply_eq_imp_iff₂]
+    apply And.intro
+    · apply le_trans h
+      apply Monotone.imp f.monotone
+      exact init_le_lfpApprox f x
+    · intros a' h
+      apply f.2; apply lfpApprox_monotone; exact h
   · conv => right; unfold lfpApprox
     apply le_sSup
-    simp only [Ordinal.add_one_eq_succ, lt_succ_iff, exists_prop, Set.mem_setOf_eq]
+    simp only [Ordinal.add_one_eq_succ, lt_succ_iff, exists_prop]
+    rw [Set.mem_union]
+    apply Or.inl
+    simp only [Set.mem_setOf_eq]
     use a
 
 /-- The ordinal approximants of the least fixed points are stabilizing
   when reaching a fixed point of f -/
-theorem lfpApprox_eq_of_mem_fixedPoint {a b : Ordinal.{u}} (h_ab : a ≤ b)
-    (h: lfpApprox f a ∈ fixedPoints f) : lfpApprox f b = lfpApprox f a := by
+theorem lfpApprox_eq_of_mem_fixedPoints {a b : Ordinal} (h_init : x ≤ f x) (h_ab : a ≤ b)
+    (h: lfpApprox f x a ∈ fixedPoints f) : lfpApprox f x b = lfpApprox f x a := by
   rw [mem_fixedPoints_iff] at h
   induction b using Ordinal.induction with | h b IH =>
   apply le_antisymm
   · conv => left; unfold lfpApprox
     apply sSup_le
-    simp only [exists_prop, Set.mem_setOf_eq, forall_exists_index, and_imp,
-      forall_apply_eq_imp_iff₂]
+    simp only [exists_prop, Set.union_singleton, Set.mem_insert_iff, Set.mem_setOf_eq,
+      forall_eq_or_imp, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
+    apply And.intro (init_le_lfpApprox f x)
     intro a' ha'b
     by_cases haa : a' < a
-    · rw [← lfpApprox_add_one]
+    · rw [← lfpApprox_add_one f x h_init]
       apply lfpApprox_monotone
       simp only [Ordinal.add_one_eq_succ, succ_le_iff]
       exact haa
-    · simp only [not_lt] at haa
-      cases le_iff_lt_or_eq.mp haa with
-      | inl haa => specialize IH a' ha'b (le_of_lt haa); rw [IH, h]
-      | inr haa => rw [← haa, h]
-  · exact lfpApprox_monotone f h_ab
+    · rw [IH a' ha'b (le_of_not_lt haa), h]
+  · exact lfpApprox_monotone f x h_ab
 
 /-- There are distinct ordinals smaller than the successor of the domains cardinals
   with equal value -/
-theorem distinct_ordinal_eq_lfpApprox : ∃ a < ord <| succ #α, ∃ b < ord <| succ #α,
-    a ≠ b ∧ lfpApprox f a = lfpApprox f b := by
-  have h_ninj := not_injective_limitation_set <| lfpApprox f
+theorem exists_lfpApprox_eq_lfpApprox : ∃ a < ord <| succ #α, ∃ b < ord <| succ #α,
+    a ≠ b ∧ lfpApprox f x a = lfpApprox f x b := by
+  have h_ninj := not_injective_limitation_set <| lfpApprox f x
   rw [Set.injOn_iff_injective, Function.not_injective_iff] at h_ninj
   let ⟨a, b, h_fab, h_nab⟩ := h_ninj
   use a.val; apply And.intro a.prop
@@ -138,98 +148,113 @@ theorem distinct_ordinal_eq_lfpApprox : ∃ a < ord <| succ #α, ∃ b < ord <|
 
 /-- If there are distinct ordinals with equal value then
   every value succeding the smaller ordinal are fixed points -/
-lemma lfpApprox_mem_fixedPoints_of_eq {a b c : Ordinal.{u}} (h_ab : a < b) (h_ac : a ≤ c)
-    (h_fab : lfpApprox f a = lfpApprox f b) :
-    lfpApprox f c ∈ fixedPoints f := by
-  have lfpApprox_has_one_fixedPoint :
-      lfpApprox f a ∈ fixedPoints f := by
-    rw [mem_fixedPoints_iff, ← lfpApprox_add_one]
-    exact Monotone.eq_of_le_of_le (lfpApprox_monotone f)
+lemma lfpApprox_mem_fixedPoints_of_eq {a b c : Ordinal}
+    (h_init : x ≤ f x) (h_ab : a < b) (h_ac : a ≤ c) (h_fab : lfpApprox f x a = lfpApprox f x b) :
+    lfpApprox f x c ∈ fixedPoints f := by
+  have lfpApprox_mem_fixedPoint :
+      lfpApprox f x a ∈ fixedPoints f := by
+    rw [mem_fixedPoints_iff, ← lfpApprox_add_one f x h_init]
+    exact Monotone.eq_of_le_of_le (lfpApprox_monotone f x)
       h_fab (SuccOrder.le_succ a) (SuccOrder.succ_le_of_lt h_ab)
-  rw [lfpApprox_eq_of_mem_fixedPoint f]
-  · exact lfpApprox_has_one_fixedPoint
+  rw [lfpApprox_eq_of_mem_fixedPoints f x h_init]
+  · exact lfpApprox_mem_fixedPoint
   · exact h_ac
-  · exact lfpApprox_has_one_fixedPoint
+  · exact lfpApprox_mem_fixedPoint
 
 /-- A fixed point of f is reached after the successor of the domains cardinality -/
-theorem lfpApprox_has_fixedPoint_cardinal : lfpApprox f (ord <| succ #α) ∈ fixedPoints f := by
-  let ⟨a, h_a, b, h_b, h_nab, h_fab⟩ := distinct_ordinal_eq_lfpApprox f
+theorem lfpApprox_ord_mem_fixedPoint (h_init : x ≤ f x) :
+    lfpApprox f x (ord <| succ #α) ∈ fixedPoints f := by
+  let ⟨a, h_a, b, h_b, h_nab, h_fab⟩ := exists_lfpApprox_eq_lfpApprox f x
   cases le_total a b with
   | inl h_ab =>
-    exact lfpApprox_mem_fixedPoints_of_eq f (h_nab.lt_of_le h_ab) (le_of_lt h_a) h_fab
+    exact lfpApprox_mem_fixedPoints_of_eq f x h_init
+      (h_nab.lt_of_le h_ab) (le_of_lt h_a) h_fab
   | inr h_ba =>
-    exact lfpApprox_mem_fixedPoints_of_eq f (h_nab.symm.lt_of_le h_ba) (le_of_lt h_b) (h_fab.symm)
+    exact lfpApprox_mem_fixedPoints_of_eq f x h_init
+      (h_nab.symm.lt_of_le h_ba) (le_of_lt h_b) (h_fab.symm)
 
 /-- Every value of the ordinal approximants are less or equal than every fixed point of f -/
-theorem lfpApprox_le_fixedPoint {a : α} (h_a : a ∈ fixedPoints f) (i : Ordinal) :
-    lfpApprox f i ≤ a := by
+theorem lfpApprox_le_of_mem_fixedPoints {a : α}
+    (h_a : a ∈ fixedPoints f) (h_le_init : x ≤ a) (i : Ordinal) : lfpApprox f x i ≤ a := by
   induction i using Ordinal.induction with
   | h i IH =>
     unfold lfpApprox
     apply sSup_le
-    simp only [exists_prop, Set.mem_setOf_eq, forall_exists_index, and_imp,
-      forall_apply_eq_imp_iff₂]
-    intro j h_j
-    rw [← h_a]
-    apply f.monotone'
-    exact IH j h_j
+    simp only [exists_prop]
+    intro y h_y
+    simp only [Set.mem_union, Set.mem_setOf_eq, Set.mem_singleton_iff] at h_y
+    cases h_y with
+    | inl h_y =>
+      let ⟨j, h_j_lt, h_j⟩ := h_y
+      rw [← h_j, ← h_a]
+      apply f.monotone'
+      exact IH j h_j_lt
+    | inr h_y =>
+      rw [h_y]
+      exact h_le_init
 
 /-- The least fixed point of f is reached after the successor of the domains cardinality -/
-theorem lfpApprox_cardinal_is_lfp : lfpApprox f (ord <| succ #α) = lfp f := by
+theorem lfpApprox_ord_eq_lfp : lfpApprox f ⊥ (ord <| succ #α) = lfp f := by
   apply le_antisymm
-  · have h_lfp : ∃ x : fixedPoints f, lfp f = x := by use ⊥; exact rfl
-    let ⟨x, h_x⟩ := h_lfp; rw [h_x]
-    exact lfpApprox_le_fixedPoint f x.2 (ord <| succ #α)
-  · have h_fix : ∃ x : fixedPoints f, lfpApprox f (ord <| succ #α) = x := by
+  · have h_lfp : ∃ y : fixedPoints f, lfp f = y := by use ⊥; exact rfl
+    let ⟨y, h_y⟩ := h_lfp; rw [h_y]
+    exact lfpApprox_le_of_mem_fixedPoints f ⊥ y.2 bot_le (ord <| succ #α)
+  · have h_fix : ∃ y : fixedPoints f, lfpApprox f ⊥ (ord <| succ #α) = y := by
       simpa only [Subtype.exists, mem_fixedPoints, exists_prop, exists_eq_right'] using
-        lfpApprox_has_fixedPoint_cardinal f
+        lfpApprox_ord_mem_fixedPoint f ⊥ bot_le
     let ⟨x, h_x⟩ := h_fix; rw [h_x]
     exact lfp_le_fixed f x.prop
 
 /-- Some ordinal approximation of the least fixed point is the least fixed point. -/
-theorem lfpApprox_is_lfp : ∃ a : Ordinal, lfpApprox f a = lfp f := by
+theorem lfp_mem_range_lfpApprox : lfp f ∈ Set.range (lfpApprox f ⊥) := by
   use (ord <| succ #α)
-  exact lfpApprox_cardinal_is_lfp f
+  exact lfpApprox_ord_eq_lfp f
 
 set_option linter.unusedVariables false in
 /-- Ordinal approximants of the greatest fixed points -/
 def gfpApprox (a : Ordinal.{u}) : α :=
-  sInf { f (gfpApprox b) | (b : Ordinal) (h : b < a) }
+  sInf ({ f (gfpApprox b) | (b : Ordinal) (h : b < a) } ∪ {x})
 termination_by a
 decreasing_by exact h
 
-theorem gfpApprox_antitone : Antitone (gfpApprox f) :=
-  lfpApprox_monotone (OrderHom.dual f)
+theorem gfpApprox_antitone : Antitone (gfpApprox f x) :=
+  lfpApprox_monotone (OrderHom.dual f) x
+
+theorem gfpApprox_le_init {a : Ordinal}: (gfpApprox f x a) ≤ x :=
+  init_le_lfpApprox (OrderHom.dual f) x
 
-theorem gfpApprox_add_one (a : Ordinal.{u}) : gfpApprox f (a+1) = f (gfpApprox f a) :=
-  lfpApprox_add_one (OrderHom.dual f) a
+theorem gfpApprox_add_one (h : f x ≤ x) (a : Ordinal) :
+    gfpApprox f x (a+1) = f (gfpApprox f x a) :=
+  lfpApprox_add_one (OrderHom.dual f) x h a
 
 /-- The ordinal approximants of the least fixed points are stabilizing
   when reaching a fixed point of f -/
-theorem gfpApprox_eq_of_mem_fixedPoint {a b : Ordinal.{u}} (h_ab : a ≤ b)
-    (h: gfpApprox f a ∈ fixedPoints f) : gfpApprox f b = gfpApprox f a :=
-  lfpApprox_eq_of_mem_fixedPoint (OrderHom.dual f) h_ab h
+theorem gfpApprox_eq_of_mem_fixedPoints {a b : Ordinal} (h_init : f x ≤ x) (h_ab : a ≤ b)
+    (h: gfpApprox f x a ∈ fixedPoints f) : gfpApprox f x b = gfpApprox f x a :=
+  lfpApprox_eq_of_mem_fixedPoints (OrderHom.dual f) x h_init h_ab h
 
 /-- There are distinct ordinals smaller than the successor of the domains cardinals with
   equal value -/
-theorem distinct_ordinal_eq_gfpApprox : ∃ a < ord <| succ #α, ∃ b < ord <| succ #α,
-    a ≠ b ∧ gfpApprox f a = gfpApprox f b :=
-  distinct_ordinal_eq_lfpApprox (OrderHom.dual f)
+theorem exists_grpApprox_eq_gfpApprox : ∃ a < ord <| succ #α, ∃ b < ord <| succ #α,
+    a ≠ b ∧ gfpApprox f x a = gfpApprox f x b :=
+  exists_lfpApprox_eq_lfpApprox (OrderHom.dual f) x
 
 /-- A fixed point of f is reached after the successor of the domains cardinality -/
-lemma gfpApprox_has_fixedPoint_cardinal : gfpApprox f (ord <| succ #α) ∈ fixedPoints f :=
-  lfpApprox_has_fixedPoint_cardinal (OrderHom.dual f)
+lemma gfpApprox_ord_mem_fixedPoint (h_init : f x ≤ x) :
+    gfpApprox f x (ord <| succ #α) ∈ fixedPoints f :=
+  lfpApprox_ord_mem_fixedPoint (OrderHom.dual f) x h_init
 
 /-- Every value of the ordinal approximants are greater or equal than every fixed point of f -/
-lemma gfpApprox_ge_fixedPoint {a : α} (h_a : a ∈ fixedPoints f) (i : Ordinal) : gfpApprox f i ≥ a :=
-  lfpApprox_le_fixedPoint (OrderHom.dual f) h_a i
+lemma le_gfpApprox_of_mem_fixedPoints {a : α}
+    (h_a : a ∈ fixedPoints f) (h_init_le : a ≤ x) (i : Ordinal) : a ≤ gfpApprox f x i:=
+  lfpApprox_le_of_mem_fixedPoints (OrderHom.dual f) x h_a h_init_le i
 
 /-- The greatest fixed point of f is reached after the successor of the domains cardinality -/
-theorem gfpApprox_cardinal_is_gfp : gfpApprox f (ord <| succ #α) = gfp f :=
-  lfpApprox_cardinal_is_lfp (OrderHom.dual f)
+theorem gfpApprox_ord_eq_gfp : gfpApprox f ⊤ (ord <| succ #α) = gfp f :=
+  lfpApprox_ord_eq_lfp (OrderHom.dual f)
 
 /-- Some ordinal approximation of the greatest fixed point is the greatest fixed point. -/
-theorem gfpApprox_is_gfp : ∃ a : Ordinal, gfpApprox f a = gfp f :=
-  lfpApprox_is_lfp (OrderHom.dual f)
+theorem gfp_mem_range_gfpApprox  : gfp f ∈ Set.range (gfpApprox f ⊤) :=
+  lfp_mem_range_lfpApprox (OrderHom.dual f)
 
 end OrdinalApprox

From 2c609b564e7a9e6c947791f60eca7affa6448b7e Mon Sep 17 00:00:00 2001
From: Ira Fesefeldt <fesefeldt@cs.rwth-aachen.de>
Date: Tue, 9 Apr 2024 15:02:01 +0200
Subject: [PATCH 28/31] better documentation

---
 .../Ordinal/FixedPointApproximants.lean       | 30 ++++++++++---------
 1 file changed, 16 insertions(+), 14 deletions(-)

diff --git a/Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean b/Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean
index 8b11f5cfac231..1f81f3eb24cf1 100644
--- a/Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean
+++ b/Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean
@@ -18,15 +18,15 @@ ordinals from mathlib. It still allows an approximation scheme indexed over the
 
 ## Main definitions
 
-* `OrdinalApprox.lfpApprox`: The ordinal approximation of
-  the least fixed point of a bundled monotone function.
-* `OrdinalApprox.gfpApprox`: The ordinal approximation of
-  the greatest fixed point of a bundled monotone function.
+* `OrdinalApprox.lfpApprox`: The ordinal approximation of the least fixed point
+  greater or equal then an initial value of a bundled monotone function.
+* `OrdinalApprox.gfpApprox`: The ordinal approximation of the greatest fixed point
+  less or equal then an initial value of a bundled monotone function.
 
 ## Main theorems
-* `OrdinalApprox.lfpApprox_is_lfp`: The approximation of
+* `OrdinalApprox.lfp_mem_range_lfpApprox`: The approximation of
   the least fixed point eventually reaches the least fixed point
-* `OrdinalApprox.gfpApprox_is_gfp`: The approximation of
+* `OrdinalApprox.gfp_mem_range_gfpApprox`: The approximation of
   the greatest fixed point eventually reaches the greatest fixed point
 
 ## References
@@ -68,7 +68,7 @@ variable [CompleteLattice α] (f : α →o α) (x : α)
 open Function fixedPoints Cardinal Order OrderHom
 
 set_option linter.unusedVariables false in
-/-- Ordinal approximants of the least fixed points greater then an initial value x -/
+/-- Ordinal approximants of the least fixed point greater then an initial value x -/
 def lfpApprox (a : Ordinal.{u}) : α :=
   sSup ({ f (lfpApprox b) | (b : Ordinal) (h : b < a) } ∪ {x})
 termination_by a
@@ -112,7 +112,7 @@ theorem lfpApprox_add_one (h : x ≤ f x) (a : Ordinal) :
     simp only [Set.mem_setOf_eq]
     use a
 
-/-- The ordinal approximants of the least fixed points are stabilizing
+/-- The ordinal approximants of the least fixed point are stabilizing
   when reaching a fixed point of f -/
 theorem lfpApprox_eq_of_mem_fixedPoints {a b : Ordinal} (h_init : x ≤ f x) (h_ab : a ≤ b)
     (h: lfpApprox f x a ∈ fixedPoints f) : lfpApprox f x b = lfpApprox f x a := by
@@ -173,7 +173,8 @@ theorem lfpApprox_ord_mem_fixedPoint (h_init : x ≤ f x) :
     exact lfpApprox_mem_fixedPoints_of_eq f x h_init
       (h_nab.symm.lt_of_le h_ba) (le_of_lt h_b) (h_fab.symm)
 
-/-- Every value of the ordinal approximants are less or equal than every fixed point of f -/
+/-- Every value of the ordinal approximants are less or equal than every fixed point of f greater
+  then the initial value -/
 theorem lfpApprox_le_of_mem_fixedPoints {a : α}
     (h_a : a ∈ fixedPoints f) (h_le_init : x ≤ a) (i : Ordinal) : lfpApprox f x i ≤ a := by
   induction i using Ordinal.induction with
@@ -211,7 +212,7 @@ theorem lfp_mem_range_lfpApprox : lfp f ∈ Set.range (lfpApprox f ⊥) := by
   exact lfpApprox_ord_eq_lfp f
 
 set_option linter.unusedVariables false in
-/-- Ordinal approximants of the greatest fixed points -/
+/-- Ordinal approximants of the greatest fixed point -/
 def gfpApprox (a : Ordinal.{u}) : α :=
   sInf ({ f (gfpApprox b) | (b : Ordinal) (h : b < a) } ∪ {x})
 termination_by a
@@ -227,7 +228,7 @@ theorem gfpApprox_add_one (h : f x ≤ x) (a : Ordinal) :
     gfpApprox f x (a+1) = f (gfpApprox f x a) :=
   lfpApprox_add_one (OrderHom.dual f) x h a
 
-/-- The ordinal approximants of the least fixed points are stabilizing
+/-- The ordinal approximants of the least fixed point are stabilizing
   when reaching a fixed point of f -/
 theorem gfpApprox_eq_of_mem_fixedPoints {a b : Ordinal} (h_init : f x ≤ x) (h_ab : a ≤ b)
     (h: gfpApprox f x a ∈ fixedPoints f) : gfpApprox f x b = gfpApprox f x a :=
@@ -244,10 +245,11 @@ lemma gfpApprox_ord_mem_fixedPoint (h_init : f x ≤ x) :
     gfpApprox f x (ord <| succ #α) ∈ fixedPoints f :=
   lfpApprox_ord_mem_fixedPoint (OrderHom.dual f) x h_init
 
-/-- Every value of the ordinal approximants are greater or equal than every fixed point of f -/
+/-- Every value of the ordinal approximants are greater or equal than every fixed point of f
+  that is smaller then the initial value -/
 lemma le_gfpApprox_of_mem_fixedPoints {a : α}
-    (h_a : a ∈ fixedPoints f) (h_init_le : a ≤ x) (i : Ordinal) : a ≤ gfpApprox f x i:=
-  lfpApprox_le_of_mem_fixedPoints (OrderHom.dual f) x h_a h_init_le i
+    (h_a : a ∈ fixedPoints f) (h_le_init : a ≤ x) (i : Ordinal) : a ≤ gfpApprox f x i:=
+  lfpApprox_le_of_mem_fixedPoints (OrderHom.dual f) x h_a h_le_init i
 
 /-- The greatest fixed point of f is reached after the successor of the domains cardinality -/
 theorem gfpApprox_ord_eq_gfp : gfpApprox f ⊤ (ord <| succ #α) = gfp f :=

From 42293bb3dc2741fd40c02fe603cbc4f0faa18f7a Mon Sep 17 00:00:00 2001
From: Ira Fesefeldt <fesefeldt@cs.rwth-aachen.de>
Date: Tue, 9 Apr 2024 15:07:33 +0200
Subject: [PATCH 29/31] typos and similiar

---
 Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean b/Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean
index 1f81f3eb24cf1..d1d27315da1e7 100644
--- a/Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean
+++ b/Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean
@@ -50,7 +50,7 @@ theorem not_injective_limitation_set : ¬ InjOn g (Iio (ord <| succ #α)) := by
   intro h_inj
   have h := lift_mk_le_lift_mk_of_injective <| injOn_iff_injective.1 h_inj
   have mk_initialSeg_subtype :
-      #(Iio (ord <| succ #α)) = lift.{u+1, u} (succ #α) := by
+      #(Iio (ord <| succ #α)) = lift (succ #α) := by
     simpa only [coe_setOf, card_typein, card_ord] using mk_initialSeg (ord <| succ #α)
   rw [mk_initialSeg_subtype, lift_lift, lift_le] at h
   exact not_le_of_lt (Order.lt_succ #α) h
@@ -236,7 +236,7 @@ theorem gfpApprox_eq_of_mem_fixedPoints {a b : Ordinal} (h_init : f x ≤ x) (h_
 
 /-- There are distinct ordinals smaller than the successor of the domains cardinals with
   equal value -/
-theorem exists_grpApprox_eq_gfpApprox : ∃ a < ord <| succ #α, ∃ b < ord <| succ #α,
+theorem exists_gfpApprox_eq_gfpApprox : ∃ a < ord <| succ #α, ∃ b < ord <| succ #α,
     a ≠ b ∧ gfpApprox f x a = gfpApprox f x b :=
   exists_lfpApprox_eq_lfpApprox (OrderHom.dual f) x
 

From 66dd10c41c3d3b7e9e59d7f56425dd35b6b429d0 Mon Sep 17 00:00:00 2001
From: Ira Fesefeldt <fesefeldt@cs.rwth-aachen.de>
Date: Wed, 10 Apr 2024 09:49:16 +0200
Subject: [PATCH 30/31] removed init from name

---
 Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

diff --git a/Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean b/Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean
index d1d27315da1e7..29995fd6e23c4 100644
--- a/Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean
+++ b/Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean
@@ -84,12 +84,11 @@ theorem lfpApprox_monotone : Monotone (lfpApprox f x) := by
   use a'
   exact ⟨lt_of_lt_of_le h' h, rfl⟩
 
-theorem init_le_lfpApprox {a : Ordinal}: x ≤ (lfpApprox f x a) := by
+theorem le_lfpApprox {a : Ordinal} : x ≤ lfpApprox f x a := by
   unfold lfpApprox
   apply le_sSup
   simp only [exists_prop, Set.union_singleton, Set.mem_insert_iff, Set.mem_setOf_eq, true_or]
 
-
 theorem lfpApprox_add_one (h : x ≤ f x) (a : Ordinal) :
     lfpApprox f x (a+1) = f (lfpApprox f x a) := by
   apply le_antisymm
@@ -101,7 +100,7 @@ theorem lfpApprox_add_one (h : x ≤ f x) (a : Ordinal) :
     apply And.intro
     · apply le_trans h
       apply Monotone.imp f.monotone
-      exact init_le_lfpApprox f x
+      exact le_lfpApprox f x
     · intros a' h
       apply f.2; apply lfpApprox_monotone; exact h
   · conv => right; unfold lfpApprox
@@ -123,7 +122,7 @@ theorem lfpApprox_eq_of_mem_fixedPoints {a b : Ordinal} (h_init : x ≤ f x) (h_
     apply sSup_le
     simp only [exists_prop, Set.union_singleton, Set.mem_insert_iff, Set.mem_setOf_eq,
       forall_eq_or_imp, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
-    apply And.intro (init_le_lfpApprox f x)
+    apply And.intro (le_lfpApprox f x)
     intro a' ha'b
     by_cases haa : a' < a
     · rw [← lfpApprox_add_one f x h_init]
@@ -221,8 +220,8 @@ decreasing_by exact h
 theorem gfpApprox_antitone : Antitone (gfpApprox f x) :=
   lfpApprox_monotone (OrderHom.dual f) x
 
-theorem gfpApprox_le_init {a : Ordinal}: (gfpApprox f x a) ≤ x :=
-  init_le_lfpApprox (OrderHom.dual f) x
+theorem gfpApprox_le {a : Ordinal}: (gfpApprox f x a) ≤ x :=
+  le_lfpApprox (OrderHom.dual f) x
 
 theorem gfpApprox_add_one (h : f x ≤ x) (a : Ordinal) :
     gfpApprox f x (a+1) = f (gfpApprox f x a) :=

From 1d00b4048c63284bae256336845b3e4709ad2b4c Mon Sep 17 00:00:00 2001
From: Ira Fesefeldt <fesefeldt@cs.rwth-aachen.de>
Date: Wed, 10 Apr 2024 09:50:54 +0200
Subject: [PATCH 31/31] typo

---
 Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean b/Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean
index 29995fd6e23c4..97a6f57f2ab46 100644
--- a/Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean
+++ b/Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean
@@ -220,7 +220,7 @@ decreasing_by exact h
 theorem gfpApprox_antitone : Antitone (gfpApprox f x) :=
   lfpApprox_monotone (OrderHom.dual f) x
 
-theorem gfpApprox_le {a : Ordinal}: (gfpApprox f x a) ≤ x :=
+theorem gfpApprox_le {a : Ordinal}: gfpApprox f x a ≤ x :=
   le_lfpApprox (OrderHom.dual f) x
 
 theorem gfpApprox_add_one (h : f x ≤ x) (a : Ordinal) :