no goals
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
x : α
C : Set α
⊢ AccPt x (𝓟 C) ↔ ∀ (U : Set α), U ∈ 𝓝 x → ∃ y, y ∈ U ∩ C ∧ y ≠ x
simp [acc_principal_iff_cluster, clusterPt_principal_iff, Set.Nonempty, exists_prop, and_assoc,
  @and_comm (¬_ = x)]