[Merged by Bors] - chore(*): use notation for filter.prod

src/analysis/calculus/fderiv.lean

@@ -1088,17 +1088,17 @@ variables {f₂ : E → G} {f₂' : E →L[𝕜] G}
 
 protected lemma has_strict_fderiv_at.prod
   (hf₁ : has_strict_fderiv_at f₁ f₁' x) (hf₂ : has_strict_fderiv_at f₂ f₂' x) :
-  has_strict_fderiv_at (λx, (f₁ x, f₂ x)) (continuous_linear_map.prod f₁' f₂') x :=
+  has_strict_fderiv_at (λx, (f₁ x, f₂ x)) (f₁'.prod f₂') x :=
 hf₁.prod_left hf₂
 
 lemma has_fderiv_at_filter.prod
   (hf₁ : has_fderiv_at_filter f₁ f₁' x L) (hf₂ : has_fderiv_at_filter f₂ f₂' x L) :
-  has_fderiv_at_filter (λx, (f₁ x, f₂ x)) (continuous_linear_map.prod f₁' f₂') x L :=
+  has_fderiv_at_filter (λx, (f₁ x, f₂ x)) (f₁'.prod f₂') x L :=
 hf₁.prod_left hf₂
 
 lemma has_fderiv_within_at.prod
   (hf₁ : has_fderiv_within_at f₁ f₁' s x) (hf₂ : has_fderiv_within_at f₂ f₂' s x) :
-  has_fderiv_within_at (λx, (f₁ x, f₂ x)) (continuous_linear_map.prod f₁' f₂') s x :=
+  has_fderiv_within_at (λx, (f₁ x, f₂ x)) (f₁'.prod f₂') s x :=
 hf₁.prod hf₂
 
 lemma has_fderiv_at.prod (hf₁ : has_fderiv_at f₁ f₁' x) (hf₂ : has_fderiv_at f₂ f₂' x) :
@@ -1126,15 +1126,14 @@ lemma differentiable.prod (hf₁ : differentiable 𝕜 f₁) (hf₂ : differenti
 
 lemma differentiable_at.fderiv_prod
   (hf₁ : differentiable_at 𝕜 f₁ x) (hf₂ : differentiable_at 𝕜 f₂ x) :
-  fderiv 𝕜 (λx:E, (f₁ x, f₂ x)) x =
-    continuous_linear_map.prod (fderiv 𝕜 f₁ x) (fderiv 𝕜 f₂ x) :=
-has_fderiv_at.fderiv (has_fderiv_at.prod hf₁.has_fderiv_at hf₂.has_fderiv_at)
+  fderiv 𝕜 (λx:E, (f₁ x, f₂ x)) x = (fderiv 𝕜 f₁ x).prod (fderiv 𝕜 f₂ x) :=
+(hf₁.has_fderiv_at.prod hf₂.has_fderiv_at).fderiv
 
 lemma differentiable_at.fderiv_within_prod
   (hf₁ : differentiable_within_at 𝕜 f₁ s x) (hf₂ : differentiable_within_at 𝕜 f₂ s x)
   (hxs : unique_diff_within_at 𝕜 s x) :
   fderiv_within 𝕜 (λx:E, (f₁ x, f₂ x)) s x =
-    continuous_linear_map.prod (fderiv_within 𝕜 f₁ s x) (fderiv_within 𝕜 f₂ s x) :=
+    (fderiv_within 𝕜 f₁ s x).prod (fderiv_within 𝕜 f₂ s x) :=
 begin
   apply has_fderiv_within_at.fderiv_within _ hxs,
   exact has_fderiv_within_at.prod hf₁.has_fderiv_within_at hf₂.has_fderiv_within_at

src/order/filter/bases.lean

@@ -38,7 +38,7 @@ and consequences are derived.
 * `basis_sets` : all sets of a filter form a basis;
 * `has_basis.inf`, `has_basis.inf_principal`, `has_basis.prod`, `has_basis.prod_self`,
   `has_basis.map`, `has_basis.comap` : combinators to construct filters of `l ⊓ l'`,
-  `l ⊓ 𝓟 t`, `l.prod l'`, `l.prod l`, `l.map f`, `l.comap f` respectively;
+  `l ⊓ 𝓟 t`, `l ×ᶠ l'`, `l ×ᶠ l`, `l.map f`, `l.comap f` respectively;
 * `has_basis.le_iff`, `has_basis.ge_iff`, has_basis.le_basis_iff` : restate `l ≤ l'` in terms
   of bases.
 * `has_basis.tendsto_right_iff`, `has_basis.tendsto_left_iff`, `has_basis.tendsto_iff` : restate
@@ -416,7 +416,7 @@ lemma comap_has_basis (f : α → β) (l : filter β) :
 ⟨λ t, mem_comap_sets⟩
 
 lemma has_basis.prod_self (hl : l.has_basis p s) :
-  (l.prod l).has_basis p (λ i, (s i).prod (s i)) :=
+  (l ×ᶠ l).has_basis p (λ i, (s i).prod (s i)) :=
 ⟨begin
   intro t,
   apply mem_prod_iff.trans,
@@ -428,6 +428,9 @@ lemma has_basis.prod_self (hl : l.has_basis p s) :
     exact ⟨s i, hl.mem_of_mem hi, s i, hl.mem_of_mem hi, H⟩ }
 end⟩
 
+lemma mem_prod_self_iff {s} : s ∈ l ×ᶠ l ↔ ∃ t ∈ l, set.prod t t ⊆ s :=
+l.basis_sets.prod_self.mem_iff
+
 lemma has_basis.exists_iff (hl : l.has_basis p s) {P : set α → Prop}
   (mono : ∀ ⦃s t⦄, s ⊆ t → P t → P s) :
   (∃ s ∈ l, P s) ↔ ∃ (i) (hi : p i), P (s i) :=
@@ -503,14 +506,14 @@ lemma tendsto.basis_both (H : tendsto f la lb) (hla : la.has_basis pa sa)
 (hla.tendsto_iff hlb).1 H
 
 lemma has_basis.prod (hla : la.has_basis pa sa) (hlb : lb.has_basis pb sb) :
-  (la.prod lb).has_basis (λ i : ι × ι', pa i.1 ∧ pb i.2) (λ i, (sa i.1).prod (sb i.2)) :=
+  (la ×ᶠ lb).has_basis (λ i : ι × ι', pa i.1 ∧ pb i.2) (λ i, (sa i.1).prod (sb i.2)) :=
 (hla.comap prod.fst).inf (hlb.comap prod.snd)
 
 lemma has_basis.prod' {la : filter α} {lb : filter β} {ι : Type*} {p : ι → Prop}
   {sa : ι → set α} {sb : ι → set β}
   (hla : la.has_basis p sa) (hlb : lb.has_basis p sb)
   (h_dir : ∀ {i j}, p i → p j → ∃ k, p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j) :
-  (la.prod lb).has_basis p (λ i, (sa i).prod (sb i)) :=
+  (la ×ᶠ lb).has_basis p (λ i, (sa i).prod (sb i)) :=
 ⟨begin
   intros t,
   rw mem_prod_iff,

src/order/filter/basic.lean

@@ -2228,7 +2228,7 @@ lemma eventually.prod_mk {la : filter α} {pa : α → Prop} (ha : ∀ᶠ x in l
 (ha.prod_inl lb).and (hb.prod_inr la)
 
 lemma eventually.curry {la : filter α} {lb : filter β} {p : α × β → Prop}
-  (h : ∀ᶠ x in la.prod lb, p x) :
+  (h : ∀ᶠ x in la ×ᶠ lb, p x) :
   ∀ᶠ x in la, ∀ᶠ y in lb, p (x, y) :=
 begin
   rcases eventually_prod_iff.1 h with ⟨pa, ha, pb, hb, h⟩,
@@ -2280,7 +2280,7 @@ begin
 end
 
 lemma map_prod (m : α × β → γ) (f : filter α) (g : filter β) :
-  map m (f.prod g) = (f.map (λa b, m (a, b))).seq g :=
+  map m (f ×ᶠ g) = (f.map (λa b, m (a, b))).seq g :=
 begin
   simp [filter.ext_iff, mem_prod_iff, mem_map_seq_iff],
   assume s,
@@ -2289,7 +2289,7 @@ begin
   exact assume ⟨s, hs, t, ht, h⟩, ⟨t, ht, s, hs, assume ⟨x, y⟩ ⟨hx, hy⟩, h x hx y hy⟩
 end
 
-lemma prod_eq {f : filter α} {g : filter β} : f.prod g = (f.map prod.mk).seq g  :=
+lemma prod_eq {f : filter α} {g : filter β} : f ×ᶠ g = (f.map prod.mk).seq g  :=
 have h : _ := map_prod id f g, by rwa [map_id] at h
 
 lemma prod_inf_prod {f₁ f₂ : filter α} {g₁ g₂ : filter β} :

src/order/filter/lift.lean

@@ -378,7 +378,7 @@ end lift'
 section prod
 variables {f : filter α}
 
-lemma prod_def {f : filter α} {g : filter β} : f.prod g = (f.lift $ λs, g.lift' $ set.prod s) :=
+lemma prod_def {f : filter α} {g : filter β} : f ×ᶠ g = (f.lift $ λs, g.lift' $ set.prod s) :=
 have ∀(s:set α) (t : set β),
     𝓟 (set.prod s t) = (𝓟 s).comap prod.fst ⊓ (𝓟 t).comap prod.snd,
   by simp only [principal_eq_iff_eq, comap_principal, inf_principal]; intros; refl,
@@ -388,18 +388,18 @@ begin
   simp only [filter.prod, lift_principal2, eq_self_iff_true]
 end
 
-lemma prod_same_eq : filter.prod f f = f.lift' (λt, set.prod t t) :=
+lemma prod_same_eq : f ×ᶠ f = f.lift' (λt, set.prod t t) :=
 by rw [prod_def];
 from lift_lift'_same_eq_lift'
   (assume s, set.monotone_prod monotone_const monotone_id)
   (assume t, set.monotone_prod monotone_id monotone_const)
 
 lemma mem_prod_same_iff {s : set (α×α)} :
-  s ∈ filter.prod f f ↔ (∃t∈f, set.prod t t ⊆ s) :=
+  s ∈ f ×ᶠ f ↔ (∃t∈f, set.prod t t ⊆ s) :=
 by rw [prod_same_eq, mem_lift'_sets]; exact set.monotone_prod monotone_id monotone_id
 
 lemma tendsto_prod_self_iff {f : α × α → β} {x : filter α} {y : filter β} :
-  filter.tendsto f (filter.prod x x) y ↔
+  filter.tendsto f (x ×ᶠ x) y ↔
   ∀ W ∈ y, ∃ U ∈ x, ∀ (x x' : α), x ∈ U → x' ∈ U → f (x, x') ∈ W :=
 by simp only [tendsto_def, mem_prod_same_iff, prod_sub_preimage_iff, exists_prop, iff_self]
 
@@ -408,7 +408,7 @@ variables {α₁ : Type*} {α₂ : Type*} {β₁ : Type*} {β₂ : Type*}
 lemma prod_lift_lift
   {f₁ : filter α₁} {f₂ : filter α₂} {g₁ : set α₁ → filter β₁} {g₂ : set α₂ → filter β₂}
   (hg₁ : monotone g₁) (hg₂ : monotone g₂) :
-  filter.prod (f₁.lift g₁) (f₂.lift g₂) = f₁.lift (λs, f₂.lift (λt, filter.prod (g₁ s) (g₂ t))) :=
+  (f₁.lift g₁) ×ᶠ (f₂.lift g₂) = f₁.lift (λs, f₂.lift (λt, g₁ s ×ᶠ g₂ t)) :=
 begin
   simp only [prod_def],
   rw [lift_assoc],
@@ -423,7 +423,7 @@ end
 lemma prod_lift'_lift'
   {f₁ : filter α₁} {f₂ : filter α₂} {g₁ : set α₁ → set β₁} {g₂ : set α₂ → set β₂}
   (hg₁ : monotone g₁) (hg₂ : monotone g₂) :
-  filter.prod (f₁.lift' g₁) (f₂.lift' g₂) = f₁.lift (λs, f₂.lift' (λt, set.prod (g₁ s) (g₂ t))) :=
+  f₁.lift' g₁ ×ᶠ f₂.lift' g₂ = f₁.lift (λs, f₂.lift' (λt, (g₁ s).prod (g₂ t))) :=
 begin
   rw [prod_def, lift_lift'_assoc],
   apply congr_arg, funext x,

src/topology/algebra/group.lean

@@ -12,7 +12,7 @@ import topology.algebra.monoid
 import topology.homeomorph
 
 open classical set filter topological_space
-open_locale classical topological_space
+open_locale classical topological_space filter
 
 universes u v w
 variables {α : Type u} {β : Type v} {γ : Type w}
@@ -139,14 +139,14 @@ end
 
 @[to_additive exists_nhds_half_neg]
 lemma exists_nhds_split_inv [topological_group α] {s : set α} (hs : s ∈ 𝓝 (1 : α)) :
-  ∃ V ∈ 𝓝 (1 : α), ∀ v w ∈ V, v * w⁻¹ ∈ s :=
+  ∃ V ∈ 𝓝 (1 : α), ∀ (v ∈ V) (w ∈ V), v * w⁻¹ ∈ s :=
 begin
-  have : tendsto (λa:α×α, a.1 * (a.2)⁻¹) ((𝓝 (1:α)).prod (𝓝 (1:α))) (𝓝 1),
+  have : tendsto (λa:α×α, a.1 * (a.2)⁻¹) (𝓝 (1:α) ×ᶠ 𝓝 (1:α)) (𝓝 1),
   { simpa using (@tendsto_fst α α (𝓝 1) (𝓝 1)).mul tendsto_snd.inv },
-  have : ((λa:α×α, a.1 * (a.2)⁻¹) ⁻¹' s) ∈ (𝓝 (1:α)).prod (𝓝 (1:α)) :=
+  have : ((λa:α×α, a.1 * (a.2)⁻¹) ⁻¹' s) ∈ 𝓝 (1:α) ×ᶠ 𝓝 (1:α) :=
     this (by simpa using hs),
-  rcases mem_prod_iff.1 this with ⟨V₁, H₁, V₂, H₂, H⟩,
-  exact ⟨V₁ ∩ V₂, inter_mem_sets H₁ H₂, assume v w ⟨hv, _⟩ ⟨_, hw⟩, @H (v, w) ⟨hv, hw⟩⟩
+  rcases mem_prod_self_iff.1 this with ⟨V, H, H'⟩,
+  exact ⟨V, H, prod_subset_iff.1 H'⟩
 end
 
 @[to_additive exists_nhds_quarter]
@@ -283,7 +283,7 @@ non-commutative groups too.
 class add_group_with_zero_nhd (α : Type u) extends add_comm_group α :=
 (Z [] : filter α)
 (zero_Z : pure 0 ≤ Z)
-(sub_Z : tendsto (λp:α×α, p.1 - p.2) (Z.prod Z) Z)
+(sub_Z : tendsto (λp:α×α, p.1 - p.2) (Z ×ᶠ Z) Z)
 end prio
 
 namespace add_group_with_zero_nhd
@@ -304,16 +304,16 @@ have tendsto (λa:α, 0 - a) (Z α) (Z α), from
   sub_Z.comp (tendsto.prod_mk this tendsto_id),
 by simpa
 
-lemma add_Z : tendsto (λp:α×α, p.1 + p.2) ((Z α).prod (Z α)) (Z α) :=
-suffices tendsto (λp:α×α, p.1 - -p.2) ((Z α).prod (Z α)) (Z α),
+lemma add_Z : tendsto (λp:α×α, p.1 + p.2) (Z α ×ᶠ Z α) (Z α) :=
+suffices tendsto (λp:α×α, p.1 - -p.2) (Z α ×ᶠ Z α) (Z α),
   by simpa [sub_eq_add_neg],
 sub_Z.comp (tendsto.prod_mk tendsto_fst (neg_Z.comp tendsto_snd))
 
-lemma exists_Z_half {s : set α} (hs : s ∈ Z α) : ∃ V ∈ Z α, ∀ v w ∈ V, v + w ∈ s :=
+lemma exists_Z_half {s : set α} (hs : s ∈ Z α) : ∃ V ∈ Z α, ∀ (v ∈ V) (w ∈ V), v + w ∈ s :=
 begin
-  have : ((λa:α×α, a.1 + a.2) ⁻¹' s) ∈ (Z α).prod (Z α) := add_Z (by simpa using hs),
-  rcases mem_prod_iff.1 this with ⟨V₁, H₁, V₂, H₂, H⟩,
-  exact ⟨V₁ ∩ V₂, inter_mem_sets H₁ H₂, assume v w ⟨hv, _⟩ ⟨_, hw⟩, @H (v, w) ⟨hv, hw⟩⟩
+  have : ((λa:α×α, a.1 + a.2) ⁻¹' s) ∈ Z α ×ᶠ Z α := add_Z (by simpa using hs),
+  rcases mem_prod_self_iff.1 this with ⟨V, H, H'⟩,
+  exact ⟨V, H, prod_subset_iff.1 H'⟩
 end
 
 lemma nhds_eq (a : α) : 𝓝 a = map (λx, x + a) (Z α) :=
@@ -326,10 +326,10 @@ topological_space.nhds_mk_of_nhds _ _
     begin
       refine ⟨(λx:α, x + b) '' t, image_mem_map ht, _, _⟩,
       { refine set.image_subset_iff.2 (assume b hbt, _),
-        simpa using eqt 0 b t0 hbt },
+        simpa using eqt 0 t0 b hbt },
       { rintros _ ⟨c, hb, rfl⟩,
         refine (Z α).sets_of_superset ht (assume x hxt, _),
-        simpa [add_assoc] using eqt _ _ hxt hb }
+        simpa [add_assoc] using eqt _ hxt _ hb }
     end)
 
 lemma nhds_zero_eq_Z : 𝓝 0 = Z α := by simp [nhds_eq]; exact filter.map_id
@@ -340,7 +340,7 @@ instance : has_continuous_add α :=
   begin
     rw [continuous_at, nhds_prod_eq, nhds_eq, nhds_eq, nhds_eq, filter.prod_map_map_eq,
       tendsto_map'_iff],
-    suffices :  tendsto ((λx:α, (a + b) + x) ∘ (λp:α×α,p.1 + p.2)) (filter.prod (Z α) (Z α))
+    suffices :  tendsto ((λx:α, (a + b) + x) ∘ (λp:α×α,p.1 + p.2)) (Z α ×ᶠ Z α)
       (map (λx:α, (a + b) + x) (Z α)),
     { simpa [(∘), add_comm, add_left_comm] },
     exact tendsto_map.comp add_Z

src/topology/algebra/infinite_sum.lean

@@ -718,7 +718,7 @@ begin
     { simp only [(finset.sum_sdiff ht₁).symm, (finset.sum_sdiff ht₂).symm,
         add_sub_add_right_eq_sub] },
     simp only [this],
-    exact hde _ _ (h _ finset.sdiff_disjoint) (h _ finset.sdiff_disjoint) }
+    exact hde _ (h _ finset.sdiff_disjoint) _ (h _ finset.sdiff_disjoint) }
 end
 
 variable [complete_space α]

src/topology/algebra/uniform_group.lean

@@ -21,7 +21,7 @@ import tactic.abel
 -/
 
 noncomputable theory
-open_locale classical uniformity topological_space
+open_locale classical uniformity topological_space filter
 
 section uniform_add_group
 open filter set
@@ -355,7 +355,7 @@ begin
   let Nx := 𝓝 x₀,
   let ee := λ u : β × β, (e u.1, e u.2),
 
-  have lim1 : tendsto (λ a : β × β, (a.2 - a.1, y₁)) (filter.prod (comap e Nx) (comap e Nx)) (𝓝 (0, y₁)),
+  have lim1 : tendsto (λ a : β × β, (a.2 - a.1, y₁)) (comap e Nx ×ᶠ comap e Nx) (𝓝 (0, y₁)),
   { have := tendsto.prod_mk (tendsto_sub_comap_self de x₀) (tendsto_const_nhds : tendsto (λ (p : β × β), y₁) (comap ee $ 𝓝 (x₀, x₀)) (𝓝 y₁)),
     rw [nhds_prod_eq, prod_comap_comap_eq, ←nhds_prod_eq],
     exact (this : _) },
@@ -380,9 +380,9 @@ begin
     rwa [is_Z_bilin.zero φ] at this },
 
   have lim_φ_sub_sub : tendsto (λ (p : (β × β) × (δ × δ)), φ (p.1.2 - p.1.1, p.2.2 - p.2.1))
-    (filter.prod (comap ee $ 𝓝 (x₀, x₀)) (comap ff $ 𝓝 (y₀, y₀))) (𝓝 0),
+    ((comap ee $ 𝓝 (x₀, x₀)) ×ᶠ (comap ff $ 𝓝 (y₀, y₀))) (𝓝 0),
   { have lim_sub_sub :  tendsto (λ (p : (β × β) × δ × δ), (p.1.2 - p.1.1, p.2.2 - p.2.1))
-      (filter.prod (comap ee (𝓝 (x₀, x₀))) (comap ff (𝓝 (y₀, y₀)))) (filter.prod (𝓝 0) (𝓝 0)),
+      ((comap ee (𝓝 (x₀, x₀))) ×ᶠ (comap ff (𝓝 (y₀, y₀)))) (𝓝 0 ×ᶠ 𝓝 0),
     { have := filter.prod_mono (tendsto_sub_comap_self de x₀) (tendsto_sub_comap_self df y₀),
       rwa prod_map_map_eq at this },
     rw ← nhds_prod_eq at lim_sub_sub,
@@ -450,7 +450,7 @@ begin
     cc },
   { suffices : map (λ (p : (β × δ) × (β × δ)), φ p.2 - φ p.1)
       (comap (λ (p : (β × δ) × β × δ), ((e p.1.1, f p.1.2), (e p.2.1, f p.2.2)))
-         (filter.prod (𝓝 (x₀, y₀)) (𝓝 (x₀, y₀)))) ≤ 𝓝 0,
+         (𝓝 (x₀, y₀) ×ᶠ 𝓝 (x₀, y₀))) ≤ 𝓝 0,
     by rwa [uniformity_eq_comap_nhds_zero G, prod_map_map_eq, ←map_le_iff_le_comap, filter.map_map,
         prod_comap_comap_eq],
 

src/topology/constructions.lean

@@ -154,7 +154,7 @@ lemma is_open_prod {s : set α} {t : set β} (hs : is_open s) (ht : is_open t) :
   is_open (set.prod s t) :=
 is_open_inter (continuous_fst s hs) (continuous_snd t ht)
 
-lemma nhds_prod_eq {a : α} {b : β} : 𝓝 (a, b) = filter.prod (𝓝 a) (𝓝 b) :=
+lemma nhds_prod_eq {a : α} {b : β} : 𝓝 (a, b) = 𝓝 a ×ᶠ 𝓝 b :=
 by rw [filter.prod, prod.topological_space, nhds_inf, nhds_induced, nhds_induced]
 
 instance [discrete_topology α] [discrete_topology β] : discrete_topology (α × β) :=
@@ -314,8 +314,7 @@ end
 lemma closure_prod_eq {s : set α} {t : set β} :
   closure (set.prod s t) = set.prod (closure s) (closure t) :=
 set.ext $ assume ⟨a, b⟩,
-have filter.prod (𝓝 a) (𝓝 b) ⊓ 𝓟 (set.prod s t) =
-  filter.prod (𝓝 a ⊓ 𝓟 s) (𝓝 b ⊓ 𝓟 t),
+have (𝓝 a ×ᶠ 𝓝 b) ⊓ 𝓟 (set.prod s t) = (𝓝 a ⊓ 𝓟 s) ×ᶠ (𝓝 b ⊓ 𝓟 t),
   by rw [←prod_inf_prod, prod_principal_principal],
 by simp [closure_eq_cluster_pts, cluster_pt, nhds_prod_eq, this]; exact prod_ne_bot
 

src/topology/continuous_on.lean

@@ -172,7 +172,7 @@ end
 
 lemma nhds_within_prod_eq {α : Type*} [topological_space α] {β : Type*} [topological_space β]
   (a : α) (b : β) (s : set α) (t : set β) :
-  𝓝[s.prod t] (a, b) = (𝓝[s] a).prod (𝓝[t] b) :=
+  𝓝[s.prod t] (a, b) = 𝓝[s] a ×ᶠ 𝓝[t] b :=
 by { delta nhds_within, rw [nhds_prod_eq, ←filter.prod_inf_prod, filter.prod_principal_principal] }
 
 lemma nhds_within_prod {α : Type*} [topological_space α] {β : Type*} [topological_space β]

src/topology/list.lean

@@ -8,7 +8,7 @@ Topology on lists and vectors.
 import topology.constructions
 
 open topological_space set filter
-open_locale topological_space
+open_locale topological_space filter
 
 variables {α : Type*} {β : Type*}
 
@@ -59,7 +59,7 @@ namespace list
 variables [topological_space α] [topological_space β]
 
 lemma tendsto_cons' {a : α} {l : list α} :
-  tendsto (λp:α×list α, list.cons p.1 p.2) ((𝓝 a).prod (𝓝 l)) (𝓝 (a :: l)) :=
+  tendsto (λp:α×list α, list.cons p.1 p.2) (𝓝 a ×ᶠ 𝓝 l) (𝓝 (a :: l)) :=
 by rw [nhds_cons, tendsto, map_prod]; exact le_refl _
 
 lemma tendsto_cons {α : Type*} {f : α → β} {g : α → list β}
@@ -68,8 +68,8 @@ lemma tendsto_cons {α : Type*} {f : α → β} {g : α → list β}
 tendsto_cons'.comp (tendsto.prod_mk hf hg)
 
 lemma tendsto_cons_iff {β : Type*} {f : list α → β} {b : _root_.filter β} {a : α} {l : list α} :
-  tendsto f (𝓝 (a :: l)) b ↔ tendsto (λp:α×list α, f (p.1 :: p.2)) ((𝓝 a).prod (𝓝 l)) b :=
-have 𝓝 (a :: l) = ((𝓝 a).prod (𝓝 l)).map (λp:α×list α, (p.1 :: p.2)),
+  tendsto f (𝓝 (a :: l)) b ↔ tendsto (λp:α×list α, f (p.1 :: p.2)) (𝓝 a ×ᶠ 𝓝 l) b :=
+have 𝓝 (a :: l) = (𝓝 a ×ᶠ 𝓝 l).map (λp:α×list α, (p.1 :: p.2)),
 begin
   simp only
     [nhds_cons, filter.prod_eq, (filter.map_def _ _).symm, (filter.seq_eq_filter_seq _ _).symm],
@@ -79,7 +79,7 @@ by rw [this, filter.tendsto_map'_iff]
 
 lemma tendsto_nhds {β : Type*} {f : list α → β} {r : list α → _root_.filter β}
   (h_nil : tendsto f (pure []) (r []))
-  (h_cons : ∀l a, tendsto f (𝓝 l) (r l) → tendsto (λp:α×list α, f (p.1 :: p.2)) ((𝓝 a).prod (𝓝 l)) (r (a::l))) :
+  (h_cons : ∀l a, tendsto f (𝓝 l) (r l) → tendsto (λp:α×list α, f (p.1 :: p.2)) (𝓝 a ×ᶠ 𝓝 l) (r (a::l))) :
   ∀l, tendsto f (𝓝 l) (r l)
 | []     := by rwa [nhds_nil]
 | (a::l) := by rw [tendsto_cons_iff]; exact h_cons l a (tendsto_nhds l)
@@ -97,15 +97,15 @@ begin
 end
 
 lemma tendsto_insert_nth' {a : α} : ∀{n : ℕ} {l : list α},
-  tendsto (λp:α×list α, insert_nth n p.1 p.2) ((𝓝 a).prod (𝓝 l)) (𝓝 (insert_nth n a l))
+  tendsto (λp:α×list α, insert_nth n p.1 p.2) (𝓝 a ×ᶠ 𝓝 l) (𝓝 (insert_nth n a l))
 | 0     l  := tendsto_cons'
 | (n+1) [] :=
   suffices tendsto (λa, []) (𝓝 a) (𝓝 ([] : list α)),
     by simpa [nhds_nil, tendsto, map_prod, (∘), insert_nth],
   tendsto_const_nhds
 | (n+1) (a'::l) :=
-  have (𝓝 a).prod (𝓝 (a' :: l)) =
-    ((𝓝 a).prod ((𝓝 a').prod (𝓝 l))).map (λp:α×α×list α, (p.1, p.2.1 :: p.2.2)),
+  have 𝓝 a ×ᶠ 𝓝 (a' :: l) =
+    (𝓝 a ×ᶠ (𝓝 a' ×ᶠ 𝓝 l)).map (λp:α×α×list α, (p.1, p.2.1 :: p.2.2)),
   begin
     simp only
       [nhds_cons, filter.prod_eq, (filter.map_def _ _).symm, (filter.seq_eq_filter_seq _ _).symm],
@@ -150,14 +150,14 @@ instance (n : ℕ) [topological_space α] : topological_space (vector α n) :=
 by unfold vector; apply_instance
 
 lemma tendsto_cons [topological_space α] {n : ℕ} {a : α} {l : vector α n}:
-  tendsto (λp:α×vector α n, vector.cons p.1 p.2) ((𝓝 a).prod (𝓝 l)) (𝓝 (a :: l)) :=
+  tendsto (λp:α×vector α n, vector.cons p.1 p.2) (𝓝 a ×ᶠ 𝓝 l) (𝓝 (a :: l)) :=
 by { simp [tendsto_subtype_rng, ←subtype.val_eq_coe, cons_val],
   exact tendsto_cons tendsto_fst (tendsto.comp continuous_at_subtype_coe tendsto_snd) }
 
 lemma tendsto_insert_nth
   [topological_space α] {n : ℕ} {i : fin (n+1)} {a:α} :
   ∀{l:vector α n}, tendsto (λp:α×vector α n, insert_nth p.1 i p.2)
-    ((𝓝 a).prod (𝓝 l)) (𝓝 (insert_nth a i l))
+    (𝓝 a ×ᶠ 𝓝 l) (𝓝 (insert_nth a i l))
 | ⟨l, hl⟩ :=
 begin
   rw [insert_nth, tendsto_subtype_rng],