no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
f : α → β
hf : LeftOrdContinuous f
h : Injective f
x y : α
⊢ f x < f y ↔ x < y
simp only [lt_iff_le_not_le, hf.le_iff h]