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