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