no goals
α : Type u_1
β : Type ?u.57475
γ : Type ?u.57478
ι : Sort ?u.57481
ι' : Sort ?u.57484
l l' : Filter α
p : ι → Prop
s : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
x y : α
⊢ Disjoint (pure x) (pure y) ↔ x ≠ y
simp only [← principal_singleton, disjoint_principal_principal, disjoint_singleton]