no goals
α : Type u_1
β : Type ?u.51338
γ : Type ?u.51341
ι : Sort u_2
ι' : Sort u_3
l l' : Filter α
p : ι → Prop
s : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
hl : HasBasis l p s
hl' : HasBasis l' p' s'
⊢ ¬Disjoint l l' ↔ ¬∃ i, p i ∧ ∃ i', p' i' ∧ Disjoint (s i) (s' i')
simp only [_root_.disjoint_iff, ← Ne.def, ← neBot_iff, inf_eq_inter,
hl.inf_basis_neBot_iff hl', not_exists, not_and, bot_eq_empty, ← nonempty_iff_ne_empty]