no goals
ι : Type ?u.27670
α : Type u
β : Type v
γ : Type w
δ : Type ?u.27679
π : ι → Type ?u.27684
r : α → α → Prop
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s : Set α
hf : StrictMonoOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ f a < f b ↔ a < b
rw [lt_iff_le_not_le, lt_iff_le_not_le, hf.le_iff_le ha hb, hf.le_iff_le hb ha]