α : Type u_1
β : Type ?u.81171
s : Set α
⊢ IsAtom s → ∃ x, s = {x}
α : Type u_1
β : Type ?u.81171
s : Set α
⊢ IsAtom s ↔ ∃ x, s = {x}
refine'
  ⟨_, by
    rintro ⟨x, rfl⟩
    exact isAtom_singleton x⟩
α : Type u_1
β : Type ?u.81171
s : Set α
⊢ (Set.Nonempty s ∧ ∀ (b : Set α), b ≠ ∅ → b ≤ s → s ≤ b) → ∃ x, s = {x}
α : Type u_1
β : Type ?u.81171
s : Set α
⊢ IsAtom s → ∃ x, s = {x}
rw [_root_.isAtom_iff, bot_eq_empty, ← nonempty_iff_ne_empty]
case intro.intro
α : Type u_1
β : Type ?u.81171
s : Set α
hs : ∀ (b : Set α), b ≠ ∅ → b ≤ s → s ≤ b
x : α
hx : x ∈ s
⊢ ∃ x, s = {x}
α : Type u_1
β : Type ?u.81171
s : Set α
⊢ (Set.Nonempty s ∧ ∀ (b : Set α), b ≠ ∅ → b ≤ s → s ≤ b) → ∃ x, s = {x}
rintro ⟨⟨x, hx⟩, hs⟩
no goals
case intro.intro
α : Type u_1
β : Type ?u.81171
s : Set α
hs : ∀ (b : Set α), b ≠ ∅ → b ≤ s → s ≤ b
x : α
hx : x ∈ s
⊢ ∃ x, s = {x}
exact
  ⟨x, eq_singleton_iff_unique_mem.2
      ⟨hx, fun y hy => (hs {y} (singleton_ne_empty _) (singleton_subset_iff.2 hy) hx).symm⟩⟩
case intro
α : Type u_1
β : Type ?u.81171
x : α
⊢ IsAtom {x}
α : Type u_1
β : Type ?u.81171
s : Set α
⊢ (∃ x, s = {x}) → IsAtom s
rintro ⟨x, rfl⟩
no goals
case intro
α : Type u_1
β : Type ?u.81171
x : α
⊢ IsAtom {x}
exact isAtom_singleton x