chore: fix double conflicting instances of OmegaCompletePartialOrder on CompleteLattice (#38297)

Currently, we have a direct instance `CompleteLattice -> OmegaCompletePartialOrder` (in `OmegaCompletePartialOrder.lean`), and a path `CompleteLattice -> ChainCompletePartialOrder -> OmegaCompletePartialOrder` (in `BourbakiWitt.lean`). They are defeq, but not implicit-reducibly. To solve the diamond, we remove the first instance, and move everything that depends on it from the first file to the second file.

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author: sgouezel

Mathlib/LinearAlgebra/Span/Basic.lean

@@ -12,7 +12,7 @@ public import Mathlib.Algebra.Module.Submodule.Equiv
 public import Mathlib.Algebra.Module.Submodule.Pointwise
 public import Mathlib.LinearAlgebra.Span.Defs
 public import Mathlib.Order.CompactlyGenerated.Basic
-public import Mathlib.Order.OmegaCompletePartialOrder
+public import Mathlib.Order.BourbakiWitt
 
 import Mathlib.Algebra.Field.Basic
 import Mathlib.Algebra.Module.Submodule.EqLocus

Mathlib/Order/BourbakiWitt.lean

@@ -32,7 +32,7 @@ The proof used can be found in [serge_lang_algebra]
 
 public section
 
-variable {α : Type*}
+variable {α β : Type*} {ι : Sort*}
 
 /-- The type of nonempty chains of an order -/
 @[ext]
@@ -228,3 +228,56 @@ theorem nonempty_fixedPoints_of_inflationary [Nonempty α] (le_map : ∀ x, x 
   exact ⟨(bot_isAdmissible le_map).cSup_mem _ (subset_refl _), rfl⟩
 
 end ChainCompletePartialOrder
+
+open OmegaCompletePartialOrder
+
+namespace CompleteLattice
+
+variable [OmegaCompletePartialOrder α] [CompleteLattice β] {f g : α → β}
+
+lemma ωScottContinuous.iSup {f : ι → α → β} (hf : ∀ i, ωScottContinuous (f i)) :
+    ωScottContinuous (⨆ i, f i) := by
+  refine ωScottContinuous.of_monotone_map_ωSup
+    ⟨Monotone.iSup fun i ↦ (hf i).monotone, fun c ↦ eq_of_forall_ge_iff fun a ↦ ?_⟩
+  simp +contextual [ωSup_le_iff, (hf _).map_ωSup, @forall_comm ι]
+
+lemma ωScottContinuous.sSup {s : Set (α → β)} (hs : ∀ f ∈ s, ωScottContinuous f) :
+    ωScottContinuous (sSup s) := by
+  rw [sSup_eq_iSup]; apply ωScottContinuous.iSup fun f ↦ ωScottContinuous.iSup <| hs f
+
+lemma ωScottContinuous.sup (hf : ωScottContinuous f) (hg : ωScottContinuous g) :
+    ωScottContinuous (f ⊔ g) := by
+  rw [← sSup_pair]
+  apply ωScottContinuous.sSup
+  rintro f (rfl | rfl | _) <;> assumption
+
+lemma ωScottContinuous.top : ωScottContinuous (⊤ : α → β) :=
+  ωScottContinuous.of_monotone_map_ωSup
+    ⟨monotone_const, fun c ↦ eq_of_forall_ge_iff fun a ↦ by simp⟩
+
+lemma ωScottContinuous.bot : ωScottContinuous (⊥ : α → β) := by
+  rw [← sSup_empty]; exact ωScottContinuous.sSup (by simp)
+
+end CompleteLattice
+
+namespace CompleteLattice
+
+variable [OmegaCompletePartialOrder α] [CompleteLinearOrder β] {f g : α → β}
+
+-- TODO Prove this result for `ScottContinuousOn` and deduce this as a special case
+-- Also consider if it holds in greater generality (e.g. finite sets)
+-- N.B. The Scott Topology coincides with the Upper Topology on a Complete Linear Order
+-- `Topology.IsScott.scott_eq_upper_of_completeLinearOrder`
+-- We have that the product topology coincides with the upper topology
+-- https://github.com/leanprover-community/mathlib4/pull/12133
+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.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 _ _)
+      (le_trans <| hg.monotone <| c.mono <| le_max_right _ _)⟩
+
+end CompleteLattice

Mathlib/Order/Category/OmegaCompletePartialOrder.lean

@@ -5,7 +5,7 @@ Authors: Simon Hudon
 -/
 module
 
-public import Mathlib.Order.OmegaCompletePartialOrder
+public import Mathlib.Order.BourbakiWitt
 public import Mathlib.CategoryTheory.Limits.Shapes.Products
 public import Mathlib.CategoryTheory.Limits.Shapes.Equalizers
 public import Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers

Mathlib/Order/FixedPoints.lean

@@ -7,7 +7,7 @@ module
 
 public import Mathlib.Dynamics.FixedPoints.Basic
 public import Mathlib.Order.Hom.Order
-public import Mathlib.Order.OmegaCompletePartialOrder
+public import Mathlib.Order.BourbakiWitt
 
 /-!
 # Fixed point construction on complete lattices

Mathlib/Order/OmegaCompletePartialOrder.lean

@@ -33,7 +33,8 @@ supremum helps define the meaning of recursive procedures.
 ## Instances of `OmegaCompletePartialOrder`
 
 * `Part`
-* every `CompleteLattice`
+* every `CompleteLattice` (proved in `BourbakiWitt` as a special case of chain-complete
+  partial orders)
 * pi-types
 * product types
 * `OrderHom`
@@ -460,65 +461,6 @@ lemma ωScottContinuous_snd : ωScottContinuous (Prod.snd : α × β → β) :=
 
 end Prod
 
-namespace CompleteLattice
-
--- see Note [lower instance priority]
-/-- Any complete lattice has an `ω`-CPO structure where the countable supremum is a special case
-of arbitrary suprema. -/
-instance (priority := 100) [CompleteLattice α] : OmegaCompletePartialOrder α where
-  ωSup c := ⨆ i, c i
-  ωSup_le := fun ⟨c, _⟩ s hs => by simpa only [iSup_le_iff]
-  le_ωSup := fun ⟨c, _⟩ i => le_iSup_of_le i le_rfl
-
-variable [OmegaCompletePartialOrder α] [CompleteLattice β] {f g : α → β}
-
-lemma ωScottContinuous.iSup {f : ι → α → β} (hf : ∀ i, ωScottContinuous (f i)) :
-    ωScottContinuous (⨆ i, f i) := by
-  refine ωScottContinuous.of_monotone_map_ωSup
-    ⟨Monotone.iSup fun i ↦ (hf i).monotone, fun c ↦ eq_of_forall_ge_iff fun a ↦ ?_⟩
-  simp +contextual [ωSup_le_iff, (hf _).map_ωSup, @forall_comm ι]
-
-lemma ωScottContinuous.sSup {s : Set (α → β)} (hs : ∀ f ∈ s, ωScottContinuous f) :
-    ωScottContinuous (sSup s) := by
-  rw [sSup_eq_iSup]; exact ωScottContinuous.iSup fun f ↦ ωScottContinuous.iSup <| hs f
-
-lemma ωScottContinuous.sup (hf : ωScottContinuous f) (hg : ωScottContinuous g) :
-    ωScottContinuous (f ⊔ g) := by
-  rw [← sSup_pair]
-  apply ωScottContinuous.sSup
-  rintro f (rfl | rfl | _) <;> assumption
-
-lemma ωScottContinuous.top : ωScottContinuous (⊤ : α → β) :=
-  ωScottContinuous.of_monotone_map_ωSup
-    ⟨monotone_const, fun c ↦ eq_of_forall_ge_iff fun a ↦ by simp⟩
-
-lemma ωScottContinuous.bot : ωScottContinuous (⊥ : α → β) := by
-  rw [← sSup_empty]; exact ωScottContinuous.sSup (by simp)
-
-end CompleteLattice
-
-namespace CompleteLattice
-
-variable [OmegaCompletePartialOrder α] [CompleteLinearOrder β] {f g : α → β}
-
--- TODO Prove this result for `ScottContinuousOn` and deduce this as a special case
--- Also consider if it holds in greater generality (e.g. finite sets)
--- N.B. The Scott Topology coincides with the Upper Topology on a Complete Linear Order
--- `Topology.IsScott.scott_eq_upper_of_completeLinearOrder`
--- We have that the product topology coincides with the upper topology
--- https://github.com/leanprover-community/mathlib4/pull/12133
-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.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 _ _)
-      (le_trans <| hg.monotone <| c.mono <| le_max_right _ _)⟩
-
-end CompleteLattice
-
 namespace OmegaCompletePartialOrder
 variable [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β]
 variable [OmegaCompletePartialOrder γ] [OmegaCompletePartialOrder δ]

Mathlib/Topology/OmegaCompletePartialOrder.lean

@@ -5,7 +5,7 @@ Authors: Simon Hudon
 -/
 module
 
-public import Mathlib.Order.OmegaCompletePartialOrder
+public import Mathlib.Order.BourbakiWitt
 public import Mathlib.Topology.Order.ScottTopology
 
 /-!