no goals
α : Type u_1
β : Type ?u.45066
γ : Type ?u.45069
ι : 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'
⊢ (∀ {i : PProd ι ι'}, p i.fst ∧ p' i.snd → Set.Nonempty (s i.fst ∩ s' i.snd)) ↔
    ∀ ⦃i : ι⦄, p i → ∀ ⦃i' : ι'⦄, p' i' → Set.Nonempty (s i ∩ s' i')
simp [@forall_swap _ ι']