no goals
α : Type u_1
β : Type ?u.39753
γ : Type ?u.39756
δ : Type ?u.39759
a✝ b✝ : α
inst✝¹ : LE α
inst✝ : OrderBot α
a : WithBot α
b : α
⊢ unbot' ⊥ a ≤ b ↔ a ≤ ↑b
cases a <;> simp [none_eq_bot, some_eq_coe]