chore(Order/Hom/Bounded): add LE instances (#12983)

urkud · urkud · commit 91e688bd4a6e · 2024-05-19T20:14:00.000Z
diff --git a/Mathlib/Order/Hom/Bounded.lean b/Mathlib/Order/Hom/Bounded.lean
@@ -307,6 +307,9 @@ theorem cancel_left {g : TopHom β γ} {f₁ f₂ : TopHom α β} (hg : Injectiv
 
 end Top
 
+instance instLE [LE β] [Top β] : LE (TopHom α β) where
+  le f g := (f : α → β) ≤ g
+
 instance [Preorder β] [Top β] : Preorder (TopHom α β) :=
   Preorder.lift (DFunLike.coe : TopHom α β → α → β)
 
@@ -315,7 +318,7 @@ instance [PartialOrder β] [Top β] : PartialOrder (TopHom α β) :=
 
 section OrderTop
 
-variable [Preorder β] [OrderTop β]
+variable [LE β] [OrderTop β]
 
 instance : OrderTop (TopHom α β) where
   top := ⟨⊤, rfl⟩
@@ -500,6 +503,9 @@ theorem cancel_left {g : BotHom β γ} {f₁ f₂ : BotHom α β} (hg : Injectiv
 
 end Bot
 
+instance instLE [LE β] [Bot β] : LE (BotHom α β) where
+  le f g := (f : α → β) ≤ g
+
 instance [Preorder β] [Bot β] : Preorder (BotHom α β) :=
   Preorder.lift (DFunLike.coe : BotHom α β → α → β)
 
@@ -508,7 +514,7 @@ instance [PartialOrder β] [Bot β] : PartialOrder (BotHom α β) :=
 
 section OrderBot
 
-variable [Preorder β] [OrderBot β]
+variable [LE β] [OrderBot β]
 
 instance : OrderBot (BotHom α β) where
   bot := ⟨⊥, rfl⟩
