no goals
α : Type u_1
β : Type ?u.72707
γ : Type ?u.72710
δ : Type ?u.72713
a b : α
inst✝ : LE α
⊢ ↑a ≤ ↑b ↔ a ≤ b
simp only [← toDual_le_toDual_iff, toDual_apply_coe, WithBot.coe_le_coe, toDual_le_toDual]