case h.e'_2.h.e'_3
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.27241
δ : Type ?u.27244
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.27241
δ : Type ?u.27244
inst✝² : LE α
inst✝¹ : LE β
inst✝ : OrderIsoClass F α β
f : F
a : α
b : β
⊢ EquivLike.inv f b ≤ a ↔ b ≤ ↑f a
convert (@map_le_map_iff _ _ _ _ _ _ f (EquivLike.inv f b) a).symm
no goals
case h.e'_2.h.e'_3
F : Type u_2
α : Type u_1
β : Type u_3
γ : Type ?u.27241
δ : Type ?u.27244
inst✝² : LE α
inst✝¹ : LE β
inst✝ : OrderIsoClass F α β
f : F
a : α
b : β
⊢ b = ↑f (EquivLike.inv f b)
exact (EquivLike.right_inv f _).symm