no goals
ι : Sort ?u.12737
α : Type u_1
β : Type ?u.12743
X : Type ?u.12746
Y : Type ?u.12749
l₁ l₂ : Filter α
⊢ 𝓝 (l₁ ⊓ l₂) = 𝓝 l₁ ⊓ 𝓝 l₂
simpa only [iInf_bool_eq] using nhds_iInf fun b => cond b l₁ l₂