case intro.intro
α : Type u_1
β : Type ?u.19501
inst✝¹ : CompleteLattice α
inst✝ : IsAtomistic α
s : Set α
hs : ∀ (a : α), a ∈ s → IsAtom a
⊢ sSup {a | IsAtom a ∧ a ≤ sSup s} = sSup s
α : Type u_1
β : Type ?u.19501
inst✝¹ : CompleteLattice α
inst✝ : IsAtomistic α
b : α
⊢ sSup {a | IsAtom a ∧ a ≤ b} = b
rcases eq_sSup_atoms b with ⟨s, rfl, hs⟩
no goals
case intro.intro
α : Type u_1
β : Type ?u.19501
inst✝¹ : CompleteLattice α
inst✝ : IsAtomistic α
s : Set α
hs : ∀ (a : α), a ∈ s → IsAtom a
⊢ sSup {a | IsAtom a ∧ a ≤ sSup s} = sSup s
exact le_antisymm (sSup_le fun _ => And.right) (sSup_le_sSup fun a ha => ⟨hs a ha, le_sSup ha⟩)