chore(Order/FixedPoints): remove adaptation notes for OrderHom regard…

…ing lean4 issue #1910 (#19380)

this PR removes 3 porting notes regarding lean4 issue leanprover/lean4#1910, and makes adaptations to mathlib to make use of the newly working notation. Concretely, that means that `OrderHom.lfp f` now is written `f.lfp`, and similar for `OrderHom.dual` and `OrderHom.gfp`.

there might still be some `dual x` application left inside code with `open OrderHom`, but those are hard to filter for with grep, as there are many declarations named `dual` in different namespaces.

Mathlib/Order/FixedPoints.lean

@@ -51,76 +51,73 @@ def gfp : (α →o α) →o α where
   toFun f := sSup { a | a ≤ f a }
   monotone' _ _ hle := sSup_le_sSup fun a ha => le_trans ha (hle a)
 
-theorem lfp_le {a : α} (h : f a ≤ a) : lfp f ≤ a :=
+theorem lfp_le {a : α} (h : f a ≤ a) : f.lfp ≤ a :=
   sInf_le h
 
-theorem lfp_le_fixed {a : α} (h : f a = a) : lfp f ≤ a :=
+theorem lfp_le_fixed {a : α} (h : f a = a) : f.lfp ≤ a :=
   f.lfp_le h.le
 
-theorem le_lfp {a : α} (h : ∀ b, f b ≤ b → a ≤ b) : a ≤ lfp f :=
+theorem le_lfp {a : α} (h : ∀ b, f b ≤ b → a ≤ b) : a ≤ f.lfp :=
   le_sInf h
 
--- Porting note: for the rest of the file, replace the dot notation `_.lfp` with `lfp _`
--- same for `_.gfp`, `_.dual`
--- Probably related to https://github.com/leanprover/lean4/issues/1910
-theorem map_le_lfp {a : α} (ha : a ≤ lfp f) : f a ≤ lfp f :=
+theorem map_le_lfp {a : α} (ha : a ≤ f.lfp) : f a ≤ f.lfp :=
   f.le_lfp fun _ hb => (f.mono <| le_sInf_iff.1 ha _ hb).trans hb
 
 @[simp]
-theorem map_lfp : f (lfp f) = lfp f :=
-  have h : f (lfp f) ≤ lfp f := f.map_le_lfp le_rfl
+theorem map_lfp : f f.lfp = f.lfp :=
+  have h : f f.lfp ≤ f.lfp := f.map_le_lfp le_rfl
   h.antisymm <| f.lfp_le <| f.mono h
 
-theorem isFixedPt_lfp : IsFixedPt f (lfp f) :=
+theorem isFixedPt_lfp : IsFixedPt f f.lfp :=
   f.map_lfp
 
-theorem lfp_le_map {a : α} (ha : lfp f ≤ a) : lfp f ≤ f a :=
+theorem lfp_le_map {a : α} (ha : f.lfp ≤ a) : f.lfp ≤ f a :=
   calc
-    lfp f = f (lfp f) := f.map_lfp.symm
+    f.lfp = f f.lfp := f.map_lfp.symm
     _ ≤ f a := f.mono ha
 
-theorem isLeast_lfp_le : IsLeast { a | f a ≤ a } (lfp f) :=
+theorem isLeast_lfp_le : IsLeast { a | f a ≤ a } f.lfp :=
   ⟨f.map_lfp.le, fun _ => f.lfp_le⟩
 
-theorem isLeast_lfp : IsLeast (fixedPoints f) (lfp f) :=
+theorem isLeast_lfp : IsLeast (fixedPoints f) f.lfp :=
   ⟨f.isFixedPt_lfp, fun _ => f.lfp_le_fixed⟩
 
-theorem lfp_induction {p : α → Prop} (step : ∀ a, p a → a ≤ lfp f → p (f a))
-    (hSup : ∀ s, (∀ a ∈ s, p a) → p (sSup s)) : p (lfp f) := by
-  set s := { a | a ≤ lfp f ∧ p a }
+theorem lfp_induction {p : α → Prop} (step : ∀ a, p a → a ≤ f.lfp → p (f a))
+    (hSup : ∀ s, (∀ a ∈ s, p a) → p (sSup s)) : p f.lfp := by
+  set s := { a | a ≤ f.lfp ∧ p a }
   specialize hSup s fun a => And.right
-  suffices sSup s = lfp f from this ▸ hSup
-  have h : sSup s ≤ lfp f := sSup_le fun b => And.left
+  suffices sSup s = f.lfp from this ▸ hSup
+  have h : sSup s ≤ f.lfp := sSup_le fun b => And.left
   have hmem : f (sSup s) ∈ s := ⟨f.map_le_lfp h, step _ hSup h⟩
   exact h.antisymm (f.lfp_le <| le_sSup hmem)
 
