no goals
α : Type u_1
β : Type ?u.58649
γ : Type ?u.58652
ι : Sort u_2
ι' : Sort ?u.58658
l l' : Filter α
p : ι → Prop
s : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
h : HasBasis l p s
⊢ Disjoint l l' ↔ ∃ i, p i ∧ s iᶜ ∈ l'
simp only [h.disjoint_iff l'.basis_sets, id, ← disjoint_principal_left,
  (hasBasis_principal _).disjoint_iff l'.basis_sets, true_and, Unique.exists_iff]