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