chore: use IsLUB IsGLB in ConditionallyCompleteLattice (#35774)

Also, some docstrings in `Order.ConditionallyCompleteLattice.Defs` are outdated (they still use Lean3 structure notation).
#36671 is an orthogonal PR to fix this.

Author: astrainfinita

Mathlib/Algebra/Tropical/Lattice.lean

@@ -55,16 +55,11 @@ instance [SupSet R] : SupSet (Tropical R) where sSup s := trop (sSup (untrop ''
 instance [InfSet R] : InfSet (Tropical R) where sInf s := trop (sInf (untrop '' s))
 
 instance instConditionallyCompleteLatticeTropical [ConditionallyCompleteLattice R] :
-    ConditionallyCompleteLattice (Tropical R) :=
-  { instLatticeTropical with
-    le_csSup := fun _s _x hs hx ↦
-      le_csSup (untrop_monotone.map_bddAbove hs) (Set.mem_image_of_mem untrop hx)
-    csSup_le := fun _s _x hs hx ↦
-      csSup_le (hs.image untrop) (untrop_monotone.mem_upperBounds_image hx)
-    le_csInf := fun _s _x hs hx ↦
-      le_csInf (hs.image untrop) (untrop_monotone.mem_lowerBounds_image hx)
-    csInf_le := fun _s _x hs hx ↦
-      csInf_le (untrop_monotone.map_bddBelow hs) (Set.mem_image_of_mem untrop hx) }
+    ConditionallyCompleteLattice (Tropical R) where
+  isLUB_csSup _ hn hb :=
+    .of_image untrop_le_iff <| isLUB_csSup (hn.image _) (untrop_monotone.map_bddAbove hb)
+  isGLB_csInf _ hn hb :=
+    .of_image untrop_le_iff <| isGLB_csInf (hn.image _) (untrop_monotone.map_bddBelow hb)
 
 instance [ConditionallyCompleteLinearOrder R] : ConditionallyCompleteLinearOrder (Tropical R) :=
   { instConditionallyCompleteLatticeTropical, Tropical.instLinearOrderTropical with

Mathlib/Data/Int/ConditionallyCompleteOrder.lean

@@ -34,22 +34,12 @@ instance instConditionallyCompleteLinearOrder : ConditionallyCompleteLinearOrder
     if h : s.Nonempty ∧ BddBelow s then
       leastOfBdd (Classical.choose h.2) (Classical.choose_spec h.2) h.1
     else 0
-  le_csSup s n hs hns := by
-    have : s.Nonempty ∧ BddAbove s := ⟨⟨n, hns⟩, hs⟩
-    simp only [dif_pos this]
-    exact (greatestOfBdd _ _ _).2.2 n hns
-  csSup_le s n hs hns := by
-    have : s.Nonempty ∧ BddAbove s := ⟨hs, ⟨n, hns⟩⟩
-    simp only [dif_pos this]
-    exact hns (greatestOfBdd _ (Classical.choose_spec this.2) _).2.1
-  csInf_le s n hs hns := by
-    have : s.Nonempty ∧ BddBelow s := ⟨⟨n, hns⟩, hs⟩
-    simp only [dif_pos this]
-    exact (leastOfBdd _ _ _).2.2 n hns
-  le_csInf s n hs hns := by
-    have : s.Nonempty ∧ BddBelow s := ⟨hs, ⟨n, hns⟩⟩
-    simp only [dif_pos this]
-    exact hns (leastOfBdd _ (Classical.choose_spec this.2) _).2.1
+  isLUB_csSup _ hn hb := by
+    rw [dif_pos ⟨hn, hb⟩]
+    exact (isGreatest_coe_greatestOfBdd ..).isLUB
+  isGLB_csInf _ hn hb := by
+    rw [dif_pos ⟨hn, hb⟩]
+    exact (isLeast_coe_leastOfBdd ..).isGLB
   csSup_of_not_bddAbove := fun s hs ↦ by simp [hs]
   csInf_of_not_bddBelow := fun s hs ↦ by simp [hs]
 

Mathlib/Data/Nat/Lattice.lean

@@ -130,11 +130,8 @@ open scoped Classical in
 noncomputable instance : ConditionallyCompleteLinearOrderBot ℕ :=
   { (inferInstance : OrderBot ℕ), (LinearOrder.toLattice : Lattice ℕ),
     (inferInstance : LinearOrder ℕ) with
-    le_csSup := fun s a hb ha ↦ by rw [sSup_def hb]; revert a ha; exact @Nat.find_spec _ _ hb
-    csSup_le := fun s a _ ha ↦ by rw [sSup_def ⟨a, ha⟩]; exact Nat.find_min' _ ha
-    le_csInf := fun s a hs hb ↦ by
-      rw [sInf_def hs]; exact hb (@Nat.find_spec (fun n ↦ n ∈ s) _ _)
-    csInf_le := fun s a _ ha ↦ by rw [sInf_def ⟨a, ha⟩]; exact Nat.find_min' _ ha
+    isLUB_csSup _ hn hb := sSup_def hb ▸ Nat.isLeast_find hb
+    isGLB_csInf _ hn hb := sInf_def hn ▸ (Nat.isLeast_find hn).isGLB
     csSup_empty := by
       simp only [sSup_def, Set.mem_empty_iff_false, forall_const, forall_prop_of_false,
         not_false_iff, exists_const]

Mathlib/Data/Real/Archimedean.lean

@@ -137,10 +137,8 @@ protected theorem isGLB_sInf (h₁ : s.Nonempty) (h₂ : BddBelow s) : IsGLB s (
 noncomputable instance : ConditionallyCompleteLinearOrder ℝ where
   __ := Real.linearOrder
   __ := Real.lattice
-  le_csSup s a hs ha := (Real.isLUB_sSup ⟨a, ha⟩ hs).1 ha
-  csSup_le s a hs ha := (Real.isLUB_sSup hs ⟨a, ha⟩).2 ha
-  csInf_le s a hs ha := (Real.isGLB_sInf ⟨a, ha⟩ hs).1 ha
-  le_csInf s a hs ha := (Real.isGLB_sInf hs ⟨a, ha⟩).2 ha
+  isLUB_csSup _ := Real.isLUB_sSup
+  isGLB_csInf _ := Real.isGLB_sInf
   csSup_of_not_bddAbove s hs := by simp [hs, sSup_def]
   csInf_of_not_bddBelow s hs := by simp [hs, sInf_def, sSup_def]
 

Mathlib/Order/CompleteLatticeIntervals.lean

@@ -127,22 +127,12 @@ noncomputable abbrev subsetConditionallyCompleteLinearOrder [Inhabited s]
     (h_Inf : ∀ {t : Set s} (_ : t.Nonempty) (_h_bdd : BddBelow t), sInf ((↑) '' t : Set α) ∈ s) :
     ConditionallyCompleteLinearOrder s :=
   { subsetSupSet s, subsetInfSet s, DistribLattice.toLattice, (inferInstance : LinearOrder s) with
-    le_csSup := by
-      rintro t c h_bdd hct
-      rw [← Subtype.coe_le_coe, ← subset_sSup_of_within s ⟨c, hct⟩ h_bdd (h_Sup ⟨c, hct⟩ h_bdd)]
-      exact (Subtype.mono_coe _).le_csSup_image hct h_bdd
-    csSup_le := by
-      rintro t B ht hB
-      rw [← Subtype.coe_le_coe, ← subset_sSup_of_within s ht ⟨B, hB⟩ (h_Sup ht ⟨B, hB⟩)]
-      exact (Subtype.mono_coe (· ∈ s)).csSup_image_le ht hB
-    le_csInf := by
-      intro t B ht hB
-      rw [← Subtype.coe_le_coe, ← subset_sInf_of_within s ht ⟨B, hB⟩ (h_Inf ht ⟨B, hB⟩)]
-      exact (Subtype.mono_coe (· ∈ s)).le_csInf_image ht hB
-    csInf_le := by
-      rintro t c h_bdd hct
-      rw [← Subtype.coe_le_coe, ← subset_sInf_of_within s ⟨c, hct⟩ h_bdd (h_Inf ⟨c, hct⟩ h_bdd)]
-      exact (Subtype.mono_coe (· ∈ s)).csInf_image_le hct h_bdd
+    isLUB_csSup t ht h_bdd := .of_image Subtype.coe_le_coe <| by
+      rw [← subset_sSup_of_within s ht h_bdd (h_Sup ht h_bdd)]
+      exact isLUB_csSup (ht.image _) ((Subtype.mono_coe _).map_bddAbove h_bdd)
+    isGLB_csInf t ht h_bdd := .of_image Subtype.coe_le_coe <| by
+      rw [← subset_sInf_of_within s ht h_bdd (h_Inf ht h_bdd)]
+      exact isGLB_csInf (ht.image _) ((Subtype.mono_coe _).map_bddBelow h_bdd)
     csSup_of_not_bddAbove := fun t ht ↦ by simp [ht]
     csInf_of_not_bddBelow := fun t ht ↦ by simp [ht] }
 

Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

@@ -147,10 +147,8 @@ attribute [instance 100] ConditionallyCompleteLinearOrderBot.toOrderBot
 on the properties of sInf and sSup in a complete lattice. -/
 instance (priority := 100) CompleteLattice.toConditionallyCompleteLattice [CompleteLattice α] :
     ConditionallyCompleteLattice α where
-  le_csSup := by intros; apply le_sSup; assumption
-  csSup_le := by intros; apply sSup_le; assumption
-  csInf_le := by intros; apply sInf_le; assumption
-  le_csInf := by intros; apply le_sInf; assumption
+  isLUB_csSup _ _ _ := isLUB_sSup _
+  isGLB_csInf _ _ _ := isGLB_sInf _
 
 -- see Note [lower instance priority]
 instance (priority := 100) CompleteLinearOrder.toConditionallyCompleteLinearOrderBot {α : Type*}
@@ -165,10 +163,8 @@ namespace OrderDual
 
 instance instConditionallyCompleteLattice (α : Type*) [ConditionallyCompleteLattice α] :
     ConditionallyCompleteLattice αᵒᵈ where
-  le_csSup := ConditionallyCompleteLattice.csInf_le (α := α)
-  csSup_le := ConditionallyCompleteLattice.le_csInf (α := α)
-  le_csInf := ConditionallyCompleteLattice.csSup_le (α := α)
-  csInf_le := ConditionallyCompleteLattice.le_csSup (α := α)
+  isLUB_csSup := ConditionallyCompleteLattice.isGLB_csInf (α := α)
+  isGLB_csInf := ConditionallyCompleteLattice.isLUB_csSup (α := α)
 
 instance (α : Type*) [ConditionallyCompleteLinearOrder α] :
     ConditionallyCompleteLinearOrder αᵒᵈ where
@@ -183,17 +179,23 @@ section ConditionallyCompleteLattice
 
 variable [ConditionallyCompleteLattice α] {s t : Set α} {a b : α}
 
+theorem isLUB_csSup (hn : s.Nonempty) (hb : BddAbove s) : IsLUB s (sSup s) :=
+  ConditionallyCompleteLattice.isLUB_csSup _ hn hb
+
+theorem isGLB_csInf (hn : s.Nonempty) (hb : BddBelow s) : IsGLB s (sInf s) :=
+  ConditionallyCompleteLattice.isGLB_csInf _ hn hb
+
 theorem le_csSup (h₁ : BddAbove s) (h₂ : a ∈ s) : a ≤ sSup s :=
-  ConditionallyCompleteLattice.le_csSup s a h₁ h₂
+  (isLUB_csSup (nonempty_of_mem h₂) h₁).1 h₂
 
 theorem csSup_le (h₁ : s.Nonempty) (h₂ : ∀ b ∈ s, b ≤ a) : sSup s ≤ a :=
-  ConditionallyCompleteLattice.csSup_le s a h₁ h₂
+  (isLUB_csSup h₁ ⟨a, h₂⟩).2 h₂
 
 theorem csInf_le (h₁ : BddBelow s) (h₂ : a ∈ s) : sInf s ≤ a :=
-  ConditionallyCompleteLattice.csInf_le s a h₁ h₂
+  (isGLB_csInf (nonempty_of_mem h₂) h₁).1 h₂
 
 theorem le_csInf (h₁ : s.Nonempty) (h₂ : ∀ b ∈ s, a ≤ b) : a ≤ sInf s :=
-  ConditionallyCompleteLattice.le_csInf s a h₁ h₂
+  (isGLB_csInf h₁ ⟨a, h₂⟩).2 h₂
 
 theorem le_csSup_of_le (hs : BddAbove s) (hb : b ∈ s) (h : a ≤ b) : a ≤ sSup s :=
   le_trans h (le_csSup hs hb)
@@ -216,12 +218,6 @@ theorem le_csSup_iff (h : BddAbove s) (hs : s.Nonempty) :
 theorem csInf_le_iff (h : BddBelow s) (hs : s.Nonempty) : sInf s ≤ a ↔ ∀ b ∈ lowerBounds s, b ≤ a :=
   ⟨fun h _ hb => le_trans (le_csInf hs hb) h, fun hb => hb _ fun _ => csInf_le h⟩
 
-theorem isLUB_csSup (ne : s.Nonempty) (H : BddAbove s) : IsLUB s (sSup s) :=
-  ⟨fun _ => le_csSup H, fun _ => csSup_le ne⟩
-
-theorem isGLB_csInf (ne : s.Nonempty) (H : BddBelow s) : IsGLB s (sInf s) :=
-  ⟨fun _ => csInf_le H, fun _ => le_csInf ne⟩
-
 theorem IsLUB.csSup_eq (H : IsLUB s a) (ne : s.Nonempty) : sSup s = a :=
   (isLUB_csSup ne ⟨a, H.1⟩).unique H
 
@@ -230,8 +226,8 @@ theorem IsGLB.csInf_eq (H : IsGLB s a) (ne : s.Nonempty) : sInf s = a :=
 
 instance (priority := 100) ConditionallyCompleteLattice.toConditionallyCompletePartialOrder :
     ConditionallyCompletePartialOrder α where
-  isGLB_csInf_of_directed _ _ non bdd := isGLB_csInf non bdd
-  isLUB_csSup_of_directed _ _ non bdd := isLUB_csSup non bdd
+  isGLB_csInf_of_directed _ _ := isGLB_csInf _
+  isLUB_csSup_of_directed _ _ := isLUB_csSup _
 
 theorem subset_Icc_csInf_csSup (hb : BddBelow s) (ha : BddAbove s) : s ⊆ Icc (sInf s) (sSup s) :=
   fun _ hx => ⟨csInf_le hb hx, le_csSup ha hx⟩
@@ -386,14 +382,12 @@ end ConditionallyCompleteLattice
 
 instance Pi.conditionallyCompleteLattice {ι : Type*} {α : ι → Type*}
     [∀ i, ConditionallyCompleteLattice (α i)] : ConditionallyCompleteLattice (∀ i, α i) where
-  le_csSup := fun _ f ⟨g, hg⟩ hf i =>
-    le_csSup ⟨g i, Set.forall_mem_range.2 fun ⟨_, hf'⟩ => hg hf' i⟩ ⟨⟨f, hf⟩, rfl⟩
-  csSup_le s _ hs hf i :=
-    (csSup_le (by have := hs.to_subtype; apply range_nonempty)) fun _ ⟨⟨_, hg⟩, hb⟩ => hb ▸ hf hg i
-  csInf_le := fun _ f ⟨g, hg⟩ hf i =>
-    csInf_le ⟨g i, Set.forall_mem_range.2 fun ⟨_, hf'⟩ => hg hf' i⟩ ⟨⟨f, hf⟩, rfl⟩
-  le_csInf s _ hs hf i :=
-    (le_csInf (by have := hs.to_subtype; apply range_nonempty)) fun _ ⟨⟨_, hg⟩, hb⟩ => hb ▸ hf hg i
+  isLUB_csSup _ hn hb := isLUB_pi.mpr fun _ ↦ by
+    rw [sSup_apply_eq_sSup_image]
+    exact isLUB_csSup (image_nonempty.mpr hn) ((monotone_eval _).map_bddAbove hb)
+  isGLB_csInf _ hn hb := isGLB_pi.mpr fun _ ↦ by
+    rw [sInf_apply_eq_sInf_image]
+    exact isGLB_csInf (image_nonempty.mpr hn) ((monotone_eval _).map_bddBelow hb)
 
 section ConditionallyCompleteLinearOrder
 
@@ -872,19 +866,15 @@ This result can be used to show that the extended reals `[-∞, ∞]` are a comp
 gives a conditionally complete lattice -/
 noncomputable instance WithTop.conditionallyCompleteLattice {α : Type*}
     [ConditionallyCompleteLattice α] : ConditionallyCompleteLattice (WithTop α) where
-  le_csSup _ a _ haS := (WithTop.isLUB_sSup' ⟨a, haS⟩).1 haS
-  csSup_le _ _ hS haS := (WithTop.isLUB_sSup' hS).2 haS
-  csInf_le _ _ hS haS := (WithTop.isGLB_sInf' hS).1 haS
-  le_csInf _ a _ haS := (WithTop.isGLB_sInf' ⟨a, haS⟩).2 haS
+  isLUB_csSup _ hS _ := WithTop.isLUB_sSup' hS
+  isGLB_csInf _ _ hS := WithTop.isGLB_sInf' hS
 
 /-- Adding a bottom element to a conditionally complete lattice
 gives a conditionally complete lattice -/
 noncomputable instance WithBot.conditionallyCompleteLattice {α : Type*}
     [ConditionallyCompleteLattice α] : ConditionallyCompleteLattice (WithBot α) where
-  le_csSup := (WithTop.conditionallyCompleteLattice (α := αᵒᵈ)).csInf_le
-  csSup_le := (WithTop.conditionallyCompleteLattice (α := αᵒᵈ)).le_csInf
-  csInf_le := (WithTop.conditionallyCompleteLattice (α := αᵒᵈ)).le_csSup
-  le_csInf := (WithTop.conditionallyCompleteLattice (α := αᵒᵈ)).csSup_le
+  isLUB_csSup := (WithTop.conditionallyCompleteLattice (α := αᵒᵈ)).isGLB_csInf
+  isGLB_csInf := (WithTop.conditionallyCompleteLattice (α := αᵒᵈ)).isLUB_csSup
 
 noncomputable instance [CompleteLattice α] : CompleteLattice (WithBot α) where
   isLUB_sSup s := ⟨fun _ ↦ le_csSup (OrderTop.bddAbove _), fun _ hsa ↦