chore: use IsLUB IsGLB in CompleteLattice (#35328)

Author: astrainfinita

Mathlib/Algebra/Group/Submonoid/Saturation.lean

@@ -168,8 +168,7 @@ theorem mem_sInf {f : Set (SaturatedSubmonoid M)} {x : M} : x ∈ sInf f ↔ ∀
 variable (M) in
 @[to_additive]
 instance : CompleteSemilatticeInf (SaturatedSubmonoid M) where
-  sInf_le f s hs x hx := mem_sInf.1 hx s hs
-  le_sInf f s ih x hx := mem_sInf.2 <| by tauto
+  isGLB_sInf _ := .of_image SetLike.coe_subset_coe isGLB_biInf
 
 end SaturatedSubmonoid
 

Mathlib/Algebra/Module/Submodule/Lattice.lean

@@ -192,6 +192,9 @@ set_option backward.privateInPublic true in
 private theorem le_sInf' {S : Set (Submodule R M)} {p} : (∀ q ∈ S, p ≤ q) → p ≤ sInf S :=
   Set.subset_iInter₂
 
+protected theorem isGLB_sInf {S : Set (Submodule R M)} : IsGLB S (sInf S) :=
+  .of_image SetLike.coe_subset_coe isGLB_biInf
+
 instance : Min (Submodule R M) :=
   ⟨fun p q ↦
     { carrier := p ∩ q
@@ -213,10 +216,8 @@ instance completeLattice : CompleteLattice (Submodule R M) :=
     inf_le_left := fun _ _ ↦ Set.inter_subset_left
     inf_le_right := fun _ _ ↦ Set.inter_subset_right
     sSup S := sInf {sm | ∀ s ∈ S, s ≤ sm}
-    le_sSup := fun _ _ hs ↦ le_sInf' fun _ hq ↦ by exact hq _ hs
-    sSup_le := fun _ _ hs ↦ sInf_le' hs
-    le_sInf := fun _ _ ↦ le_sInf'
-    sInf_le := fun _ _ ↦ sInf_le' }
+    isLUB_sSup _ := isGLB_upperBounds.mp Submodule.isGLB_sInf
+    isGLB_sInf _ := Submodule.isGLB_sInf }
 
 @[simp]
 theorem coe_inf : ↑(p ⊓ q) = (p ∩ q : Set M) :=

Mathlib/AlgebraicGeometry/IdealSheaf/Basic.lean

@@ -98,8 +98,7 @@ instance : CompleteSemilatticeSup (IdealSheafData X) where
         conv_lhs => rw [← Subtype.range_val (s := s), ← Set.range_comp]
         rfl
       simp only [this, iSup_apply, Ideal.map_iSup, map_ideal_basicOpen, implies_true] }
-  le_sSup s x hxs := le_sSup (s := ideal '' s) ⟨_, hxs, rfl⟩
-  sSup_le s i hi := sSup_le (s := ideal '' s) (Set.forall_mem_image.mpr hi)
+  isLUB_sSup _ := .of_image (f := ideal) le_def (isLUB_sSup _)
 
 /-- The largest ideal sheaf contained in a family of ideals. -/
 def ofIdeals (I : ∀ U : X.affineOpens, Ideal Γ(X, U)) : IdealSheafData X :=

Mathlib/AlgebraicTopology/SimplicialComplex/Basic.lean

@@ -77,6 +77,9 @@ instance : LE (PreAbstractSimplicialComplex ι) where
 instance : LT (PreAbstractSimplicialComplex ι) where
   lt K L := K.faces ⊂ L.faces
 
+instance : IsConcreteLE (PreAbstractSimplicialComplex ι) (Finset ι) where
+  coe_subset_coe' := .rfl
+
 instance : PartialOrder (PreAbstractSimplicialComplex ι) :=
   PartialOrder.lift (fun K => K.faces) (fun _ _ => PreAbstractSimplicialComplex.ext)
 
@@ -102,12 +105,12 @@ instance : Bot (PreAbstractSimplicialComplex ι) where
       isRelLowerSet_faces := isRelLowerSet_empty }
 
 instance : CompleteSemilatticeSup (PreAbstractSimplicialComplex ι) where
