no goals
α : Type u_1
β : Type ?u.19934
γ : Type ?u.19937
δ : Type ?u.19940
a b✝ : α
inst✝ : LT α
b : α
⊢ Option.some b < ↑b✝ ↔ ∀ (a : WithBot α), Option.some b = a → a < ↑b✝
simp [some_eq_coe, coe_eq_coe, coe_lt_coe]
no goals
α : Type u_1
β : Type ?u.19934
γ : Type ?u.19937
δ : Type ?u.19940
a b : α
inst✝ : LT α
⊢ none < ↑b ↔ ∀ (a : WithBot α), none = a → a < ↑b
simp [none_eq_bot, bot_lt_coe]