F : Type u_3
α : Type u_1
β : Type u_2
γ : Type ?u.6610
δ : Type ?u.6613
inst✝⁴ : LE α
inst✝³ : OrderTop α
inst✝² : PartialOrder β
inst✝¹ : OrderTop β
inst✝ : OrderIsoClass F α β
f : F
a : α
this : TopHomClass F α β := OrderIsoClass.toTopHomClass
⊢ ↑f a = ⊤ ↔ a = ⊤
F : Type u_3
α : Type u_1
β : Type u_2
γ : Type ?u.6610
δ : Type ?u.6613
inst✝⁴ : LE α
inst✝³ : OrderTop α
inst✝² : PartialOrder β
inst✝¹ : OrderTop β
inst✝ : OrderIsoClass F α β
f : F
a : α
⊢ ↑f a = ⊤ ↔ a = ⊤
letI : TopHomClass F α β := OrderIsoClass.toTopHomClass
no goals
F : Type u_3
α : Type u_1
β : Type u_2
γ : Type ?u.6610
δ : Type ?u.6613
inst✝⁴ : LE α
inst✝³ : OrderTop α
inst✝² : PartialOrder β
inst✝¹ : OrderTop β
inst✝ : OrderIsoClass F α β
f : F
a : α
this : TopHomClass F α β := OrderIsoClass.toTopHomClass
⊢ ↑f a = ⊤ ↔ a = ⊤
rw [← map_top f, (EquivLike.injective f).eq_iff]