no goals
α : Type u_1
β : Type ?u.13300
γ : Type ?u.13303
δ : Type ?u.13306
a b✝ : α
inst✝ : LE α
b : α
⊢ Option.some b ≤ ↑b✝ ↔ ∀ (a : α), Option.some b = ↑a → a ≤ b✝
simp [some_eq_coe, coe_eq_coe]
no goals
α : Type u_1
β : Type ?u.13300
γ : Type ?u.13303
δ : Type ?u.13306
a b : α
inst✝ : LE α
⊢ none ≤ ↑b ↔ ∀ (a : α), none = ↑a → a ≤ b
simp [none_eq_bot]