chore(topology/constructions): rename tendsto_prod_mk_nhds (#2008)

New name is `tendsto.prod_mk_nhds`. Also use it in a few proofs and
generalize `tendsto_smul` to a `topological_semimodule`.

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

src/analysis/calculus/tangent_cone.lean

@@ -166,7 +166,7 @@ begin
     assume n hn,
     simp at hn,
     simp [hn, (hd' n).1] },
-  { apply tendsto_prod_mk_nhds hy,
+  { apply hy.prod_mk_nhds,
     change tendsto (λ (n : ℕ), c n • d' n) at_top (𝓝 0),
     rw tendsto_zero_iff_norm_tendsto_zero,
     refine squeeze_zero (λn, norm_nonneg _) (λn, (hd' n).2) _,
@@ -206,7 +206,7 @@ begin
     assume n hn,
     simp at hn,
     simp [hn, (hd' n).1] },
-  { apply tendsto_prod_mk_nhds _ hy,
+  { apply tendsto.prod_mk_nhds _ hy,
     change tendsto (λ (n : ℕ), c n • d' n) at_top (𝓝 0),
     rw tendsto_zero_iff_norm_tendsto_zero,
     refine squeeze_zero (λn, norm_nonneg _) (λn, (hd' n).2) _,

src/analysis/normed_space/basic.lean

@@ -620,43 +620,21 @@ nnreal.eq $ norm_smul s x
 variables {E : Type*} {F : Type*}
 [normed_group E] [normed_space α E] [normed_group F] [normed_space α F]
 
-lemma tendsto_smul {f : γ → α} { g : γ → F} {e : filter γ} {s : α} {b : F} :
-  (tendsto f e (𝓝 s)) → (tendsto g e (𝓝 b)) → tendsto (λ x, (f x) • (g x)) e (𝓝 (s • b)) :=
+@[priority 100] -- see Note [lower instance priority]
+instance normed_space.topological_vector_space : topological_vector_space α E :=
 begin
-  intros limf limg,
-  rw tendsto_iff_norm_tendsto_zero,
-  have ineq := λ x : γ, calc
-      ∥f x • g x - s • b∥ = ∥(f x • g x - s • g x) + (s • g x - s • b)∥ : by simp[add_assoc]
-                      ... ≤ ∥f x • g x - s • g x∥ + ∥s • g x - s • b∥ : norm_add_le (f x • g x - s • g x) (s • g x - s • b)
-                      ... ≤ ∥f x - s∥*∥g x∥ + ∥s∥*∥g x - b∥ : by { rw [←smul_sub, ←sub_smul, norm_smul, norm_smul] },
-  apply squeeze_zero,
-  { intro t, exact norm_nonneg _ },
-  { exact ineq },
-  { clear ineq,
-
-    have limf': tendsto (λ x, ∥f x - s∥) e (𝓝 0) := tendsto_iff_norm_tendsto_zero.1 limf,
-    have limg' : tendsto (λ x, ∥g x∥) e (𝓝 ∥b∥) := filter.tendsto.comp (continuous_iff_continuous_at.1 continuous_norm _) limg,
-
-    have lim1 := limf'.mul limg',
-    simp only [zero_mul, sub_eq_add_neg] at lim1,
-
-    have limg3 := tendsto_iff_norm_tendsto_zero.1 limg,
-
-    have lim2 := (tendsto_const_nhds : tendsto _ _ (𝓝 ∥ s ∥)).mul limg3,
-    simp only [sub_eq_add_neg, mul_zero] at lim2,
-
-    rw [show (0:ℝ) = 0 + 0, by simp],
-    exact lim1.add lim2  }
+  refine { continuous_smul := continuous_iff_continuous_at.2 $ λ p, tendsto_iff_norm_tendsto_zero.2 _ },
+  refine squeeze_zero (λ _, norm_nonneg _) _ _,
+  { exact λ q, ∥q.1 - p.1∥ * ∥q.2∥ + ∥p.1∥ * ∥q.2 - p.2∥ },
+  { intro q,
+    rw [← sub_add_sub_cancel, ← norm_smul, ← norm_smul, smul_sub, sub_smul],
+    exact norm_add_le _ _ },
+  { conv { congr, skip, skip, congr, rw [← zero_add (0:ℝ)], congr,
+      rw [← zero_mul ∥p.2∥], skip, rw [← mul_zero ∥p.1∥] },
+    exact ((tendsto_iff_norm_tendsto_zero.1 (continuous_fst.tendsto p)).mul (continuous_snd.tendsto p).norm).add
+            (tendsto_const_nhds.mul (tendsto_iff_norm_tendsto_zero.1 (continuous_snd.tendsto p))) }
 end
 
-lemma tendsto_smul_const {g : γ → F} {e : filter γ} (s : α) {b : F} :
-  (tendsto g e (𝓝 b)) → tendsto (λ x, s • (g x)) e (𝓝 (s • b)) :=
-tendsto_smul tendsto_const_nhds
-
-@[priority 100] -- see Note [lower instance priority]
-instance normed_space.topological_vector_space : topological_vector_space α E :=
-{ continuous_smul := continuous_iff_continuous_at.2 $ λp, tendsto_smul
-    (continuous_iff_continuous_at.1 continuous_fst _) (continuous_iff_continuous_at.1 continuous_snd _) }
 
 open normed_field
 

src/topology/algebra/module.lean

@@ -29,7 +29,8 @@ A cosmetic disadvantage is that one can not extend topological vector spaces.
 The solution is to extend `topological_module` instead.
 -/
 
-open topological_space
+open filter
+open_locale topological_space
 
 universes u v w u'
 
@@ -55,10 +56,17 @@ variables {R : Type u} {M : Type v}
 lemma continuous_smul : continuous (λp:R×M, p.1 • p.2) :=
 topological_semimodule.continuous_smul R M
 
-lemma continuous.smul {M₂ : Type*} [topological_space M₂] {f : M₂ → R} {g : M₂ → M}
+lemma continuous.smul {α : Type*} [topological_space α] {f : α → R} {g : α → M}
   (hf : continuous f) (hg : continuous g) : continuous (λp, f p • g p) :=
 continuous_smul.comp (hf.prod_mk hg)
 
+lemma tendsto_smul {c : R} {x : M} : tendsto (λp:R×M, p.fst • p.snd) (𝓝 (c, x)) (𝓝 (c • x)) :=
+continuous_smul.tendsto _
+
+lemma filter.tendsto.smul {α : Type*} {l : filter α} {f : α → R} {g : α → M} {c : R} {x : M}
+  (hf : tendsto f l (𝓝 c)) (hg : tendsto g l (𝓝 x)) : tendsto (λ a, f a • g a) l (𝓝 (c • x)) :=
+tendsto_smul.comp (hf.prod_mk_nhds hg)
+
 end
 
 section prio
@@ -118,7 +126,7 @@ set_option class.instance_max_depth 36
 /-- Scalar multiplication by a non-zero field element is a
 homeomorphism from a topological vector space onto itself. -/
 protected def homeomorph.smul_of_ne_zero (ha : a ≠ 0) : M ≃ₜ M :=
-{.. homeomorph.smul_of_unit ((equiv.units_equiv_ne_zero _).inv_fun ⟨_, ha⟩)}
+{.. homeomorph.smul_of_unit (units.mk0 a ha)}
 
 lemma is_open_map_smul_of_ne_zero (ha : a ≠ 0) : is_open_map (λ (x : M), a • x) :=
 (homeomorph.smul_of_ne_zero ha).is_open_map

src/topology/algebra/monoid.lean

@@ -71,7 +71,7 @@ continuous_iff_continuous_at.mp (topological_monoid.continuous_mul α) (a, b)
 lemma filter.tendsto.mul {f : β → α} {g : β → α} {x : filter β} {a b : α}
   (hf : tendsto f x (𝓝 a)) (hg : tendsto g x (𝓝 b)) :
   tendsto (λx, f x * g x) x (𝓝 (a * b)) :=
-tendsto.comp (by rw [←nhds_prod_eq]; exact tendsto_mul) (hf.prod_mk hg)
+tendsto_mul.comp (hf.prod_mk_nhds hg)
 
 @[to_additive]
 lemma continuous_at.mul [topological_space β] {f : β → α} {g : β → α} {x : β}

src/topology/constructions.lean

@@ -143,14 +143,14 @@ by rw [nhds_prod_eq]; exact prod_mem_prod ha hb
 lemma nhds_swap (a : α) (b : β) : 𝓝 (a, b) = (𝓝 (b, a)).map prod.swap :=
 by rw [nhds_prod_eq, filter.prod_comm, nhds_prod_eq]; refl
 
-lemma tendsto_prod_mk_nhds {γ} {a : α} {b : β} {f : filter γ} {ma : γ → α} {mb : γ → β}
+lemma filter.tendsto.prod_mk_nhds {γ} {a : α} {b : β} {f : filter γ} {ma : γ → α} {mb : γ → β}
   (ha : tendsto ma f (𝓝 a)) (hb : tendsto mb f (𝓝 b)) :
   tendsto (λc, (ma c, mb c)) f (𝓝 (a, b)) :=
 by rw [nhds_prod_eq]; exact filter.tendsto.prod_mk ha hb
 
 lemma continuous_at.prod {f : α → β} {g : α → γ} {x : α}
   (hf : continuous_at f x) (hg : continuous_at g x) : continuous_at (λx, (f x, g x)) x :=
-tendsto_prod_mk_nhds hf hg
+hf.prod_mk_nhds hg
 
 lemma prod_generate_from_generate_from_eq {α : Type*} {β : Type*} {s : set (set α)} {t : set (set β)}
   (hs : ⋃₀ s = univ) (ht : ⋃₀ t = univ) :

src/topology/continuous_on.lean

@@ -516,7 +516,7 @@ end
 lemma continuous_within_at.prod {f : α → β} {g : α → γ} {s : set α} {x : α}
   (hf : continuous_within_at f s x) (hg : continuous_within_at g s x) :
   continuous_within_at (λx, (f x, g x)) s x :=
-tendsto_prod_mk_nhds hf hg
+hf.prod_mk_nhds hg
 
 lemma continuous_on.prod {f : α → β} {g : α → γ} {s : set α}
   (hf : continuous_on f s) (hg : continuous_on g s) : continuous_on (λx, (f x, g x)) s :=

src/topology/instances/ennreal.lean

@@ -250,7 +250,7 @@ protected lemma tendsto.mul {f : filter α} {ma : α → ennreal} {mb : α → e
   (hma : tendsto ma f (𝓝 a)) (ha : a ≠ 0 ∨ b ≠ ⊤) (hmb : tendsto mb f (𝓝 b)) (hb : b ≠ 0 ∨ a ≠ ⊤) :
   tendsto (λa, ma a * mb a) f (𝓝 (a * b)) :=
 show tendsto ((λp:ennreal×ennreal, p.1 * p.2) ∘ (λa, (ma a, mb a))) f (𝓝 (a * b)), from
-tendsto.comp (ennreal.tendsto_mul ha hb) (tendsto_prod_mk_nhds hma hmb)
+tendsto.comp (ennreal.tendsto_mul ha hb) (hma.prod_mk_nhds hmb)
 
 protected lemma tendsto.const_mul {f : filter α} {m : α → ennreal} {a b : ennreal}
   (hm : tendsto m f (𝓝 b)) (hb : b ≠ 0 ∨ a ≠ ⊤) : tendsto (λb, a * m b) f (𝓝 (a * b)) :=