F : Type u_3
α : Type u_1
β : Type u_2
γ : Type ?u.7624
δ : Type ?u.7627
inst✝⁴ : LE α
inst✝³ : OrderBot α
inst✝² : PartialOrder β
inst✝¹ : OrderBot β
inst✝ : OrderIsoClass F α β
f : F
a : α
this : BotHomClass F α β := OrderIsoClass.toBotHomClass
⊢ ↑f a = ⊥ ↔ a = ⊥
F : Type u_3
α : Type u_1
β : Type u_2
γ : Type ?u.7624
δ : Type ?u.7627
inst✝⁴ : LE α
inst✝³ : OrderBot α
inst✝² : PartialOrder β
inst✝¹ : OrderBot β
inst✝ : OrderIsoClass F α β
f : F
a : α
⊢ ↑f a = ⊥ ↔ a = ⊥
letI : BotHomClass F α β := OrderIsoClass.toBotHomClass
no goals
F : Type u_3
α : Type u_1
β : Type u_2
γ : Type ?u.7624
δ : Type ?u.7627
inst✝⁴ : LE α
inst✝³ : OrderBot α
inst✝² : PartialOrder β
inst✝¹ : OrderBot β
inst✝ : OrderIsoClass F α β
f : F
a : α
this : BotHomClass F α β := OrderIsoClass.toBotHomClass
⊢ ↑f a = ⊥ ↔ a = ⊥
rw [← map_bot f, (EquivLike.injective f).eq_iff]