α : Type u
β : Type v
γ : Type ?u.24778
δ : Type ?u.24781
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : OrderBot β
f : α → β
H : StrictMono f
a : α
h_bot : f a = ⊥
x : α
p : β
⊢ ⊥ ≤ p
α : Type u
β : Type v
γ : Type ?u.24778
δ : Type ?u.24781
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : OrderBot β
f : α → β
H : StrictMono f
a : α
h_bot : f a = ⊥
x : α
p : β
⊢ f a ≤ p
rw [h_bot]
no goals
α : Type u
β : Type v
γ : Type ?u.24778
δ : Type ?u.24781
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : OrderBot β
f : α → β
H : StrictMono f
a : α
h_bot : f a = ⊥
x : α
p : β
⊢ ⊥ ≤ p
exact bot_le