no goals
α : Type u_1
β : Type ?u.11671
γ : Type ?u.11674
δ : Type ?u.11677
a b : α
inst✝ : LE α
x : α
⊢ ↑a ≤ Option.some x ↔ ∃ b, Option.some x = ↑b ∧ a ≤ b
simp [some_eq_coe]
no goals
α : Type u_1
β : Type ?u.11671
γ : Type ?u.11674
δ : Type ?u.11677
a b : α
inst✝ : LE α
⊢ ¬∃ b, none = ↑b ∧ a ≤ b
simp [none_eq_bot]