chore(Order): More simp lemmas (#13338)

These lemmas are needed in #13201

Author: YaelDillies

Mathlib/Order/Bounds/Basic.lean

@@ -624,19 +624,19 @@ end
 -/
 
 
-theorem isGreatest_singleton : IsGreatest {a} a :=
+@[simp] theorem isGreatest_singleton : IsGreatest {a} a :=
   ⟨mem_singleton a, fun _ hx => le_of_eq <| eq_of_mem_singleton hx⟩
 #align is_greatest_singleton isGreatest_singleton
 
-theorem isLeast_singleton : IsLeast {a} a :=
+@[simp] theorem isLeast_singleton : IsLeast {a} a :=
   @isGreatest_singleton αᵒᵈ _ a
 #align is_least_singleton isLeast_singleton
 
-theorem isLUB_singleton : IsLUB {a} a :=
+@[simp] theorem isLUB_singleton : IsLUB {a} a :=
   isGreatest_singleton.isLUB
 #align is_lub_singleton isLUB_singleton
 
-theorem isGLB_singleton : IsGLB {a} a :=
+@[simp] theorem isGLB_singleton : IsGLB {a} a :=
   isLeast_singleton.isGLB
 #align is_glb_singleton isGLB_singleton
 

Mathlib/Order/CompleteLattice.lean

@@ -1743,11 +1743,13 @@ instance Pi.instCompleteLattice {α : Type*} {β : α → Type*} [∀ i, Complet
   le_sInf _ _ hf := fun i => le_iInf fun g => hf g g.2 i
 #align pi.complete_lattice Pi.instCompleteLattice
 
+@[simp]
 theorem sSup_apply {α : Type*} {β : α → Type*} [∀ i, SupSet (β i)] {s : Set (∀ a, β a)} {a : α} :
     (sSup s) a = ⨆ f : s, (f : ∀ a, β a) a :=
   rfl
 #align Sup_apply sSup_apply
 
+@[simp]
 theorem sInf_apply {α : Type*} {β : α → Type*} [∀ i, InfSet (β i)] {s : Set (∀ a, β a)} {a : α} :
     sInf s a = ⨅ f : s, (f : ∀ a, β a) a :=
   rfl
@@ -1792,15 +1794,33 @@ theorem binary_relation_sInf_iff {α β : Type*} (s : Set (α → β → Prop))
 
 section CompleteLattice
 
-variable [Preorder α] [CompleteLattice β]
+variable {ι : Sort*} [Preorder α] [CompleteLattice β] {s : Set (α → β)} {f : ι → α → β}
+
+protected lemma Monotone.sSup (hs : ∀ f ∈ s, Monotone f) : Monotone (sSup s) :=
+  fun _ _ h ↦ iSup_mono fun f ↦ hs f f.2 h
+#align monotone_Sup_of_monotone Monotone.sSup
+
+protected lemma Monotone.sInf (hs : ∀ f ∈ s, Monotone f) : Monotone (sInf s) :=
+  fun _ _ h ↦ iInf_mono fun f ↦ hs f f.2 h
+#align monotone_Inf_of_monotone Monotone.sInf
+
+protected lemma Antitone.sSup (hs : ∀ f ∈ s, Antitone f) : Antitone (sSup s) :=
+  fun _ _ h ↦ iSup_mono fun f ↦ hs f f.2 h
+
+protected lemma Antitone.sInf (hs : ∀ f ∈ s, Antitone f) : Antitone (sInf s) :=
+  fun _ _ h ↦ iInf_mono fun f ↦ hs f f.2 h
 
-theorem monotone_sSup_of_monotone {s : Set (α → β)} (m_s : ∀ f ∈ s, Monotone f) :
-    Monotone (sSup s) := fun _ _ h => iSup_mono fun f => m_s f f.2 h
-#align monotone_Sup_of_monotone monotone_sSup_of_monotone
+@[deprecated (since := "2024-05-29")] alias monotone_sSup_of_monotone := Monotone.sSup
+@[deprecated (since := "2024-05-29")] alias monotone_sInf_of_monotone := Monotone.sInf
 
-theorem monotone_sInf_of_monotone {s : Set (α → β)} (m_s : ∀ f ∈ s, Monotone f) :
-    Monotone (sInf s) := fun _ _ h => iInf_mono fun f => m_s f f.2 h
-#align monotone_Inf_of_monotone monotone_sInf_of_monotone
+protected lemma Monotone.iSup (hf : ∀ i, Monotone (f i)) : Monotone (⨆ i, f i) :=
+  Monotone.sSup (by simpa)
+protected lemma Monotone.iInf (hf : ∀ i, Monotone (f i)) : Monotone (⨅ i, f i) :=
+  Monotone.sInf (by simpa)
+protected lemma Antitone.iSup (hf : ∀ i, Antitone (f i)) : Antitone (⨆ i, f i) :=
+  Antitone.sSup (by simpa)
+protected lemma Antitone.iInf (hf : ∀ i, Antitone (f i)) : Antitone (⨅ i, f i) :=
+  Antitone.sInf (by simpa)
 
 end CompleteLattice
 

Mathlib/Order/Hom/Basic.lean

@@ -344,6 +344,9 @@ theorem comp_mono ⦃g₁ g₂ : β →o γ⦄ (hg : g₁ ≤ g₂) ⦃f₁ f₂
     g₁.comp f₁ ≤ g₂.comp f₂ := fun _ => (hg _).trans (g₂.mono <| hf _)
 #align order_hom.comp_mono OrderHom.comp_mono
 
+@[simp] lemma mk_comp_mk (g : β → γ) (f : α → β) (hg hf) :
+    comp ⟨g, hg⟩ ⟨f, hf⟩ = ⟨g ∘ f, hg.comp hf⟩ := rfl
+
 /-- The composition of two bundled monotone functions, a fully bundled version. -/
 @[simps! (config := .asFn)]
 def compₘ : (β →o γ) →o (α →o β) →o α →o γ :=