-  le_sSup _ _ hK := Set.subset_biUnion_of_mem hK
-  sSup_le _ _ hK := Set.iUnion₂_subset hK
+  isLUB_sSup _ := .of_image SetLike.coe_subset_coe isLUB_biSup
 
 instance : CompleteSemilatticeInf (PreAbstractSimplicialComplex ι) where
-  sInf_le _ _ hK := Set.inter_subset_left.trans (Set.biInter_subset_of_mem hK)
-  le_sInf _ K hK _ ht := ⟨Set.mem_iInter₂.mpr fun L hL => hK L hL ht, (K.isRelLowerSet_faces ht).1⟩
+  isGLB_sInf _ :=
+    ⟨fun _ hK ↦ Set.inter_subset_left.trans (Set.biInter_subset_of_mem hK),
+      fun K hK _ ht ↦ ⟨Set.mem_iInter₂.mpr fun _ hL => hK hL ht, (K.isRelLowerSet_faces ht).1⟩⟩
 
 instance : CompleteLattice (PreAbstractSimplicialComplex ι) where
   inf := min
@@ -198,6 +201,9 @@ instance : LE (AbstractSimplicialComplex ι) where
 instance : LT (AbstractSimplicialComplex ι) where
   lt K L := K.faces ⊂ L.faces
 
+instance : IsConcreteLE (AbstractSimplicialComplex ι) (Finset ι) where
+  coe_subset_coe' := .rfl
+
 instance : PartialOrder (AbstractSimplicialComplex ι) :=
   PartialOrder.lift (fun K => K.faces) (fun _ _ => AbstractSimplicialComplex.ext)
 
@@ -260,20 +266,24 @@ instance : Bot (AbstractSimplicialComplex ι) where
       singleton_mem v := ⟨v, rfl⟩ }
 
 instance : CompleteSemilatticeSup (AbstractSimplicialComplex ι) where
-  le_sSup _ K hK _ ht := Or.inl (Set.mem_biUnion hK ht)
-  sSup_le _ L hL _ ht := by
-    cases ht with
-    | inl ht =>
-      simp only [Set.mem_iUnion] at ht
-      obtain ⟨K, hK, htK⟩ := ht
-      exact hL K hK htK
-    | inr ht =>
-      obtain ⟨v, hv⟩ := ht
-      exact hv ▸ L.singleton_mem v
+  isLUB_sSup _ := by
+    constructor
+    · intro K hK _ ht
+      exact Or.inl (Set.mem_biUnion hK ht)
+    · intro L hL _ ht
+      cases ht with
+      | inl ht =>
+        simp only [Set.mem_iUnion] at ht
+        obtain ⟨K, hK, htK⟩ := ht
+        exact hL hK htK
+      | inr ht =>
+        obtain ⟨v, hv⟩ := ht
+        exact hv ▸ L.singleton_mem v
 
 instance : CompleteSemilatticeInf (AbstractSimplicialComplex ι) where
-  sInf_le _ _ hK := Set.inter_subset_left.trans (Set.biInter_subset_of_mem hK)
-  le_sInf _ K hK _ ht := ⟨Set.mem_iInter₂.mpr fun L hL => hK L hL ht, (K.isRelLowerSet_faces ht).1⟩
+  isGLB_sInf _ :=
+    ⟨fun _ hK ↦ Set.inter_subset_left.trans (Set.biInter_subset_of_mem hK),
+      fun K hK _ ht ↦ ⟨Set.mem_iInter₂.mpr fun _ hL => hK hL ht, (K.isRelLowerSet_faces ht).1⟩⟩
 
 instance : CompleteLattice (AbstractSimplicialComplex ι) where
   inf := min

Mathlib/CategoryTheory/Sites/Sieves.lean

@@ -573,10 +573,8 @@ instance : CompleteLattice (Sieve X) where
   inf := Sieve.inter
   sSup := Sieve.sup
   sInf := Sieve.inf
