no goals
α : Type u_1
β : Type ?u.11708
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
h : IsCoatomic αᵒᵈ
b : α
⊢ b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b
apply h.eq_top_or_exists_le_coatom
no goals
α : Type u_1
β : Type ?u.11708
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
h : IsAtomic α
b : αᵒᵈ
⊢ b = ⊤ ∨ ∃ a, IsCoatom a ∧ b ≤ a
apply h.eq_bot_or_exists_atom_le