no goals
α : Type u
β : Type v
ι : Sort w
a✝ : α
s✝ s₁ s₂ t✝ : Set α
p✝ p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
a : α
p : ι → Prop
s : ι → Set α
h : HasBasis (𝓝 a) p s
t : Set α
⊢ (∀ ⦃i : ι⦄, p i → ∀ ⦃j : Unit⦄, True → Set.Nonempty (s i ∩ t)) ↔ ∀ (i : ι), p i → Set.Nonempty (s i ∩ t)
simp only [exists_prop, forall_const]