no goals
α : Type u_1
β : Type ?u.57921
γ : Type ?u.57924
ι : Sort ?u.57927
ι' : Sort ?u.57930
l l' : Filter α
p : ι → Prop
s : ι → Set α
t : Set α
i : ι
p' : ι' → Prop
s' : ι' → Set α
i' : ι'
l₁ l₂ : Filter α
⊢ diagonal αᶜ ∈ l₁ ×ˢ l₂ ↔ Disjoint l₁ l₂
simp only [mem_prod_iff, Filter.disjoint_iff, prod_subset_compl_diagonal_iff_disjoint]