no goals
α : Type u_1
β : Type u_2
γ : Type ?u.33858
δ : Type ?u.33861
a b : α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ ((StrictMono fun a => map f ↑a) ∧ ∀ (x : α), map f ⊥ < map f ↑x) ↔ StrictMono f
simp [StrictMono, bot_lt_coe]