-  le_sSup _ S hS _ _ hf := ⟨S, hS, hf⟩
-  sSup_le := fun _ _ ha _ _ ⟨b, hb, hf⟩ => (ha b hb) _ hf
-  sInf_le _ _ hS _ _ h := h _ hS
-  le_sInf _ _ hS _ _ hf _ hR := hS _ hR _ hf
+  isLUB_sSup _ := ⟨fun S hS _ _ hf ↦ ⟨S, hS, hf⟩, fun _ ha _ _ ⟨b, hb, hf⟩ ↦ ha hb _ hf⟩
+  isGLB_sInf _ := ⟨fun S hS _ _ h ↦ h _ hS, fun _ hS _ _ hf _ hR ↦ hS hR _ hf⟩
   le_sup_left _ _ _ _ := Or.inl
   le_sup_right _ _ _ _ := Or.inr
   sup_le _ _ _ h₁ h₂ _ f := by

Mathlib/CategoryTheory/Subfunctor/Basic.lean

@@ -75,15 +75,13 @@ instance : CompleteLattice (Subfunctor F) where
         simp only [Set.sSup_eq_sUnion, Set.sUnion_image, Set.preimage_iUnion,
           Set.mem_iUnion, Set.mem_preimage, exists_prop]
         exact ⟨_, h, F.map f h'⟩ }
-  le_sSup _ _ _ _ _ := by aesop
-  sSup_le _ _ _ _ _ := by aesop
+  isLUB_sSup _ := ⟨fun _ _ _ _ ↦ by aesop, fun _ _ _ ↦ by aesop⟩
   sInf S :=
     { obj U := sInf (Set.image (fun T ↦ T.obj U) S)
       map f x hx := by
         rintro _ ⟨F, h, rfl⟩
         exact F.map f (hx _ ⟨_, h, rfl⟩) }
-  sInf_le _ _ _ _ _ := by aesop
-  le_sInf _ _ _ _ _ := by aesop
+  isGLB_sInf _ := ⟨fun _ _ _ _ ↦ by aesop, fun _ _ _ ↦ by aesop⟩
   bot :=
     { obj U := ⊥
       map := by simp }

Mathlib/CategoryTheory/Subobject/Lattice.lean