-theorem le_gfp {a : α} (h : a ≤ f a) : a ≤ gfp f :=
+theorem le_gfp {a : α} (h : a ≤ f a) : a ≤ f.gfp :=
   le_sSup h
 
-theorem gfp_le {a : α} (h : ∀ b, b ≤ f b → b ≤ a) : gfp f ≤ a :=
+theorem gfp_le {a : α} (h : ∀ b, b ≤ f b → b ≤ a) : f.gfp ≤ a :=
   sSup_le h
 
-theorem isFixedPt_gfp : IsFixedPt f (gfp f) :=
+theorem isFixedPt_gfp : IsFixedPt f f.gfp :=
   f.dual.isFixedPt_lfp
 
 @[simp]
-theorem map_gfp : f (gfp f) = gfp f :=
+theorem map_gfp : f f.gfp = f.gfp :=
   f.dual.map_lfp
 
-theorem map_le_gfp {a : α} (ha : a ≤ gfp f) : f a ≤ gfp f :=
+theorem map_le_gfp {a : α} (ha : a ≤ f.gfp) : f a ≤ f.gfp :=
   f.dual.lfp_le_map ha
 
-theorem gfp_le_map {a : α} (ha : gfp f ≤ a) : gfp f ≤ f a :=
+theorem gfp_le_map {a : α} (ha : f.gfp ≤ a) : f.gfp ≤ f a :=
   f.dual.map_le_lfp ha
 
-theorem isGreatest_gfp_le : IsGreatest { a | a ≤ f a } (gfp f) :=
+theorem isGreatest_gfp_le : IsGreatest { a | a ≤ f a } f.gfp :=
   f.dual.isLeast_lfp_le
 
-theorem isGreatest_gfp : IsGreatest (fixedPoints f) (gfp f) :=
+theorem isGreatest_gfp : IsGreatest (fixedPoints f) f.gfp :=
   f.dual.isLeast_lfp
 
-theorem gfp_induction {p : α → Prop} (step : ∀ a, p a → gfp f ≤ a → p (f a))
-    (hInf : ∀ s, (∀ a ∈ s, p a) → p (sInf s)) : p (gfp f) :=
+theorem gfp_induction {p : α → Prop} (step : ∀ a, p a → f.gfp ≤ a → p (f a))
+    (hInf : ∀ s, (∀ a ∈ s, p a) → p (sInf s)) : p f.gfp :=
   f.dual.lfp_induction step hInf
 
 end Basic
@@ -130,53 +127,52 @@ section Eqn
 variable [CompleteLattice α] [CompleteLattice β] (f : β →o α) (g : α →o β)
 
 -- Rolling rule
-theorem map_lfp_comp : f (lfp (g.comp f)) = lfp (f.comp g) :=
+theorem map_lfp_comp : f (g.comp f).lfp = (f.comp g).lfp :=
   le_antisymm ((f.comp g).map_lfp ▸ f.mono (lfp_le_fixed _ <| congr_arg g (f.comp g).map_lfp)) <|
     lfp_le _ (congr_arg f (g.comp f).map_lfp).le
 
-theorem map_gfp_comp : f (gfp (g.comp f)) = gfp (f.comp g) :=
-  f.dual.map_lfp_comp (OrderHom.dual g)
+theorem map_gfp_comp : f (g.comp f).gfp = (f.comp g).gfp :=
+  f.dual.map_lfp_comp g.dual
 
 -- Diagonal rule
-theorem lfp_lfp (h : α →o α →o α) : lfp (lfp.comp h) = lfp h.onDiag := by
-  let a := lfp (lfp.comp h)
+theorem lfp_lfp (h : α →o α →o α) : (lfp.comp h).lfp = h.onDiag.lfp := by
+  let a := (lfp.comp h).lfp
   refine (lfp_le _ ?_).antisymm (lfp_le _ (Eq.le ?_))
   · exact lfp_le _ h.onDiag.map_lfp.le
   have ha : (lfp ∘ h) a = a := (lfp.comp h).map_lfp
   calc
-    h a a = h a (lfp (h a)) := congr_arg (h a) ha.symm
-    _ = lfp (h a) := (h a).map_lfp
+    h a a = h a (h a).lfp := congr_arg (h a) ha.symm
+    _ = (h a).lfp := (h a).map_lfp
     _ = a := ha
 
