refactor(Order/OmegaCompletePartialOrder): make Chain a structure (#37258)

It has a different `LE` to `OrderHom`, hence should not be an `abbrev`.

Author: YaelDillies

Mathlib/LinearAlgebra/Span/Basic.lean

@@ -160,7 +160,7 @@ Scott continuous for the ω-complete partial order induced by the complete latti
 theorem coe_scott_continuous :
     OmegaCompletePartialOrder.ωScottContinuous ((↑) : Submodule R M → Set M) :=
   OmegaCompletePartialOrder.ωScottContinuous.of_monotone_map_ωSup
-    ⟨SetLike.coe_mono, coe_iSup_of_chain⟩
+    ⟨SetLike.coe_mono, fun _ ↦ coe_iSup_of_chain _⟩
 
 section IsScalarTower
 

Mathlib/Order/Hom/Basic.lean

@@ -287,7 +287,7 @@ instance : Inhabited (α →o α) :=
 
 /-- The preorder structure of `α →o β` is pointwise inequality: `f ≤ g ↔ ∀ a, f a ≤ g a`. -/
 instance : Preorder (α →o β) :=
-  @Preorder.lift (α →o β) (α → β) _ toFun
+  @Preorder.lift (α →o β) (α → β) _ DFunLike.coe
 
 instance {β : Type*} [PartialOrder β] : PartialOrder (α →o β) :=
   @PartialOrder.lift (α →o β) (α → β) _ toFun ext

Mathlib/Order/OmegaCompletePartialOrder.lean

@@ -67,42 +67,52 @@ namespace OmegaCompletePartialOrder
 
 /-- A chain is a monotone sequence.
 
+This is made a one-field structure around order homomorphisms `ℕ →o α` because we want to endow
+chains with the domination order rather than the pointwise order. See `Chain.instLE`.
+
 See the definition on page 114 of [gunter1992]. -/
-def Chain (α : Type u) [Preorder α] :=
-  ℕ →o α
+structure Chain (α : Type u) [Preorder α] extends ℕ →o α
 
 namespace Chain
 variable [Preorder α] [Preorder β] [Preorder γ]
 
-instance : FunLike (Chain α) ℕ α := inferInstanceAs <| FunLike (ℕ →o α) ℕ α
-instance : OrderHomClass (Chain α) ℕ α := inferInstanceAs <| OrderHomClass (ℕ →o α) ℕ α
+instance : FunLike (Chain α) ℕ α where
+  coe c := c.toOrderHom
+  coe_injective' := by rintro ⟨f, hf⟩; congr!
+
+initialize_simps_projections Chain (toFun → apply)
+
+instance : OrderHomClass (Chain α) ℕ α where
+  map_rel c _m _n hmn := c.monotone hmn
 
 /-- See note [partially-applied ext lemmas]. -/
 @[ext] lemma ext ⦃f g : Chain α⦄ (h : ⇑f = ⇑g) : f = g := DFunLike.ext' h
 
+@[simp] lemma coe_toOrderHom (c : Chain α) : ⇑c.toOrderHom = c := rfl
+
 instance [Inhabited α] : Inhabited (Chain α) :=
   ⟨⟨default, fun _ _ _ => le_rfl⟩⟩
 
-instance : Membership α (Chain α) :=
-  ⟨fun (c : ℕ →o α) a => ∃ i, a = c i⟩
+instance : Membership α (Chain α) where
+  mem c a := ∃ i, a = c i
 
 variable (c c' : Chain α)
 variable (f : α →o β)
 variable (g : β →o γ)
 
-instance : LE (Chain α) where le x y := ∀ i, ∃ j, x i ≤ y j
+instance instLE : LE (Chain α) where le x y := ∀ i, ∃ j, x i ≤ y j
 
 lemma isChain_range : IsChain (· ≤ ·) (Set.range c) := Monotone.isChain_range (OrderHomClass.mono c)
 
 lemma directed : Directed (· ≤ ·) c := directedOn_range.2 c.isChain_range.directedOn
 
 /-- `map` function for `Chain` -/
--- Not `@[simps]`: we need `@[simps!]` to see through the type synonym `Chain β = ℕ →o β`,
--- but then we'd get the `FunLike` instance for `OrderHom` instead.
-def map : Chain β :=
-  f.comp c
+@[simps toOrderHom]
+def map : Chain β where toOrderHom := f.comp c.toOrderHom
 
-@[simp] theorem map_coe : ⇑(map c f) = f ∘ c := rfl
+@[simp] lemma coe_map : ⇑(c.map f) = f ∘ c := rfl
+
+@[deprecated (since := "2026-03-27")] alias map_coe := coe_map
 
 variable {f}
 
@@ -119,25 +129,23 @@ theorem mem_map_iff {b : β} : b ∈ c.map f ↔ ∃ a, a ∈ c ∧ f a = b :=
     subst b
     apply mem_map c _ h⟩
 
-@[simp]
-theorem map_id : c.map OrderHom.id = c :=
-  OrderHom.comp_id _
+@[simp] lemma map_id : c.map OrderHom.id = c := by ext; simp
 
 theorem map_comp : (c.map f).map g = c.map (g.comp f) :=
   rfl
 
 @[mono]
-theorem map_le_map {g : α →o β} (h : f ≤ g) : c.map f ≤ c.map g :=
-  fun i => by simp only [map_coe, Function.comp_apply]; exists i; apply h
+theorem map_le_map {g : α →o β} (h : f ≤ g) : c.map f ≤ c.map g := fun _ ↦ ⟨_, h _⟩
 
 /-- `OmegaCompletePartialOrder.Chain.zip` pairs up the elements of two chains
 that have the same index. -/
--- Not `@[simps]`: we need `@[simps!]` to see through the type synonym `Chain β = ℕ →o β`,
--- but then we'd get the `FunLike` instance for `OrderHom` instead.
-def zip (c₀ : Chain α) (c₁ : Chain β) : Chain (α × β) :=
-  OrderHom.prod c₀ c₁
+@[simps toOrderHom]
+def zip (c₀ : Chain α) (c₁ : Chain β) : Chain (α × β) where
+  toOrderHom := c₀.toOrderHom.prod c₁.toOrderHom
+
+@[simp] lemma zip_apply (c₀ : Chain α) (c₁ : Chain β) (n : ℕ) : c₀.zip c₁ n = (c₀ n, c₁ n) := rfl
 
-@[simp] theorem zip_coe (c₀ : Chain α) (c₁ : Chain β) (n : ℕ) : c₀.zip c₁ n = (c₀ n, c₁ n) := rfl
+@[deprecated (since := "2026-03-27")] alias zip_coe := zip_apply
 
 /-- An example of a `Chain` constructed from an ordered pair. -/
 def pair (a b : α) (hab : a ≤ b) : Chain α where
@@ -154,7 +162,7 @@ def pair (a b : α) (hab : a ≤ b) : Chain α where
 
 @[simp] lemma pair_zip_pair (a₁ a₂ : α) (b₁ b₂ : β) (ha hb) :
     (pair a₁ a₂ ha).zip (pair b₁ b₂ hb) = pair (a₁, b₁) (a₂, b₂) (Prod.le_def.2 ⟨ha, hb⟩) := by
-  unfold Chain; ext n : 2; cases n <;> rfl
+  ext n : 2; cases n <;> rfl
 
 end Chain
 
@@ -263,7 +271,7 @@ lemma ωScottContinuous.monotone (h : ωScottContinuous f) : Monotone f :=
 
 lemma ωScottContinuous.isLUB {c : Chain α} (hf : ωScottContinuous f) :
     IsLUB (Set.range (c.map ⟨f, hf.monotone⟩)) (f (ωSup c)) := by
-  simpa [map_coe, OrderHom.coe_mk, Set.range_comp]
+  simpa [Set.range_comp]
     using hf (by simp) (Set.range_nonempty _) (isChain_range c).directedOn (isLUB_range_ωSup c)
 
 @[fun_prop, to_fun (attr := simp)]
@@ -278,7 +286,7 @@ lemma ωScottContinuous_iff_monotone_map_ωSup :
   refine ⟨fun hf ↦ ⟨hf.monotone, hf.map_ωSup⟩, ?_⟩
   intro hf _ ⟨c, hc⟩ _ _ _ hda
   convert isLUB_range_ωSup (c.map { toFun := f, monotone' := hf.1 })
-  · rw [map_coe, OrderHom.coe_mk, ← hc, ← (Set.range_comp f ⇑c)]
+  · simp [← hc, ← (Set.range_comp f ⇑c)]
   · rw [← hc] at hda
     rw [← hf.2 c, ωSup_eq_of_isLUB hda]
 
@@ -504,7 +512,7 @@ lemma ωScottContinuous.inf (hf : ωScottContinuous f) (hg : ωScottContinuous g
     ωScottContinuous (f ⊓ g) := by
   refine ωScottContinuous.of_monotone_map_ωSup
     ⟨hf.monotone.inf hg.monotone, fun c ↦ eq_of_forall_ge_iff fun a ↦ ?_⟩
-  simp only [Pi.inf_apply, hf.map_ωSup c, hg.map_ωSup c, inf_le_iff, ωSup_le_iff, Chain.map_coe,
+  simp only [Pi.inf_apply, hf.map_ωSup c, hg.map_ωSup c, inf_le_iff, ωSup_le_iff, Chain.coe_map,
     Function.comp, OrderHom.coe_mk, ← forall_or_left, ← forall_or_right]
   exact ⟨fun h _ ↦ h _ _, fun h i j ↦
     (h (max j i)).imp (le_trans <| hf.monotone <| c.mono <| le_max_left _ _)
@@ -606,15 +614,15 @@ theorem ωSup_bind {β γ : Type v} (c : Chain α) (f : α →o Part β) (g : α
     simp only [Part.mem_ωSup] at hb
     rcases hb with ⟨j, hb⟩
     replace hb := hb.symm
-    simp only [Part.eq_some_iff, Chain.map_coe, Function.comp_apply] at hy hb
+    simp only [Part.eq_some_iff, Chain.coe_map, Function.comp_apply] at hy hb
     replace hb : b ∈ f (c (max i j)) := f.mono (c.mono (le_max_right i j)) _ hb
     replace hy : y ∈ g (c (max i j)) b := g.mono (c.mono (le_max_left i j)) _ _ hy
     apply h''' (max i j)
-    simp only [Part.mem_bind_iff, Chain.map_coe,
+    simp only [Part.mem_bind_iff, Chain.coe_map,
       Function.comp_apply, OrderHom.partBind_coe]
     exact ⟨_, hb, hy⟩
   · intro i y hy
-    simp only [Part.mem_bind_iff, Chain.map_coe,
+    simp only [Part.mem_bind_iff, Chain.coe_map,
       Function.comp_apply, OrderHom.partBind_coe] at hy
     rcases hy with ⟨b, hb₀, hb₁⟩
     apply h''' b _
@@ -808,7 +816,7 @@ theorem ωSup_iterate_mem_fixedPoint (h : x ≤ f x) :
   apply le_antisymm
   · apply ωSup_le
     intro n
-    simp only [Chain.map_coe, OrderHomClass.coe_coe, comp_apply]
+    simp only [Chain.coe_map, OrderHomClass.coe_coe, comp_apply]
     have : iterateChain f x h (n.succ) = f (iterateChain f x h n) :=
       Function.iterate_succ_apply' ..
     rw [← this]

Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean

@@ -121,12 +121,9 @@ theorem lfpApprox_mono_left : Monotone (lfpApprox : (α →o α) → _) := by
     forall_eq_or_imp, le_sup_left, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
     true_and]
   intro i' h_lt
-  apply le_sup_of_le_right
-  apply le_sSup_of_le
-  · use i'
-  · apply le_trans (h _)
-    simp only [OrderHom.toFun_eq_coe]
-    exact g.monotone (ih i' h_lt)
+  grw [← le_sup_right]
+  refine le_sSup_of_le ⟨i', h_lt, rfl⟩ ?_
+  grw [h _, ih i' h_lt]
 
 theorem lfpApprox_mono_mid : Monotone (lfpApprox f) := by
   intro x₁ x₂ h a