@@ -626,8 +626,7 @@ theorem le_sInf {A : C} (s : Set (Subobject A)) (f : Subobject A) (k : ∀ g ∈
 
 instance completeSemilatticeInf {B : C} : CompleteSemilatticeInf (Subobject B) where
   sInf := sInf
-  sInf_le := sInf_le
-  le_sInf := le_sInf
+  isGLB_sInf _ := ⟨sInf_le _, le_sInf _⟩
 
 end Inf
 
@@ -679,8 +678,7 @@ theorem sSup_le {A : C} (s : Set (Subobject A)) (f : Subobject A) (k : ∀ g ∈
 
 instance completeSemilatticeSup {B : C} : CompleteSemilatticeSup (Subobject B) where
   sSup := sSup
-  le_sSup := le_sSup
-  sSup_le := sSup_le
+  isLUB_sSup _ := ⟨le_sSup _, sSup_le _⟩
 
 end Sup
 

Mathlib/Combinatorics/Digraph/Basic.lean

@@ -181,12 +181,8 @@ instance completeAtomicBooleanAlgebra : CompleteAtomicBooleanAlgebra (Digraph V)
   bot_le _ _ _ h := h.elim
   inf_compl_le_bot _ _ _ h := absurd h.1 h.2
   top_le_sup_compl G v w _ := by tauto
-  le_sSup _ G hG _ _ hab := ⟨G, hG, hab⟩
-  sSup_le s G hG a b := by
-    rintro ⟨H, hH, hab⟩
-    exact hG _ hH hab
-  sInf_le _ _ hG _ _ hab := hab hG
-  le_sInf _ _ hG _ _ hab _ hH := hG _ hH hab
+  isLUB_sSup _ := ⟨fun G hG _ _ hab ↦ ⟨G, hG, hab⟩, fun _ hG _ _ ⟨_, hH, hab⟩ ↦ hG hH hab⟩
+  isGLB_sInf _ := ⟨fun _ hG _ _ hab ↦ hab hG, fun _ hG _ _ hab _ hH ↦ hG hH hab⟩
   iInf_iSup_eq f := by ext; simp [Classical.skolem]
 
 @[simp] theorem top_adj (v w : V) : (⊤ : Digraph V).Adj v w := trivial

Mathlib/Combinatorics/SimpleGraph/Basic.lean

@@ -321,12 +321,8 @@ instance completeAtomicBooleanAlgebra : CompleteAtomicBooleanAlgebra (SimpleGrap
     by_cases h : G.Adj v w
     · exact Or.inl h
     · exact Or.inr ⟨hvw, h⟩
-  le_sSup _ G hG _ _ hab := ⟨G, hG, hab⟩
-  sSup_le s G hG a b := by
-    rintro ⟨H, hH, hab⟩
-    exact hG _ hH hab
-  sInf_le _ _ hG _ _ hab := hab.1 hG
-  le_sInf _ _ hG _ _ hab := ⟨fun _ hH => hG _ hH hab, hab.ne⟩
+  isLUB_sSup _ := ⟨fun G hG _ _ hab ↦ ⟨G, hG, hab⟩, fun _ hG _ _ ⟨_, hH, hab⟩ ↦ hG hH hab⟩
+  isGLB_sInf _ := ⟨fun _ hG _ _ hab ↦ hab.1 hG, fun _ hG _ _ hab ↦ ⟨fun _ hH => hG hH hab, hab.ne⟩⟩
   iInf_iSup_eq f := by ext; simp [Classical.skolem]
 /-- The complete graph on a type `V` is the simple graph with all pairs of distinct vertices. -/
 abbrev completeGraph (V : Type u) : SimpleGraph V := ⊤

Mathlib/Combinatorics/SimpleGraph/Subgraph.lean

@@ -474,16 +474,15 @@ instance : BoundedOrder (Subgraph G) where
 def completelyDistribLatticeMinimalAxioms : CompletelyDistribLattice.MinimalAxioms G.Subgraph where
   le_top G' := ⟨Set.subset_univ _, fun _ _ => G'.adj_sub⟩
   bot_le _ := ⟨Set.empty_subset _, fun _ _ => False.elim⟩
-  -- Porting note: needed `apply` here to modify elaboration; previously the term itself was fine.
-  le_sSup s G' hG' := ⟨by apply Set.subset_iUnion₂ G' hG', fun _ _ hab => ⟨G', hG', hab⟩⟩
-  sSup_le s G' hG' :=
-    ⟨Set.iUnion₂_subset fun _ hH => (hG' _ hH).1, by
-      rintro a b ⟨H, hH, hab⟩
-      exact (hG' _ hH).2 hab⟩
-  sInf_le _ G' hG' := ⟨Set.iInter₂_subset G' hG', fun _ _ hab => hab.1 hG'⟩
-  le_sInf _ G' hG' :=
-    ⟨Set.subset_iInter₂ fun _ hH => (hG' _ hH).1, fun _ _ hab =>
-      ⟨fun _ hH => (hG' _ hH).2 hab, G'.adj_sub hab⟩⟩
+  isLUB_sSup _ :=
+    ⟨fun G' hG' ↦ ⟨Set.subset_biUnion_of_mem hG', fun _ _ hab => ⟨G', hG', hab⟩⟩,
+      fun G' hG' ↦
+        ⟨Set.iUnion₂_subset fun _ hH => (hG' hH).1, fun a b ⟨H, hH, hab⟩ ↦ (hG' hH).2 hab⟩⟩
+  isGLB_sInf _ :=
+    ⟨fun G' hG' ↦ ⟨Set.iInter₂_subset G' hG', fun _ _ hab => hab.1 hG'⟩,
+      fun G' hG' ↦
+        ⟨Set.subset_iInter₂ fun _ hH => (hG' hH).1, fun _ _ hab =>
+          ⟨fun _ hH => (hG' hH).2 hab, G'.adj_sub hab⟩⟩⟩
   iInf_iSup_eq f := Subgraph.ext (by simpa using iInf_iSup_eq)
     (by ext; simp [Classical.skolem])