refactor(topology/algebra): use the dot notation in continuous_mul and friends (#1758)

* continuous_add

* fixes

* more fixes

* fix

* tendsto_add

* fix tendsto

* last fix

Author: sgouezel

src/analysis/calculus/fderiv.lean

@@ -160,7 +160,7 @@ begin
   { conv in (nhds_within x s) { rw ← add_zero x },
     rw [← tendsto_iff_comap, nhds_within, tendsto_inf],
     split,
-    { apply tendsto_add tendsto_const_nhds (tangent_cone_at.lim_zero clim cdlim) },
+    { apply tendsto.add tendsto_const_nhds (tangent_cone_at.lim_zero clim cdlim) },
     { rwa tendsto_principal } },
   have : is_o (λ y, f y - f x - f' (y - x)) (λ y, y - x) (nhds_within x s) := h,
   have : is_o (λ n:ℕ, f (x + d n) - f x - f' ((x + d n) - x)) (λ n, (x + d n)  - x)
@@ -179,7 +179,7 @@ begin
     tendsto.comp f'.cont.continuous_at cdlim,
   have L3 : tendsto (λn:ℕ, (c n • (f (x + d n) - f x - f' (d n)) +  f' (c n • d n)))
             at_top (𝓝 (0 + f' v)) :=
-    tendsto_add L1 L2,
+    tendsto.add L1 L2,
   have : (λn:ℕ, (c n • (f (x + d n) - f x - f' (d n)) +  f' (c n • d n)))
           = (λn: ℕ, c n • (f (x + d n) - f x)),
     by { ext n, simp [smul_add] },
@@ -249,7 +249,7 @@ begin
     have : 𝓝 0 ≤ comap (λ (z : E), z + x) (𝓝 (0 + x)),
     { refine tendsto_iff_comap.mp _,
       apply continuous.tendsto,
-      exact continuous_add continuous_id continuous_const },
+      exact continuous.add continuous_id continuous_const },
     apply is_o.mono this,
     convert is_o.comp H (λz, z + x),
     { ext h, simp },
@@ -259,7 +259,7 @@ begin
     have : 𝓝 x ≤ comap (λ (z : E), z - x) (𝓝 (x - x)),
     { refine tendsto_iff_comap.mp _,
       apply continuous.tendsto,
-      exact continuous_add continuous_id continuous_const },
+      exact continuous.add continuous_id continuous_const },
     apply is_o.mono this,
     convert is_o.comp H (λz, z - x),
     { ext h, simp },
@@ -895,8 +895,8 @@ theorem has_fderiv_at_filter.tendsto_nhds
 begin
   have : tendsto (λ x', f x' - f x) L (𝓝 0),
   { refine h.is_O_sub.trans_tendsto (tendsto_le_left hL _),
-    rw ← sub_self x, exact tendsto_sub tendsto_id tendsto_const_nhds },
-  have := tendsto_add this tendsto_const_nhds,
+    rw ← sub_self x, exact tendsto.sub tendsto_id tendsto_const_nhds },
+  have := tendsto.add this tendsto_const_nhds,
   rw zero_add (f x) at this,
   exact this.congr (by simp)
 end
@@ -963,7 +963,7 @@ begin
       have : 0 = ∥p - p∥, by simp,
       rw this,
       have : continuous (λx, ∥x-p∥) :=
-        continuous_norm.comp (continuous_sub continuous_id continuous_const),
+        continuous_norm.comp (continuous.sub continuous_id continuous_const),
       exact this.tendsto p },
     simp only [forall_prop_of_false, not_false_iff, one_ne_zero, forall_true_iff] },
   simp only [one_mul, asymptotics.is_o_norm_right] at B,

src/analysis/calculus/mean_value.lean

@@ -40,7 +40,7 @@ begin
     { apply continuous_on.prod,
       { refine continuous_norm.comp_continuous_on _,
         apply continuous_on.sub hf.continuous_on continuous_on_const },
-      { exact (continuous_mul continuous_const continuous_id).continuous_on } },
+      { exact (continuous.mul continuous_const continuous_id).continuous_on } },
     show is_closed K, from
       A.preimage_closed_of_closed is_closed_Icc (ordered_topology.is_closed_le' _) },
   have : k = 1,

src/analysis/calculus/tangent_cone.lean

@@ -100,7 +100,7 @@ begin
   have B : tendsto (λn, ∥c n • d n∥) at_top (𝓝 ∥y∥) :=
     (continuous_norm.tendsto _).comp hd,
   have C : tendsto (λn, ∥c n∥⁻¹ * ∥c n • d n∥) at_top (𝓝 (0 * ∥y∥)) :=
-    tendsto_mul A B,
+    tendsto.mul A B,
   rw zero_mul at C,
   have : {n | ∥c n∥⁻¹ * ∥c n • d n∥ = ∥d n∥} ∈ (@at_top ℕ _),
   { have : {n | 1 ≤ ∥c n∥} ∈ (@at_top ℕ _) :=
@@ -124,7 +124,7 @@ begin
   refine ⟨c, d, _, ctop, clim⟩,
   have : {n : ℕ | x + d n ∈ t} ∈ at_top,
   { have : tendsto (λn, x + d n) at_top (𝓝 (x + 0)) :=
-      tendsto_add tendsto_const_nhds (tangent_cone_at.lim_zero ctop clim),
+      tendsto.add tendsto_const_nhds (tangent_cone_at.lim_zero ctop clim),
     rw add_zero at this,
     exact mem_map.1 (this ht) },
   exact inter_mem_sets ds this

src/analysis/complex/exponential.lean

@@ -127,9 +127,9 @@ lemma continuous_cos : continuous cos :=
 differentiable_cos.continuous
 
 lemma continuous_tan : continuous (λ x : {x // cos x ≠ 0}, tan x) :=
-continuous_mul
+continuous.mul
   (continuous_sin.comp continuous_subtype_val)
-  (continuous_inv subtype.property
+  (continuous.inv subtype.property
     (continuous_cos.comp continuous_subtype_val))
 
 /-- The complex hyperbolic sine function is everywhere differentiable, with the derivative `sinh x`. -/
@@ -216,9 +216,8 @@ differentiable_cos.continuous
 
 lemma continuous_tan : continuous (λ x : {x // cos x ≠ 0}, tan x) :=
 by simp only [tan_eq_sin_div_cos]; exact
-continuous_mul
-  (continuous_sin.comp continuous_subtype_val)
-  (continuous_inv subtype.property
+  (continuous_sin.comp continuous_subtype_val).mul
+  (continuous.inv subtype.property
     (continuous_cos.comp continuous_subtype_val))
 
 lemma has_deriv_at_sinh (x : ℝ) : has_deriv_at sinh (cosh x) x :=
@@ -348,9 +347,9 @@ begin
     have : f₁ = λ h:{h:ℝ // 0 < h}, log x.1 + log h.1,
       ext h, rw ← log_mul x.2 h.2,
     simp only [this, log_mul x.2 zero_lt_one, log_one], exact
-      tendsto_add tendsto_const_nhds (tendsto.comp tendsto_log_one_zero continuous_at_subtype_val),
+      tendsto.add tendsto_const_nhds (tendsto.comp tendsto_log_one_zero continuous_at_subtype_val),
   have H2 : tendsto f₂ (𝓝 x) (𝓝 ⟨x.1⁻¹ * x.1, mul_pos (inv_pos x.2) x.2⟩),
-    rw tendsto_subtype_rng, exact tendsto_mul tendsto_const_nhds continuous_at_subtype_val,
+    rw tendsto_subtype_rng, exact tendsto.mul tendsto_const_nhds continuous_at_subtype_val,
   suffices h : tendsto (f₁ ∘ f₂) (𝓝 x) (𝓝 (log x.1)),
   begin
     convert h, ext y,
@@ -1701,22 +1700,22 @@ section prove_rpow_is_continuous
 lemma continuous_rpow_aux1 : continuous (λp : {p:ℝ×ℝ // 0 < p.1}, p.val.1 ^ p.val.2) :=
 suffices h : continuous (λ p : {p:ℝ×ℝ // 0 < p.1 }, exp (log p.val.1 * p.val.2)),
   by { convert h, ext p, rw rpow_def_of_pos p.2 },
-continuous_exp.comp $ continuous_mul
+continuous_exp.comp $ continuous.mul
   (show continuous ((λp:{p:ℝ//0 < p}, log (p.val)) ∘ (λp:{p:ℝ×ℝ//0<p.fst}, ⟨p.val.1, p.2⟩)), from
     continuous_log'.comp $ continuous_subtype_mk _ $ continuous_fst.comp continuous_subtype_val)
   (continuous_snd.comp $ continuous_subtype_val.comp continuous_id)
 
 lemma continuous_rpow_aux2 : continuous (λ p : {p:ℝ×ℝ // p.1 < 0}, p.val.1 ^ p.val.2) :=
 suffices h : continuous (λp:{p:ℝ×ℝ // p.1 < 0}, exp (log (-p.val.1) * p.val.2) * cos (p.val.2 * π)),
   by { convert h, ext p, rw [rpow_def_of_neg p.2] },
-continuous_mul
-  (continuous_exp.comp $ continuous_mul
+continuous.mul
+  (continuous_exp.comp $ continuous.mul
     (show continuous $ (λp:{p:ℝ//0<p},
             log (p.val))∘(λp:{p:ℝ×ℝ//p.1<0}, ⟨-p.val.1, neg_pos_of_neg p.2⟩),
-     from continuous_log'.comp $ continuous_subtype_mk _ $ continuous_neg'.comp $
+     from continuous_log'.comp $ continuous_subtype_mk _ $ continuous_neg.comp $
             continuous_fst.comp continuous_subtype_val)
     (continuous_snd.comp $ continuous_subtype_val.comp continuous_id))
-  (continuous_cos.comp $ continuous_mul
+  (continuous_cos.comp $ continuous.mul
     (continuous_snd.comp $ continuous_subtype_val.comp continuous_id) continuous_const)
 
 lemma continuous_at_rpow_of_ne_zero (hx : x ≠ 0) (y : ℝ) :

src/analysis/normed_space/banach.lean

@@ -158,13 +158,13 @@ begin
     tendsto.comp (hf.continuous.tendsto _) this,
   simp only [fsumeq] at L₁,
   have L₂ : tendsto (λn, y - (h^[n]) y) at_top (𝓝 (y - 0)),
-  { refine tendsto_sub tendsto_const_nhds _,
+  { refine tendsto.sub tendsto_const_nhds _,
     rw tendsto_iff_norm_tendsto_zero,
     simp only [sub_zero],
     refine squeeze_zero (λ_, norm_nonneg _) hnle _,
     have : 0 = 0 * ∥y∥, by rw zero_mul,
     rw this,
-    refine tendsto_mul _ tendsto_const_nhds,
+    refine tendsto.mul _ tendsto_const_nhds,
     exact tendsto_pow_at_top_nhds_0_of_lt_1 (by norm_num) (by norm_num) },
   have feq : f x = y - 0,
   { apply tendsto_nhds_unique _ L₁ L₂,

src/analysis/normed_space/basic.lean

@@ -337,12 +337,12 @@ instance normed_ring_top_monoid [normed_ring α] : topological_monoid α :=
       apply squeeze_zero,
       { intro, apply norm_nonneg },
       { simp only [this], intro, apply norm_add_le },
-      { rw ←zero_add (0 : ℝ), apply tendsto_add,
+      { rw ←zero_add (0 : ℝ), apply tendsto.add,
         { apply squeeze_zero,
           { intro, apply norm_nonneg },
           { intro t, show ∥t.fst * t.snd - t.fst * x.snd∥ ≤ ∥t.fst∥ * ∥t.snd - x.snd∥,
             rw ←mul_sub, apply norm_mul_le },
-          { rw ←mul_zero (∥x.fst∥), apply tendsto_mul,
+          { rw ←mul_zero (∥x.fst∥), apply tendsto.mul,
             { apply continuous_iff_continuous_at.1,
               apply continuous_norm.comp continuous_fst },
             { apply tendsto_iff_norm_tendsto_zero.1,
@@ -352,7 +352,7 @@ instance normed_ring_top_monoid [normed_ring α] : topological_monoid α :=
           { intro, apply norm_nonneg },
           { intro t, show ∥t.fst * x.snd - x.fst * x.snd∥ ≤ ∥t.fst - x.fst∥ * ∥x.snd∥,
             rw ←sub_mul, apply norm_mul_le },
-          { rw ←zero_mul (∥x.snd∥), apply tendsto_mul,
+          { rw ←zero_mul (∥x.snd∥), apply tendsto.mul,
             { apply tendsto_iff_norm_tendsto_zero.1,
               apply continuous_iff_continuous_at.1,
               apply continuous_fst },
@@ -533,16 +533,16 @@ begin
     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 := tendsto_mul limf' limg',
+    have lim1 := tendsto.mul limf' limg',
     simp only [zero_mul, sub_eq_add_neg] at lim1,
 
     have limg3 := tendsto_iff_norm_tendsto_zero.1 limg,
 
-    have lim2 := tendsto_mul (tendsto_const_nhds : tendsto _ _ (𝓝 ∥ s ∥)) limg3,
+    have lim2 := tendsto.mul (tendsto_const_nhds : tendsto _ _ (𝓝 ∥ s ∥)) limg3,
     simp only [sub_eq_add_neg, mul_zero] at lim2,
 
     rw [show (0:ℝ) = 0 + 0, by simp],
-    exact tendsto_add lim1 lim2  }
+    exact tendsto.add lim1 lim2  }
 end
 
 lemma tendsto_smul_const {g : γ → F} {e : filter γ} (s : α) {b : F} :

src/analysis/normed_space/bounded_linear_maps.lean

@@ -119,7 +119,7 @@ tendsto_iff_norm_tendsto_zero.2 $
       calc ∥f e - f x∥ = ∥hf.mk' f (e - x)∥ : by rw (hf.mk' _).map_sub e x; refl
                    ... ≤ M * ∥e - x∥        : hM (e - x))
     (suffices (λ (e : E), M * ∥e - x∥) →_{x} (M * 0), by simpa,
-      tendsto_mul tendsto_const_nhds (lim_norm _))
+      tendsto.mul tendsto_const_nhds (lim_norm _))
 
 lemma continuous (hf : is_bounded_linear_map 𝕜 f) : continuous f :=
 continuous_iff_continuous_at.2 $ λ _, hf.tendsto _

src/analysis/normed_space/operator_norm.lean

@@ -379,8 +379,8 @@ have eq : _ := uniformly_extend_of_ind h_e h_dense f.uniform_continuous,
   add :=
   begin
     refine is_closed_property2 h_dense (is_closed_eq _ _) _,
-    { exact cont.comp (_root_.continuous_add continuous_fst continuous_snd) },
-    { exact _root_.continuous_add (cont.comp continuous_fst) (cont.comp continuous_snd) },
+    { exact cont.comp (_root_.continuous.add continuous_fst continuous_snd) },
+    { exact _root_.continuous.add (cont.comp continuous_fst) (cont.comp continuous_snd) },
     { assume x y, rw ← e.map_add, simp only [eq], exact f.map_add _ _  },
   end,
   smul := λk,
@@ -419,7 +419,7 @@ begin
   { refine op_norm_le_bound ψ _ (is_closed_property h_dense (is_closed_le _ _) _),
     { exact mul_nonneg N0 (norm_nonneg _) },
     { exact continuous_norm.comp (cont ψ) },
-    { exact continuous_mul continuous_const continuous_norm },
+    { exact continuous.mul continuous_const continuous_norm },
     { assume x,
       rw eq,
       calc ∥f x∥ ≤ ∥f∥ * ∥x∥ : le_op_norm _ _

src/analysis/normed_space/real_inner_product.lean

@@ -250,7 +250,7 @@ begin
     have h : tendsto (λ n:ℕ, δ) at_top (𝓝 δ),
       exact tendsto_const_nhds,
     have h' : tendsto (λ n:ℕ, δ + 1 / (n + 1)) at_top (𝓝 δ),
-      convert tendsto_add h tendsto_one_div_add_at_top_nhds_0_nat, simp only [add_zero],
+      convert tendsto.add h tendsto_one_div_add_at_top_nhds_0_nat, simp only [add_zero],
     exact tendsto_of_tendsto_of_tendsto_of_le_of_le h h'
       (by { rw mem_at_top_sets, use 0, assume n hn, exact δ_le _ })
       (by { rw mem_at_top_sets, use 0, assume n hn, exact le_of_lt (hw _) }),
@@ -316,21 +316,21 @@ begin
     apply tendsto.comp,
     { convert continuous_sqrt.continuous_at, exact sqrt_zero.symm },
     have eq₁ : tendsto (λ (n : ℕ), 8 * δ * (1 / (n + 1))) at_top (𝓝 (0:ℝ)),
-      convert tendsto_mul (@tendsto_const_nhds _ _ _ (8 * δ) _) tendsto_one_div_add_at_top_nhds_0_nat,
+      convert tendsto.mul (@tendsto_const_nhds _ _ _ (8 * δ) _) tendsto_one_div_add_at_top_nhds_0_nat,
       simp only [mul_zero],
     have : tendsto (λ (n : ℕ), (4:ℝ) * (1 / (n + 1))) at_top (𝓝 (0:ℝ)),
-      convert tendsto_mul (@tendsto_const_nhds _ _ _ (4:ℝ) _) tendsto_one_div_add_at_top_nhds_0_nat,
+      convert tendsto.mul (@tendsto_const_nhds _ _ _ (4:ℝ) _) tendsto_one_div_add_at_top_nhds_0_nat,
       simp only [mul_zero],
     have eq₂ : tendsto (λ (n : ℕ), (4:ℝ) * (1 / (n + 1)) * (1 / (n + 1))) at_top (𝓝 (0:ℝ)),
-      convert tendsto_mul this tendsto_one_div_add_at_top_nhds_0_nat,
+      convert tendsto.mul this tendsto_one_div_add_at_top_nhds_0_nat,
       simp only [mul_zero],
-    convert tendsto_add eq₁ eq₂, simp only [add_zero],
+    convert tendsto.add eq₁ eq₂, simp only [add_zero],
   -- Step 3: By completeness of `K`, let `w : ℕ → K` converge to some `v : K`.
   -- Prove that it satisfies all requirements.
   rcases cauchy_seq_tendsto_of_is_complete h₁ (λ n, _) seq_is_cauchy with ⟨v, hv, w_tendsto⟩,
   use v, use hv,
   have h_cont : continuous (λ v, ∥u - v∥) :=
-    continuous.comp continuous_norm (continuous_sub continuous_const continuous_id),
+    continuous.comp continuous_norm (continuous.sub continuous_const continuous_id),
   have : tendsto (λ n, ∥u - w n∥) at_top (𝓝 ∥u - v∥),
     convert (tendsto.comp h_cont.continuous_at w_tendsto),
   exact tendsto_nhds_unique at_top_ne_bot this norm_tendsto,

src/analysis/specific_limits.lean

@@ -138,7 +138,7 @@ lemma tendsto_inverse_at_top_nhds_0_nat : tendsto (λ n : ℕ, (n : ℝ)⁻¹) a
 tendsto.comp tendsto_inverse_at_top_nhds_0 (tendsto_coe_nat_real_at_top_iff.2 tendsto_id)
 
 lemma tendsto_const_div_at_top_nhds_0_nat (C : ℝ) : tendsto (λ n : ℕ, C / n) at_top (𝓝 0) :=
-by simpa only [mul_zero] using tendsto_mul tendsto_const_nhds tendsto_inverse_at_top_nhds_0_nat
+by simpa only [mul_zero] using tendsto.mul tendsto_const_nhds tendsto_inverse_at_top_nhds_0_nat
 
 lemma tendsto_one_div_add_at_top_nhds_0_nat :
   tendsto (λ n : ℕ, 1 / ((n : ℝ) + 1)) at_top (𝓝 0) :=
@@ -151,8 +151,8 @@ have r ≠ 1, from ne_of_lt h₂,
 have r + -1 ≠ 0,
   by rw [←sub_eq_add_neg, ne, sub_eq_iff_eq_add]; simp; assumption,
 have tendsto (λn, (r ^ n - 1) * (r - 1)⁻¹) at_top (𝓝 ((0 - 1) * (r - 1)⁻¹)),
-  from tendsto_mul
-    (tendsto_sub (tendsto_pow_at_top_nhds_0_of_lt_1 h₁ h₂) tendsto_const_nhds) tendsto_const_nhds,
+  from tendsto.mul
+    (tendsto.sub (tendsto_pow_at_top_nhds_0_of_lt_1 h₁ h₂) tendsto_const_nhds) tendsto_const_nhds,
 have (λ n, (range n).sum (λ i, r ^ i)) = (λ n, geom_series r n) := rfl,
 (has_sum_iff_tendsto_nat_of_nonneg (pow_nonneg h₁) _).mpr $
   by simp [neg_inv, geom_sum, div_eq_mul_inv, *] at *