no goals
α : Type u_1
β : Type ?u.18281
γ : Type ?u.18284
δ : Type ?u.18287
a✝ b✝ : α
inst✝ : LT α
a : WithBot α
b : α
⊢ a < Option.some b ↔ ∃ p, Option.some b = ↑p ∧ a < ↑p
simp [some_eq_coe, coe_eq_coe]
no goals
α : Type u_1
β : Type ?u.18281
γ : Type ?u.18284
δ : Type ?u.18287
a✝ b : α
inst✝ : LT α
a : WithBot α
⊢ ¬∃ p, none = ↑p ∧ a < ↑p
simp [none_eq_bot]