F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.32870
δ : Type ?u.32873
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : OrderIsoClass F α β
f : F
a : α
b : β
⊢ ↑f a < ↑f (EquivLike.inv f b) ↔ ↑f a < b
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.32870
δ : Type ?u.32873
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : OrderIsoClass F α β
f : F
a : α
b : β
⊢ a < EquivLike.inv f b ↔ ↑f a < b
rw [← map_lt_map_iff f]
no goals
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.32870
δ : Type ?u.32873
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : OrderIsoClass F α β
f : F
a : α
b : β
⊢ ↑f a < ↑f (EquivLike.inv f b) ↔ ↑f a < b
simp only [EquivLike.apply_inv_apply]