-theorem gfp_gfp (h : α →o α →o α) : gfp (gfp.comp h) = gfp h.onDiag :=
-  @lfp_lfp αᵒᵈ _ <| (OrderHom.dualIso αᵒᵈ αᵒᵈ).symm.toOrderEmbedding.toOrderHom.comp
-    (OrderHom.dual h)
+theorem gfp_gfp (h : α →o α →o α) : (gfp.comp h).gfp = h.onDiag.gfp :=
+  @lfp_lfp αᵒᵈ _ <| (OrderHom.dualIso αᵒᵈ αᵒᵈ).symm.toOrderEmbedding.toOrderHom.comp h.dual
 
 end Eqn
 
 section PrevNext
 
 variable [CompleteLattice α] (f : α →o α)
 
-theorem gfp_const_inf_le (x : α) : gfp (const α x ⊓ f) ≤ x :=
+theorem gfp_const_inf_le (x : α) : (const α x ⊓ f).gfp ≤ x :=
   (gfp_le _) fun _ hb => hb.trans inf_le_left
 
 /-- Previous fixed point of a monotone map. If `f` is a monotone self-map of a complete lattice and
 `x` is a point such that `f x ≤ x`, then `f.prevFixed x hx` is the greatest fixed point of `f`
 that is less than or equal to `x`. -/
 def prevFixed (x : α) (hx : f x ≤ x) : fixedPoints f :=
-  ⟨gfp (const α x ⊓ f),
+  ⟨(const α x ⊓ f).gfp,
     calc
-      f (gfp (const α x ⊓ f)) = x ⊓ f (gfp (const α x ⊓ f)) :=
+      f (const α x ⊓ f).gfp = x ⊓ f (const α x ⊓ f).gfp :=
         Eq.symm <| inf_of_le_right <| (f.mono <| f.gfp_const_inf_le x).trans hx
-      _ = gfp (const α x ⊓ f) := (const α x ⊓ f).map_gfp
+      _ = (const α x ⊓ f).gfp := (const α x ⊓ f).map_gfp
       ⟩
 
 /-- Next fixed point of a monotone map. If `f` is a monotone self-map of a complete lattice and
 `x` is a point such that `x ≤ f x`, then `f.nextFixed x hx` is the least fixed point of `f`
 that is greater than or equal to `x`. -/
 def nextFixed (x : α) (hx : x ≤ f x) : fixedPoints f :=
-  { f.dual.prevFixed x hx with val := lfp (const α x ⊔ f) }
+  { f.dual.prevFixed x hx with val := (const α x ⊔ f).lfp }
 
 theorem prevFixed_le {x : α} (hx : f x ≤ x) : ↑(f.prevFixed x hx) ≤ x :=
   f.gfp_const_inf_le x
@@ -240,7 +236,7 @@ instance : SemilatticeSup (fixedPoints f) :=
 /- porting note: removed `Subtype.partialOrder _` from mathlib3port version,
   threw `typeclass instance` error and was seemingly unnecessary?-/
 instance : SemilatticeInf (fixedPoints f) :=
