case h.e'_2.h.e'_4
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.29401
δ : Type ?u.29404
inst✝² : LE α
inst✝¹ : LE β
inst✝ : OrderIsoClass F α β
f : F
a : α
b : β
⊢ b = ↑f (EquivLike.inv f b)
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.29401
δ : Type ?u.29404
inst✝² : LE α
inst✝¹ : LE β
inst✝ : OrderIsoClass F α β
f : F
a : α
b : β
⊢ a ≤ EquivLike.inv f b ↔ ↑f a ≤ b
convert (@map_le_map_iff _ _ _ _ _ _ f a (EquivLike.inv f b)).symm
no goals
case h.e'_2.h.e'_4
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.29401
δ : Type ?u.29404
inst✝² : LE α
inst✝¹ : LE β
inst✝ : OrderIsoClass F α β
f : F
a : α
b : β
⊢ b = ↑f (EquivLike.inv f b)
exact (EquivLike.right_inv _ _).symm