chore(Filter/Prod): drop Filter.prod, use SProd instead (#18315)

This way we can't accidentally use the underlying `Filter.prod` instead of the normal form.

Author: urkud

Mathlib/Analysis/SpecialFunctions/NonIntegrable.lean

@@ -58,7 +58,7 @@ theorem not_integrableOn_of_tendsto_norm_atTop_of_deriv_isBigO_filter_aux
       (∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], DifferentiableAt ℝ f z) ∧
         ∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], ‖deriv f z‖ ≤ C * ‖g z‖ := by
     rcases hfg.exists_nonneg with ⟨C, C₀, hC⟩
-    have h : ∀ᶠ x : ℝ × ℝ in l.prod l,
+    have h : ∀ᶠ x : ℝ × ℝ in l ×ˢ l,
         ∀ y ∈ [[x.1, x.2]], (DifferentiableAt ℝ f y ∧ ‖deriv f y‖ ≤ C * ‖g y‖) ∧ y ∈ k :=
       (tendsto_fst.uIcc tendsto_snd).eventually ((hd.and hC.bound).and hl).smallSets
     rcases mem_prod_self_iff.1 h with ⟨s, hsl, hs⟩

Mathlib/Data/Analysis/Filter.lean

@@ -286,7 +286,7 @@ protected def iSup {f : α → Filter β} (F : ∀ i, (f i).Realizer) : (⨆ i,
       ⟨fun ⟨_, f⟩ i ↦ f i ⟨⟩, fun f ↦ ⟨(), fun i _ ↦ f i⟩, fun _ ↦ rfl, fun _ ↦ rfl⟩
 
 /-- Construct a realizer for the product of filters -/
-protected def prod {f g : Filter α} (F : f.Realizer) (G : g.Realizer) : (f.prod g).Realizer :=
+protected def prod {f g : Filter α} (F : f.Realizer) (G : g.Realizer) : (f ×ˢ g).Realizer :=
   (F.comap _).inf (G.comap _)
 
 theorem le_iff {f g : Filter α} (F : f.Realizer) (G : g.Realizer) :

Mathlib/Order/Filter/Basic.lean

@@ -646,6 +646,10 @@ theorem eventually_or_distrib_right {f : Filter α} {p : α → Prop} {q : Prop}
     (∀ᶠ x in f, p x ∨ q) ↔ (∀ᶠ x in f, p x) ∨ q := by
   simp only [@or_comm _ q, eventually_or_distrib_left]
 
+theorem eventually_imp_distrib_left {f : Filter α} {p : Prop} {q : α → Prop} :
+    (∀ᶠ x in f, p → q x) ↔ p → ∀ᶠ x in f, q x := by
+  simp only [imp_iff_not_or, eventually_or_distrib_left]
+
 @[simp]
 theorem eventually_bot {p : α → Prop} : ∀ᶠ x in ⊥, p x :=
   ⟨⟩
@@ -798,6 +802,16 @@ theorem eventually_imp_distrib_right {f : Filter α} {p : α → Prop} {q : Prop
     (∀ᶠ x in f, p x → q) ↔ (∃ᶠ x in f, p x) → q := by
   simp only [imp_iff_not_or, eventually_or_distrib_right, not_frequently]
 
+@[simp]
+theorem frequently_and_distrib_left {f : Filter α} {p : Prop} {q : α → Prop} :
+    (∃ᶠ x in f, p ∧ q x) ↔ p ∧ ∃ᶠ x in f, q x := by
+  simp only [Filter.Frequently, not_and, eventually_imp_distrib_left, Classical.not_imp]
+
+@[simp]
+theorem frequently_and_distrib_right {f : Filter α} {p : α → Prop} {q : Prop} :
+    (∃ᶠ x in f, p x ∧ q) ↔ (∃ᶠ x in f, p x) ∧ q := by
+  simp only [@and_comm _ q, frequently_and_distrib_left]
+
 @[simp]
 theorem frequently_bot {p : α → Prop} : ¬∃ᶠ x in ⊥, p x := by simp
 

Mathlib/Order/Filter/Curry.lean

@@ -47,46 +47,34 @@ uniform convergence, curried filters, product filters
 
 namespace Filter
 
-variable {α β γ : Type*}
+variable {α β γ : Type*} {l : Filter α} {m : Filter β} {s : Set α} {t : Set β}
 
-theorem eventually_curry_iff {f : Filter α} {g : Filter β} {p : α × β → Prop} :
-    (∀ᶠ x : α × β in f.curry g, p x) ↔ ∀ᶠ x : α in f, ∀ᶠ y : β in g, p (x, y) :=
+theorem eventually_curry_iff {p : α × β → Prop} :
+    (∀ᶠ x : α × β in l.curry m, p x) ↔ ∀ᶠ x : α in l, ∀ᶠ y : β in m, p (x, y) :=
   Iff.rfl
 
-theorem frequently_curry_iff {α β : Type*} {l : Filter α} {m : Filter β}
+theorem frequently_curry_iff
     (p : (α × β) → Prop) : (∃ᶠ x in l.curry m, p x) ↔ ∃ᶠ x in l, ∃ᶠ y in m, p (x, y) := by
   simp_rw [Filter.Frequently, not_iff_not, not_not, eventually_curry_iff]
 
-theorem mem_curry_iff {f : Filter α} {g : Filter β} {s : Set (α × β)} :
-    s ∈ f.curry g ↔ ∀ᶠ x : α in f, ∀ᶠ y : β in g, (x, y) ∈ s := Iff.rfl
+theorem mem_curry_iff {s : Set (α × β)} :
+    s ∈ l.curry m ↔ ∀ᶠ x : α in l, ∀ᶠ y : β in m, (x, y) ∈ s := Iff.rfl
 
-theorem curry_le_prod {f : Filter α} {g : Filter β} : f.curry g ≤ f.prod g :=
-  fun _ => Eventually.curry
+theorem curry_le_prod : l.curry m ≤ l ×ˢ m := fun _ => Eventually.curry
 
 theorem Tendsto.curry {f : α → β → γ} {la : Filter α} {lb : Filter β} {lc : Filter γ}
     (h : ∀ᶠ a in la, Tendsto (fun b : β => f a b) lb lc) : Tendsto (↿f) (la.curry lb) lc :=
   fun _s hs => h.mono fun _a ha => ha hs
 
-theorem frequently_curry_prod_iff {α β : Type*} {l : Filter α} {m : Filter β}
-    (s : Set α) (t : Set β) : (∃ᶠ x in l.curry m, x ∈ s ×ˢ t) ↔ sᶜ ∉ l ∧ tᶜ ∉ m := by
-  refine ⟨fun h => ?_, fun ⟨hs, ht⟩ => ?_⟩
-  · exact frequently_prod_and.mp (Frequently.filter_mono h curry_le_prod)
-  rw [frequently_curry_iff]
-  exact Frequently.mono hs <| fun x hx => Frequently.mono ht (by simp [hx])
+theorem frequently_curry_prod_iff :
+    (∃ᶠ x in l.curry m, x ∈ s ×ˢ t) ↔ (∃ᶠ x in l, x ∈ s) ∧ ∃ᶠ y in m, y ∈ t := by
+  simp [frequently_curry_iff]
 
-theorem prod_mem_curry {α β : Type*} {l : Filter α} {m : Filter β} {s : Set α} {t : Set β}
-    (hs : s ∈ l) (ht : t ∈ m) : s ×ˢ t ∈ l.curry m :=
-  curry_le_prod <| prod_mem_prod hs ht
-
-theorem eventually_curry_prod_iff {α β : Type*} {l : Filter α} {m : Filter β}
-    [NeBot l] [NeBot m] (s : Set α) (t : Set β) :
+theorem eventually_curry_prod_iff [NeBot l] [NeBot m] :
     (∀ᶠ x in l.curry m, x ∈ s ×ˢ t) ↔ s ∈ l ∧ t ∈ m := by
-  refine ⟨fun h => ⟨?_, ?_⟩, fun ⟨hs, ht⟩ => prod_mem_curry hs ht⟩ <;>
-    rw [eventually_curry_iff] at h
-  · apply mem_of_superset h
-    simp
-  rcases h.exists with ⟨_, hx⟩
-  apply mem_of_superset hx
-  exact fun _ hy => hy.2
+  simp [eventually_curry_iff]
+
+theorem prod_mem_curry (hs : s ∈ l) (ht : t ∈ m) : s ×ˢ t ∈ l.curry m :=
+  curry_le_prod <| prod_mem_prod hs ht
 
 end Filter

Mathlib/Order/Filter/Defs.lean

@@ -301,17 +301,20 @@ def comap (m : α → β) (f : Filter β) : Filter α where
   inter_sets := fun ⟨a', ha₁, ha₂⟩ ⟨b', hb₁, hb₂⟩ =>
     ⟨a' ∩ b', inter_mem ha₁ hb₁, inter_subset_inter ha₂ hb₂⟩
 
-/-- Product of filters. This is the filter generated by cartesian products
-of elements of the component filters. -/
-protected def prod (f : Filter α) (g : Filter β) : Filter (α × β) :=
-  f.comap Prod.fst ⊓ g.comap Prod.snd
-
 /-- Coproduct of filters. -/
 protected def coprod (f : Filter α) (g : Filter β) : Filter (α × β) :=
   f.comap Prod.fst ⊔ g.comap Prod.snd
 
+/-- Product of filters. This is the filter generated by cartesian products
+of elements of the component filters. -/
 instance instSProd : SProd (Filter α) (Filter β) (Filter (α × β)) where
-  sprod := Filter.prod
+  sprod f g := f.comap Prod.fst ⊓ g.comap Prod.snd
+
+/-- Product of filters. This is the filter generated by cartesian products
+of elements of the component filters.
+Deprecated. Use `f ×ˢ g` instead. -/
+@[deprecated (since := "2024-11-29")]
+protected def prod (f : Filter α) (g : Filter β) : Filter (α × β) := f ×ˢ g
 
 theorem prod_eq_inf (f : Filter α) (g : Filter β) : f ×ˢ g = f.comap Prod.fst ⊓ g.comap Prod.snd :=
   rfl

Mathlib/Order/Filter/Finite.lean

@@ -263,23 +263,6 @@ alias _root_.Finset.eventually_all := eventually_all_finset
 
 -- attribute [protected] Finset.eventually_all
 
-theorem eventually_imp_distrib_left {f : Filter α} {p : Prop} {q : α → Prop} :
-    (∀ᶠ x in f, p → q x) ↔ p → ∀ᶠ x in f, q x :=
-  eventually_all
-
-
-/-! ### Frequently -/
-
-@[simp]
-theorem frequently_and_distrib_left {f : Filter α} {p : Prop} {q : α → Prop} :
-    (∃ᶠ x in f, p ∧ q x) ↔ p ∧ ∃ᶠ x in f, q x := by
-  simp only [Filter.Frequently, not_and, eventually_imp_distrib_left, Classical.not_imp]
-
-@[simp]
-theorem frequently_and_distrib_right {f : Filter α} {p : α → Prop} {q : Prop} :
-    (∃ᶠ x in f, p x ∧ q) ↔ (∃ᶠ x in f, p x) ∧ q := by
-  simp only [@and_comm _ q, frequently_and_distrib_left]
-
 /-!
 ### Relation “eventually equal”
 -/

Mathlib/Order/Filter/Prod.lean

@@ -51,7 +51,6 @@ theorem prod_mem_prod (hs : s ∈ f) (ht : t ∈ g) : s ×ˢ t ∈ f ×ˢ g :=
 
 theorem mem_prod_iff {s : Set (α × β)} {f : Filter α} {g : Filter β} :
     s ∈ f ×ˢ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ s := by
-  simp only [SProd.sprod, Filter.prod]
   constructor
   · rintro ⟨t₁, ⟨s₁, hs₁, hts₁⟩, t₂, ⟨s₂, hs₂, hts₂⟩, rfl⟩
     exact ⟨s₁, hs₁, s₂, hs₂, fun p ⟨h, h'⟩ => ⟨hts₁ h, hts₂ h'⟩⟩
@@ -100,20 +99,16 @@ theorem comap_prodMap_prod (f : α → β) (g : γ → δ) (lb : Filter β) (ld
   simp [prod_eq_inf, comap_comap, Function.comp_def]
 
 theorem prod_top : f ×ˢ (⊤ : Filter β) = f.comap Prod.fst := by
-  dsimp only [SProd.sprod]
-  rw [Filter.prod, comap_top, inf_top_eq]
+  rw [prod_eq_inf, comap_top, inf_top_eq]
 
 theorem top_prod : (⊤ : Filter α) ×ˢ g = g.comap Prod.snd := by
-  dsimp only [SProd.sprod]
-  rw [Filter.prod, comap_top, top_inf_eq]
+  rw [prod_eq_inf, comap_top, top_inf_eq]
 
 theorem sup_prod (f₁ f₂ : Filter α) (g : Filter β) : (f₁ ⊔ f₂) ×ˢ g = (f₁ ×ˢ g) ⊔ (f₂ ×ˢ g) := by
-  dsimp only [SProd.sprod]
-  rw [Filter.prod, comap_sup, inf_sup_right, ← Filter.prod, ← Filter.prod]
+  simp only [prod_eq_inf, comap_sup, inf_sup_right]
 
 theorem prod_sup (f : Filter α) (g₁ g₂ : Filter β) : f ×ˢ (g₁ ⊔ g₂) = (f ×ˢ g₁) ⊔ (f ×ˢ g₂) := by
-  dsimp only [SProd.sprod]
-  rw [Filter.prod, comap_sup, inf_sup_left, ← Filter.prod, ← Filter.prod]
+  simp only [prod_eq_inf, comap_sup, inf_sup_left]
 
 theorem eventually_prod_iff {p : α × β → Prop} :
     (∀ᶠ x in f ×ˢ g, p x) ↔
@@ -203,15 +198,11 @@ theorem tendsto_diag : Tendsto (fun i => (i, i)) f (f ×ˢ f) :=
 
 theorem prod_iInf_left [Nonempty ι] {f : ι → Filter α} {g : Filter β} :
     (⨅ i, f i) ×ˢ g = ⨅ i, f i ×ˢ g := by
-  dsimp only [SProd.sprod]
-  rw [Filter.prod, comap_iInf, iInf_inf]
-  simp only [Filter.prod, eq_self_iff_true]
+  simp only [prod_eq_inf, comap_iInf, iInf_inf]
 
 theorem prod_iInf_right [Nonempty ι] {f : Filter α} {g : ι → Filter β} :
     (f ×ˢ ⨅ i, g i) = ⨅ i, f ×ˢ g i := by
-  dsimp only [SProd.sprod]
-  rw [Filter.prod, comap_iInf, inf_iInf]
-  simp only [Filter.prod, eq_self_iff_true]
+  simp only [prod_eq_inf, comap_iInf, inf_iInf]
 
 @[mono, gcongr]
 theorem prod_mono {f₁ f₂ : Filter α} {g₁ g₂ : Filter β} (hf : f₁ ≤ f₂) (hg : g₁ ≤ g₂) :
@@ -229,11 +220,10 @@ theorem prod_mono_right (f : Filter α) {g₁ g₂ : Filter β} (hf : g₁ ≤ g
 theorem prod_comap_comap_eq.{u, v, w, x} {α₁ : Type u} {α₂ : Type v} {β₁ : Type w} {β₂ : Type x}
     {f₁ : Filter α₁} {f₂ : Filter α₂} {m₁ : β₁ → α₁} {m₂ : β₂ → α₂} :
     comap m₁ f₁ ×ˢ comap m₂ f₂ = comap (fun p : β₁ × β₂ => (m₁ p.1, m₂ p.2)) (f₁ ×ˢ f₂) := by
-  simp only [SProd.sprod, Filter.prod, comap_comap, comap_inf, Function.comp_def]
+  simp only [prod_eq_inf, comap_comap, comap_inf, Function.comp_def]
 
 theorem prod_comm' : f ×ˢ g = comap Prod.swap (g ×ˢ f) := by
-  simp only [SProd.sprod, Filter.prod, comap_comap, Function.comp_def, inf_comm, Prod.swap,
-    comap_inf]
+  simp only [prod_eq_inf, comap_comap, Function.comp_def, inf_comm, Prod.swap, comap_inf]
 
 theorem prod_comm : f ×ˢ g = map (fun p : β × α => (p.2, p.1)) (g ×ˢ f) := by
   rw [prod_comm', ← map_swap_eq_comap_swap]
@@ -280,12 +270,12 @@ theorem eventually_swap_iff {p : α × β → Prop} :
 
 theorem prod_assoc (f : Filter α) (g : Filter β) (h : Filter γ) :
     map (Equiv.prodAssoc α β γ) ((f ×ˢ g) ×ˢ h) = f ×ˢ (g ×ˢ h) := by
-  simp_rw [← comap_equiv_symm, SProd.sprod, Filter.prod, comap_inf, comap_comap, inf_assoc,
+  simp_rw [← comap_equiv_symm, prod_eq_inf, comap_inf, comap_comap, inf_assoc,
     Function.comp_def, Equiv.prodAssoc_symm_apply]
 
 theorem prod_assoc_symm (f : Filter α) (g : Filter β) (h : Filter γ) :
     map (Equiv.prodAssoc α β γ).symm (f ×ˢ (g ×ˢ h)) = (f ×ˢ g) ×ˢ h := by
-  simp_rw [map_equiv_symm, SProd.sprod, Filter.prod, comap_inf, comap_comap, inf_assoc,
+  simp_rw [map_equiv_symm, prod_eq_inf, comap_inf, comap_comap, inf_assoc,
     Function.comp_def, Equiv.prodAssoc_apply]
 
 theorem tendsto_prodAssoc {h : Filter γ} :
@@ -300,7 +290,7 @@ theorem tendsto_prodAssoc_symm {h : Filter γ} :
 theorem map_swap4_prod {h : Filter γ} {k : Filter δ} :
     map (fun p : (α × β) × γ × δ => ((p.1.1, p.2.1), (p.1.2, p.2.2))) ((f ×ˢ g) ×ˢ (h ×ˢ k)) =
       (f ×ˢ h) ×ˢ (g ×ˢ k) := by
-  simp_rw [map_swap4_eq_comap, SProd.sprod, Filter.prod, comap_inf, comap_comap]; ac_rfl
+  simp_rw [map_swap4_eq_comap, prod_eq_inf, comap_inf, comap_comap]; ac_rfl
 
 theorem tendsto_swap4_prod {h : Filter γ} {k : Filter δ} :
     Tendsto (fun p : (α × β) × γ × δ => ((p.1.1, p.2.1), (p.1.2, p.2.2))) ((f ×ˢ g) ×ˢ (h ×ˢ k))
@@ -351,7 +341,7 @@ theorem prod_eq : f ×ˢ g = (f.map Prod.mk).seq g := f.map_prod id g
 
 theorem prod_inf_prod {f₁ f₂ : Filter α} {g₁ g₂ : Filter β} :
     (f₁ ×ˢ g₁) ⊓ (f₂ ×ˢ g₂) = (f₁ ⊓ f₂) ×ˢ (g₁ ⊓ g₂) := by
-  simp only [SProd.sprod, Filter.prod, comap_inf, inf_comm, inf_assoc, inf_left_comm]
+  simp only [prod_eq_inf, comap_inf, inf_comm, inf_assoc, inf_left_comm]
 
 theorem inf_prod {f₁ f₂ : Filter α} : (f₁ ⊓ f₂) ×ˢ g = (f₁ ×ˢ g) ⊓ (f₂ ×ˢ g) := by
   rw [prod_inf_prod, inf_idem]
@@ -361,8 +351,7 @@ theorem prod_inf {g₁ g₂ : Filter β} : f ×ˢ (g₁ ⊓ g₂) = (f ×ˢ g₁
 
 @[simp]
 theorem prod_principal_principal {s : Set α} {t : Set β} : 𝓟 s ×ˢ 𝓟 t = 𝓟 (s ×ˢ t) := by
-  simp only [SProd.sprod, Filter.prod, comap_principal, principal_eq_iff_eq, comap_principal,
-    inf_principal]; rfl
+  simp only [prod_eq_inf, comap_principal, principal_eq_iff_eq, comap_principal, inf_principal]; rfl
 
 @[simp]
 theorem pure_prod {a : α} {f : Filter β} : pure a ×ˢ f = map (Prod.mk a) f := by
@@ -413,9 +402,7 @@ theorem tendsto_prod_iff {f : α × β → γ} {x : Filter α} {y : Filter β} {
 
 theorem tendsto_prod_iff' {g' : Filter γ} {s : α → β × γ} :
     Tendsto s f (g ×ˢ g') ↔ Tendsto (fun n => (s n).1) f g ∧ Tendsto (fun n => (s n).2) f g' := by
-  dsimp only [SProd.sprod]
-  unfold Filter.prod
-  simp only [tendsto_inf, tendsto_comap_iff, Function.comp_def]
+  simp only [prod_eq_inf, tendsto_inf, tendsto_comap_iff, Function.comp_def]
 
 theorem le_prod {f : Filter (α × β)} {g : Filter α} {g' : Filter β} :
     (f ≤ g ×ˢ g') ↔ Tendsto Prod.fst f g ∧ Tendsto Prod.snd f g' :=

Mathlib/Topology/Algebra/UniformGroup/Defs.lean

@@ -406,19 +406,11 @@ variable {G}
 @[to_additive]
 -- Porting note: renamed theorem to conform to naming convention
 theorem comm_topologicalGroup_is_uniform : UniformGroup G := by
-  have :
-    Tendsto
-      ((fun p : G × G => p.1 / p.2) ∘ fun p : (G × G) × G × G => (p.1.2 / p.1.1, p.2.2 / p.2.1))
-      (comap (fun p : (G × G) × G × G => (p.1.2 / p.1.1, p.2.2 / p.2.1)) ((𝓝 1).prod (𝓝 1)))
-      (𝓝 (1 / 1)) :=
-    (tendsto_fst.div' tendsto_snd).comp tendsto_comap
   constructor
-  rw [UniformContinuous, uniformity_prod_eq_prod, tendsto_map'_iff, uniformity_eq_comap_nhds_one' G,
-    tendsto_comap_iff, prod_comap_comap_eq]
-  simp only [Function.comp_def, div_eq_mul_inv, mul_inv_rev, inv_inv, mul_comm, mul_left_comm] at *
-  simp only [inv_one, mul_one, ← mul_assoc] at this
-  simp_rw [← mul_assoc, mul_comm]
-  assumption
+  simp only [UniformContinuous, uniformity_prod_eq_prod, uniformity_eq_comap_nhds_one',
+    tendsto_comap_iff, tendsto_map'_iff, prod_comap_comap_eq, Function.comp_def,
+    div_div_div_comm _ (Prod.snd (Prod.snd _)), ← nhds_prod_eq, Prod.mk_one_one]
+  exact (continuous_div'.tendsto' 1 1 (div_one 1)).comp tendsto_comap
 
 open Set
 

Mathlib/Topology/Constructions.lean

@@ -477,11 +477,9 @@ theorem IsOpen.prod {s : Set X} {t : Set Y} (hs : IsOpen s) (ht : IsOpen t) : Is
 
 -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11215): TODO: Lean fails to find `t₁` and `t₂` by unification
 theorem nhds_prod_eq {x : X} {y : Y} : 𝓝 (x, y) = 𝓝 x ×ˢ 𝓝 y := by
-  dsimp only [SProd.sprod]
-  rw [Filter.prod, instTopologicalSpaceProd, nhds_inf (t₁ := TopologicalSpace.induced Prod.fst _)
+  rw [prod_eq_inf, instTopologicalSpaceProd, nhds_inf (t₁ := TopologicalSpace.induced Prod.fst _)
     (t₂ := TopologicalSpace.induced Prod.snd _), nhds_induced, nhds_induced]
 
--- Porting note: moved from `Topology.ContinuousOn`
 theorem nhdsWithin_prod_eq (x : X) (y : Y) (s : Set X) (t : Set Y) :
     𝓝[s ×ˢ t] (x, y) = 𝓝[s] x ×ˢ 𝓝[t] y := by
   simp only [nhdsWithin, nhds_prod_eq, ← prod_inf_prod, prod_principal_principal]
@@ -504,15 +502,13 @@ theorem mem_nhdsWithin_prod_iff {x : X} {y : Y} {s : Set (X × Y)} {tx : Set X}
     s ∈ 𝓝[tx ×ˢ ty] (x, y) ↔ ∃ u ∈ 𝓝[tx] x, ∃ v ∈ 𝓝[ty] y, u ×ˢ v ⊆ s := by
   rw [nhdsWithin_prod_eq, mem_prod_iff]
 
--- Porting note: moved up
 theorem Filter.HasBasis.prod_nhds {ιX ιY : Type*} {px : ιX → Prop} {py : ιY → Prop}
     {sx : ιX → Set X} {sy : ιY → Set Y} {x : X} {y : Y} (hx : (𝓝 x).HasBasis px sx)
     (hy : (𝓝 y).HasBasis py sy) :
     (𝓝 (x, y)).HasBasis (fun i : ιX × ιY => px i.1 ∧ py i.2) fun i => sx i.1 ×ˢ sy i.2 := by
   rw [nhds_prod_eq]
   exact hx.prod hy
 
--- Porting note: moved up
 theorem Filter.HasBasis.prod_nhds' {ιX ιY : Type*} {pX : ιX → Prop} {pY : ιY → Prop}
     {sx : ιX → Set X} {sy : ιY → Set Y} {p : X × Y} (hx : (𝓝 p.1).HasBasis pX sx)
     (hy : (𝓝 p.2).HasBasis pY sy) :

Mathlib/Topology/Instances/TrivSqZeroExt.lean

@@ -42,14 +42,12 @@ instance instTopologicalSpace : TopologicalSpace (tsze R M) :=
 instance [T2Space R] [T2Space M] : T2Space (tsze R M) :=
   Prod.t2Space
 
-theorem nhds_def (x : tsze R M) : 𝓝 x = (𝓝 x.fst).prod (𝓝 x.snd) := by
-  cases x using Prod.rec
-  exact nhds_prod_eq
+theorem nhds_def (x : tsze R M) : 𝓝 x = 𝓝 x.fst ×ˢ 𝓝 x.snd := nhds_prod_eq
 
-theorem nhds_inl [Zero M] (x : R) : 𝓝 (inl x : tsze R M) = (𝓝 x).prod (𝓝 0) :=
+theorem nhds_inl [Zero M] (x : R) : 𝓝 (inl x : tsze R M) = 𝓝 x ×ˢ 𝓝 0 :=
   nhds_def _
 
-theorem nhds_inr [Zero R] (m : M) : 𝓝 (inr m : tsze R M) = (𝓝 0).prod (𝓝 m) :=
+theorem nhds_inr [Zero R] (m : M) : 𝓝 (inr m : tsze R M) = 𝓝 0 ×ˢ 𝓝 m :=
   nhds_def _
 
 nonrec theorem continuous_fst : Continuous (fst : tsze R M → R) :=