-  { OrderDual.instSemilatticeInf (fixedPoints (OrderHom.dual f)) with
+  { OrderDual.instSemilatticeInf (fixedPoints f.dual) with
     inf := fun x y => f.prevFixed (x ⊓ y) (f.map_inf_fixedPoints_le x y) }
 
 -- Porting note: `coe` replaced with `Subtype.val`
@@ -271,8 +267,8 @@ instance completeLattice : CompleteLattice (fixedPoints f) where
   __ := inferInstanceAs (SemilatticeSup (fixedPoints f))
   __ := inferInstanceAs (CompleteSemilatticeInf (fixedPoints f))
   __ := inferInstanceAs (CompleteSemilatticeSup (fixedPoints f))
-  top := ⟨gfp f, f.isFixedPt_gfp⟩
-  bot := ⟨lfp f, f.isFixedPt_lfp⟩
+  top := ⟨f.gfp, f.isFixedPt_gfp⟩
+  bot := ⟨f.lfp, f.isFixedPt_lfp⟩
   le_top x := f.le_gfp x.2.ge
   bot_le x := f.lfp_le x.2.le
 
@@ -281,7 +277,7 @@ open OmegaCompletePartialOrder fixedPoints
 /-- **Kleene's fixed point Theorem**: The least fixed point in a complete lattice is
 the supremum of iterating a function on bottom arbitrary often. -/
 theorem lfp_eq_sSup_iterate (h : ωScottContinuous f) :
-    lfp f = ⨆ n, f^[n] ⊥ := by
+    f.lfp = ⨆ n, f^[n] ⊥ := by
   apply le_antisymm
   · apply lfp_le_fixed
     exact Function.mem_fixedPoints.mp (ωSup_iterate_mem_fixedPoint
@@ -290,8 +286,8 @@ theorem lfp_eq_sSup_iterate (h : ωScottContinuous f) :
     intro a h_a
     exact ωSup_iterate_le_prefixedPoint ⟨f, h.map_ωSup_of_orderHom⟩ ⊥ bot_le h_a bot_le
 
-theorem gfp_eq_sInf_iterate (h : ωScottContinuous (OrderHom.dual f)) :
-    gfp f = ⨅ n, f^[n] ⊤ :=
-  lfp_eq_sSup_iterate (OrderHom.dual f) h
+theorem gfp_eq_sInf_iterate (h : ωScottContinuous f.dual) :
+    f.gfp = ⨅ n, f^[n] ⊤ :=
+  lfp_eq_sSup_iterate f.dual h
 
 end fixedPoints

Mathlib/Order/Hom/Basic.lean

@@ -488,16 +488,13 @@ protected def dual : (α →o β) ≃ (αᵒᵈ →o βᵒᵈ) where
   left_inv _ := rfl
   right_inv _ := rfl
 
--- Porting note: We used to be able to write `(OrderHom.id : α →o α).dual` here rather than
--- `OrderHom.dual (OrderHom.id : α →o α)`.
--- See https://github.com/leanprover/lean4/issues/1910
 @[simp]
-theorem dual_id : OrderHom.dual (OrderHom.id : α →o α) = OrderHom.id :=
+theorem dual_id : (OrderHom.id : α →o α).dual = OrderHom.id :=
   rfl
 
 @[simp]
 theorem dual_comp (g : β →o γ) (f : α →o β) :
-    OrderHom.dual (g.comp f) = (OrderHom.dual g).comp (OrderHom.dual f) :=
+    (g.comp f).dual = g.dual.comp f.dual :=
   rfl
 
 @[simp]

Mathlib/Order/Hom/Bounded.lean

@@ -725,18 +725,18 @@ protected def dual :
     BoundedOrderHom α β ≃
       BoundedOrderHom αᵒᵈ
         βᵒᵈ where
-  toFun f := ⟨OrderHom.dual f.toOrderHom, f.map_bot', f.map_top'⟩
+  toFun f := ⟨f.toOrderHom.dual, f.map_bot', f.map_top'⟩
   invFun f := ⟨OrderHom.dual.symm f.toOrderHom, f.map_bot', f.map_top'⟩
   left_inv _ := ext fun _ => rfl
   right_inv _ := ext fun _ => rfl
 
 @[simp]
-theorem dual_id : BoundedOrderHom.dual (BoundedOrderHom.id α) = BoundedOrderHom.id _ :=
+theorem dual_id : (BoundedOrderHom.id α).dual = BoundedOrderHom.id _ :=
   rfl
 
 @[simp]
 theorem dual_comp (g : BoundedOrderHom β γ) (f : BoundedOrderHom α β) :
-    BoundedOrderHom.dual (g.comp f) = g.dual.comp (BoundedOrderHom.dual f) :=
+    (g.comp f).dual = g.dual.comp f.dual :=
   rfl
 
 @[simp]

Mathlib/Order/Interval/Basic.lean

@@ -153,7 +153,7 @@ theorem map_map (g : β →o γ) (f : α →o β) (a : NonemptyInterval α) :
 
 @[simp]
 theorem dual_map (f : α →o β) (a : NonemptyInterval α) :
-    dual (a.map f) = a.dual.map (OrderHom.dual f) :=
+    dual (a.map f) = a.dual.map f.dual :=
   rfl
 
 /-- Binary pushforward of nonempty intervals. -/
@@ -360,7 +360,7 @@ theorem map_map (g : β →o γ) (f : α →o β) (s : Interval α) : (s.map f).
   Option.map_map _ _ _
 
 @[simp]
-theorem dual_map (f : α →o β) (s : Interval α) : dual (s.map f) = s.dual.map (OrderHom.dual f) := by
+theorem dual_map (f : α →o β) (s : Interval α) : dual (s.map f) = s.dual.map f.dual := by
   cases s
   · rfl
   · exact WithBot.map_comm rfl _

Mathlib/SetTheory/Cardinal/SchroederBernstein.lean

@@ -49,8 +49,7 @@ theorem schroeder_bernstein {f : α → β} {g : β → α} (hf : Function.Injec
     { toFun := fun s => (g '' (f '' s)ᶜ)ᶜ
       monotone' := fun s t hst =>
         compl_subset_compl.mpr <| image_subset _ <| compl_subset_compl.mpr <| image_subset _ hst }
-  -- Porting note: dot notation `F.lfp` doesn't work here
-  set s : Set α := OrderHom.lfp F
+  set s : Set α := F.lfp
   have hs : (g '' (f '' s)ᶜ)ᶜ = s := F.map_lfp
   have hns : g '' (f '' s)ᶜ = sᶜ := compl_injective (by simp [hs])
   set g' := invFun g

Mathlib/SetTheory/Ordinal/FixedPointApproximants.lean

@@ -226,9 +226,9 @@ theorem lfpApprox_le_of_mem_fixedPoints {a : α}
 
 /-- 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 #α) = lfp f := by
+theorem lfpApprox_ord_eq_lfp : lfpApprox f ⊥ (ord <| succ #α) = f.lfp := by
   apply le_antisymm
-  · have h_lfp : ∃ y : fixedPoints f, lfp f = y := by use ⊥; exact rfl
+  · 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 #α)
   · have h_fix : ∃ y : fixedPoints f, lfpApprox f ⊥ (ord <| succ #α) = y := by
@@ -238,7 +238,7 @@ theorem lfpApprox_ord_eq_lfp : lfpApprox f ⊥ (ord <| succ #α) = lfp f := by
     exact lfp_le_fixed f x.prop
 
 /-- Some approximation of the least fixed point starting from `⊥` is the least fixed point. -/
-theorem lfp_mem_range_lfpApprox : lfp f ∈ Set.range (lfpApprox f ⊥) := by
+theorem lfp_mem_range_lfpApprox : f.lfp ∈ Set.range (lfpApprox f ⊥) := by
   use ord <| succ #α
   exact lfpApprox_ord_eq_lfp f
 
@@ -256,52 +256,52 @@ decreasing_by exact h
 unseal gfpApprox lfpApprox
 
 theorem gfpApprox_antitone : Antitone (gfpApprox f x) :=
-  lfpApprox_monotone (OrderHom.dual f) x
+  lfpApprox_monotone f.dual x
 
 theorem gfpApprox_le {a : Ordinal} : gfpApprox f x a ≤ x :=
-  le_lfpApprox (OrderHom.dual f) x
+  le_lfpApprox f.dual x
 
 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
+  lfpApprox_add_one f.dual x h a
 
 theorem gfpApprox_mono_left : Monotone (gfpApprox : (α →o α) → _) := by
   intro f g h
-  have : OrderHom.dual g ≤ OrderHom.dual f := h
+  have : g.dual ≤ f.dual := h
   exact lfpApprox_mono_left this
 
 theorem gfpApprox_mono_mid : Monotone (gfpApprox f) :=
-  fun _ _ h => lfpApprox_mono_mid (OrderHom.dual f) h
+  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)
     (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
+  lfpApprox_eq_of_mem_fixedPoints f.dual x h_init h_ab h
 
 /-- There are distinct indices smaller than the successor of the domain's cardinality
 yielding the same value -/
 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
+  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) :
     gfpApprox f x (ord <| succ #α) ∈ fixedPoints f :=
-  lfpApprox_ord_mem_fixedPoint (OrderHom.dual f) x h_init
+  lfpApprox_ord_mem_fixedPoint f.dual x h_init
 
 /-- 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 (OrderHom.dual f) x h_a h_le_init i
+  lfpApprox_le_of_mem_fixedPoints f.dual x h_a h_le_init i
 
 /-- The approximation sequence converges at the successor of the domain's cardinality
 to the greatest fixed point if starting from `⊥` -/
-theorem gfpApprox_ord_eq_gfp : gfpApprox f ⊤ (ord <| succ #α) = gfp f :=
-  lfpApprox_ord_eq_lfp (OrderHom.dual f)
+theorem gfpApprox_ord_eq_gfp : gfpApprox f ⊤ (ord <| succ #α) = f.gfp :=
+  lfpApprox_ord_eq_lfp f.dual
 
 /-- Some approximation of the least fixed point starting from `⊤` is the greatest fixed point. -/
-theorem gfp_mem_range_gfpApprox : gfp f ∈ Set.range (gfpApprox f ⊤) :=
-  lfp_mem_range_lfpApprox (OrderHom.dual f)
+theorem gfp_mem_range_gfpApprox : f.gfp ∈ Set.range (gfpApprox f ⊤) :=
+  lfp_mem_range_lfpApprox f.dual
 
 end OrdinalApprox