chore(SetTheory/Ordinal/FixedPointApproximants): simpler definition for lfpApprox (leanprover-community#37383)

We simplify the definition of `Ordinal.lfpApprox` - the old definition wasn't even simp-normal. We then golf the entire API using it.

Author: vihdzp

Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean

@@ -64,101 +64,66 @@ namespace OrdinalApprox
 
 universe u
 variable {α : Type u}
-variable [CompleteLattice α] (f : α →o α) (x : α)
+variable [CompleteLattice α] (f : α →o α) {x : α} {a b c : Ordinal.{u}}
 
 open Function fixedPoints Cardinal Order OrderHom
 
+variable (x) in
 /-- The ordinal-indexed sequence approximating the least fixed point greater than
 an initial value `x`. It is defined in such a way that we have `lfpApprox 0 x = x` and
 `lfpApprox a x = ⨆ b < a, f (lfpApprox b x)`. -/
 def lfpApprox (a : Ordinal.{u}) : α :=
-  sSup ({ f (lfpApprox b) | (b : Ordinal) (_ : b < a) } ∪ {x})
+  x ⊔ ⨆ b < a, f (lfpApprox b)
 termination_by a
 
-theorem lfpApprox_monotone : Monotone (lfpApprox f x) := by
+theorem lfpApprox_mono_right : Monotone (lfpApprox f x) := by
   intro a b h
   rw [lfpApprox, lfpApprox]
-  gcongr sSup (?_ ∪ {x})
-  simp only [exists_prop, Set.setOf_subset_setOf, forall_exists_index, and_imp,
-    forall_apply_eq_imp_iff₂]
-  intro a' h'
-  use a'
-  exact ⟨lt_of_lt_of_le h' h, rfl⟩
+  apply sup_le_sup_left (iSup₂_mono' _)
+  grind
+
+@[deprecated (since := "2026-03-30")] alias lfpApprox_monotone := lfpApprox_mono_right
 
 theorem le_lfpApprox {a : Ordinal} : x ≤ lfpApprox f x a := by
   rw [lfpApprox]
-  apply le_sSup
-  simp only [exists_prop, Set.union_singleton, Set.mem_insert_iff, Set.mem_setOf_eq, true_or]
+  exact le_sup_left
 
-theorem lfpApprox_add_one (h : x ≤ f x) (a : Ordinal) :
+theorem lfpApprox_add_one (hx : x ≤ f x) (a : Ordinal) :
     lfpApprox f x (a + 1) = f (lfpApprox f x a) := by
-  apply le_antisymm
-  · conv => left; rw [lfpApprox]
-    apply sSup_le
-    simp only [lt_add_one_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 le_lfpApprox f x
-    · intro a' h
-      apply f.2; apply lfpApprox_monotone; exact h
-  · conv => right; rw [lfpApprox]
-    apply le_sSup
-    simp only [lt_add_one_iff, exists_prop]
-    rw [Set.mem_union]
-    apply Or.inl
-    simp only [Set.mem_setOf_eq]
-    use a
-
-theorem lfpApprox_mono_left : Monotone (lfpApprox : (α →o α) → _) := by
+  rw [lfpApprox]
+  apply (sup_le (hx.trans (f.mono (le_lfpApprox ..))) _).antisymm
+  · exact le_sup_of_le_right <| le_iSup₂ (f := fun b _ ↦ f (lfpApprox f x b)) a (lt_add_one a)
+  · simpa using fun i h ↦ f.monotone.comp (lfpApprox_mono_right f) h
+
+theorem lfpApprox_mono_left : Monotone (lfpApprox (α := α)) := by
   intro f g h x a
-  induction a using WellFoundedLT.induction with | ind i ih
+  induction a using WellFoundedLT.induction with | ind i IH
   rw [lfpApprox, lfpApprox]
-  apply sSup_le
-  simp only [exists_prop, Set.union_singleton, Set.mem_insert_iff, Set.mem_setOf_eq, sSup_insert,
-    forall_eq_or_imp, le_sup_left, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
-    true_and]
-  intro i' h_lt
-  grw [← le_sup_right]
-  refine le_sSup_of_le ⟨i', h_lt, rfl⟩ ?_
-  grw [h _, ih i' h_lt]
+  exact sup_le_sup_left (iSup₂_mono fun j hj ↦ (f.mono (IH j hj)).trans (h _)) _
 
 theorem lfpApprox_mono_mid : Monotone (lfpApprox f) := by
   intro x₁ x₂ h a
-  induction a using WellFoundedLT.induction with | ind i ih
+  induction a using WellFoundedLT.induction with | ind i IH
   rw [lfpApprox, lfpApprox]
-  apply sSup_le
-  simp only [exists_prop, Set.union_singleton, Set.mem_insert_iff, Set.mem_setOf_eq, sSup_insert,
-    forall_eq_or_imp, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
-  constructor
-  · exact le_sup_of_le_left h
-  · intro i' h_i'
-    apply le_sup_of_le_right
-    apply le_sSup_of_le
-    · use i'
-    · exact f.monotone (ih i' h_i')
+  exact sup_le_sup h <| iSup₂_mono fun j hj ↦ f.mono (IH j hj)
 
 /-- The approximations of the least fixed point stabilize at 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
-  rw [mem_fixedPoints_iff] at h
+theorem lfpApprox_eq_of_mem_fixedPoints (hx : x ≤ f x) (hab : a ≤ b)
+    (hf : lfpApprox f x a ∈ fixedPoints f) : lfpApprox f x b = lfpApprox f x a := by
+  rw [mem_fixedPoints_iff] at hf
   induction b using WellFoundedLT.induction with | ind b IH
-  apply le_antisymm
-  · conv => left; rw [lfpApprox]
-    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 (le_lfpApprox f x)
-    intro a' ha'b
-    by_cases! haa : a' < a
-    · rw [← lfpApprox_add_one f x h_init]
-      apply lfpApprox_monotone
-      simpa
-    · rw [IH a' ha'b haa, h]
-  · exact lfpApprox_monotone f x h_ab
-
+  apply (lfpApprox_mono_right f hab).antisymm'
+  rw [lfpApprox]
+  apply sup_le (le_lfpApprox ..)
+  rw [iSup₂_le_iff]
+  intro i hi
+  by_cases! hi' : i < a
+  · rw [← lfpApprox_add_one f hx]
+    apply lfpApprox_mono_right
+    rwa [add_one_le_iff]
+  · rw [IH _ hi hi', hf]
+
+variable (x) in
 /-- There are distinct indices smaller than the successor of the domain's cardinality
 yielding the same value -/
 theorem exists_lfpApprox_eq_lfpApprox : ∃ a < ord <| succ #α, ∃ b < ord <| succ #α,
@@ -174,60 +139,42 @@ theorem exists_lfpApprox_eq_lfpApprox : ∃ a < ord <| succ #α, ∃ b < ord <|
 
 /-- If the sequence of ordinal-indexed approximations takes a value twice,
 then it actually stabilised at that value. -/
-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_ge_of_le (lfpApprox_monotone f x)
-      h_fab (SuccOrder.le_succ a) (SuccOrder.succ_le_of_lt h_ab)
-  rw [lfpApprox_eq_of_mem_fixedPoints f x h_init]
-  · exact lfpApprox_mem_fixedPoint
-  · exact h_ac
-  · exact lfpApprox_mem_fixedPoint
+lemma lfpApprox_mem_fixedPoints_of_eq (hx : x ≤ f x) (hab : a < b) (hac : a ≤ c)
+    (hf : lfpApprox f x a = lfpApprox f x b) : lfpApprox f x c ∈ fixedPoints f := by
+  have H : lfpApprox f x a ∈ fixedPoints f := by
+    rw [mem_fixedPoints_iff, ← lfpApprox_add_one f hx]
+    exact (lfpApprox_mono_right f).eq_of_ge_of_le
+      hf (lt_add_one a).le (add_one_le_of_lt hab)
+  rwa [lfpApprox_eq_of_mem_fixedPoints f hx hac H]
 
 /-- The approximation at the index of the successor of the domain's cardinality is a fixed point -/
-theorem lfpApprox_ord_mem_fixedPoint (h_init : x ≤ f x) :
+theorem lfpApprox_ord_mem_fixedPoint (hx : 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
+  let ⟨a, ha, b, hb, hne, hf⟩ := exists_lfpApprox_eq_lfpApprox f x
   cases le_total a b with
-  | inl h_ab =>
-    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 x h_init
-      (h_nab.symm.lt_of_le h_ba) (le_of_lt h_b) (h_fab.symm)
+  | inl hab => exact lfpApprox_mem_fixedPoints_of_eq f hx (hne.lt_of_le hab) ha.le hf
+  | inr hba => exact lfpApprox_mem_fixedPoints_of_eq f hx (hne.symm.lt_of_le hba) hb.le hf.symm
 
 /-- Every value of the approximation is less or equal than every fixed point of `f`
 greater or equal than 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
+    (ha : a ∈ fixedPoints f) (hxa : x ≤ a) (i : Ordinal) : lfpApprox f x i ≤ a := by
   induction i using WellFoundedLT.induction with | ind i IH
   rw [lfpApprox]
-  apply sSup_le
-  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]
-    exact f.monotone' (IH j h_j_lt)
-  | inr h_y =>
-    rw [h_y]
-    exact h_le_init
+  apply sup_le hxa
+  rw [iSup₂_le_iff, ← ha.eq]
+  exact fun y hy ↦ f.mono (IH y hy)
 
 /-- The approximation sequence converges at the successor of the domain's cardinality
 to the least fixed point if starting from `⊥` -/
 theorem lfpApprox_ord_eq_lfp : lfpApprox f ⊥ (ord <| succ #α) = f.lfp := by
   apply le_antisymm
   · have h_lfp : ∃ y : fixedPoints f, f.lfp = 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 #α)
+    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_ord_mem_fixedPoint f ⊥ bot_le
+        lfpApprox_ord_mem_fixedPoint f bot_le
     let ⟨x, h_x⟩ := h_fix; rw [h_x]
     exact lfp_le_fixed f x.prop
 
@@ -236,26 +183,29 @@ theorem lfp_mem_range_lfpApprox : f.lfp ∈ Set.range (lfpApprox f ⊥) := by
   use ord <| succ #α
   exact lfpApprox_ord_eq_lfp f
 
+variable (x) in
 /-- The ordinal-indexed sequence approximating the greatest fixed point greater than
 an initial value `x`. It is defined in such a way that we have `gfpApprox 0 x = x` and
 `gfpApprox a x = ⨅ b < a, f (lfpApprox b x)`. -/
 def gfpApprox (a : Ordinal.{u}) : α :=
-  sInf ({ f (gfpApprox b) | (b : Ordinal) (_ : b < a) } ∪ {x})
+  x ⊓ ⨅ b < a, f (gfpApprox b)
 termination_by a
 
 -- By unsealing these recursive definitions we can relate them
 -- by definitional equality
 unseal gfpApprox lfpApprox
 
-theorem gfpApprox_antitone : Antitone (gfpApprox f x) :=
-  lfpApprox_monotone f.dual x
+theorem gfpApprox_anti_right : Antitone (gfpApprox f x) :=
+  lfpApprox_mono_right f.dual
+
+@[deprecated (since := "2026-03-30")] alias gfpApprox_antitone := gfpApprox_anti_right
 
 theorem gfpApprox_le {a : Ordinal} : gfpApprox f x a ≤ x :=
-  le_lfpApprox f.dual x
+  le_lfpApprox f.dual
 
-theorem gfpApprox_add_one (h : f x ≤ x) (a : Ordinal) :
+theorem gfpApprox_add_one (hx : f x ≤ x) (a : Ordinal) :
     gfpApprox f x (a + 1) = f (gfpApprox f x a) :=
-  lfpApprox_add_one f.dual x h a
+  lfpApprox_add_one f.dual hx a
 
 theorem gfpApprox_mono_left : Monotone (gfpApprox : (α →o α) → _) := by
   intro f g h
@@ -266,9 +216,9 @@ theorem gfpApprox_mono_mid : Monotone (gfpApprox f) :=
   fun _ _ h => lfpApprox_mono_mid f.dual h
 
 /-- The approximations of the greatest fixed point stabilize at a fixed point of `f` -/
-theorem gfpApprox_eq_of_mem_fixedPoints {a b : Ordinal} (h_init : f x ≤ x) (h_ab : a ≤ b)
+theorem gfpApprox_eq_of_mem_fixedPoints {a b : Ordinal} (hx : f x ≤ x) (hab : a ≤ b)
     (h : gfpApprox f x a ∈ fixedPoints f) : gfpApprox f x b = gfpApprox f x a :=
-  lfpApprox_eq_of_mem_fixedPoints f.dual x h_init h_ab h
+  lfpApprox_eq_of_mem_fixedPoints f.dual hx hab h
 
 /-- There are distinct indices smaller than the successor of the domain's cardinality
 yielding the same value -/
@@ -277,15 +227,15 @@ theorem exists_gfpApprox_eq_gfpApprox : ∃ a < ord <| succ #α, ∃ b < ord <|
   exists_lfpApprox_eq_lfpApprox f.dual x
 
 /-- The approximation at the index of the successor of the domain's cardinality is a fixed point -/
-lemma gfpApprox_ord_mem_fixedPoint (h_init : f x ≤ x) :
+lemma gfpApprox_ord_mem_fixedPoint (hx : f x ≤ x) :
     gfpApprox f x (ord <| succ #α) ∈ fixedPoints f :=
-  lfpApprox_ord_mem_fixedPoint f.dual x h_init
+  lfpApprox_ord_mem_fixedPoint f.dual hx
 
 /-- Every value of the approximation is greater or equal than every fixed point of `f`
 less or equal than the initial value -/
 lemma le_gfpApprox_of_mem_fixedPoints {a : α}
-    (h_a : a ∈ fixedPoints f) (h_le_init : a ≤ x) (i : Ordinal) : a ≤ gfpApprox f x i :=
-  lfpApprox_le_of_mem_fixedPoints f.dual x h_a h_le_init i
+    (ha : a ∈ fixedPoints f) (hax : a ≤ x) (i : Ordinal) : a ≤ gfpApprox f x i :=
+  lfpApprox_le_of_mem_fixedPoints f.dual ha hax i
 
 /-- The approximation sequence converges at the successor of the domain's cardinality
 to the greatest fixed point if starting from `⊥` -/