refactor(topology/algebra): use dot notation in tendsto.add and frien…

…ds (#1765)

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_const_nhds.add (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,
+    L1.add 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] },
@@ -888,7 +888,7 @@ 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 },
+    rw ← sub_self x, exact tendsto_id.sub tendsto_const_nhds },
   have := tendsto.add this tendsto_const_nhds,
   rw zero_add (f x) at this,
   exact this.congr (by simp)

src/analysis/calculus/tangent_cone.lean

@@ -99,8 +99,7 @@ begin
     tendsto_inverse_at_top_nhds_0.comp hc,
   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,
+  have C : tendsto (λn, ∥c n∥⁻¹ * ∥c n • d n∥) at_top (𝓝 (0 * ∥y∥)) := A.mul 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 +123,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_const_nhds.add (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

@@ -344,10 +344,10 @@ begin
   have H1 : tendsto f₁ (𝓝 ⟨1, zero_lt_one⟩) (𝓝 (log (x.1*1))),
     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),
+    simp only [this, log_mul x.2 zero_lt_one, log_one],
+    exact tendsto_const_nhds.add (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_const_nhds.mul continuous_at_subtype_val,
   suffices h : tendsto (f₁ ∘ f₂) (𝓝 x) (𝓝 (log x.1)),
   begin
     convert h, ext y,

src/analysis/normed_space/banach.lean

@@ -158,7 +158,7 @@ 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_const_nhds.sub _,
     rw tendsto_iff_norm_tendsto_zero,
     simp only [sub_zero],
     refine squeeze_zero (λ_, norm_nonneg _) hnle _,

src/analysis/normed_space/basic.lean

@@ -539,16 +539,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 := 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.mul (tendsto_const_nhds : tendsto _ _ (𝓝 ∥ s ∥)) limg3,
+    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 tendsto.add lim1 lim2  }
+    exact lim1.add 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_const_nhds.mul (lim_norm _))
 
 lemma continuous (hf : is_bounded_linear_map 𝕜 f) : continuous f :=
 continuous_iff_continuous_at.2 $ λ _, hf.tendsto _

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 h.add 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,15 +316,15 @@ 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_const_nhds _ _ _ (8 * δ) _).mul 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_const_nhds _ _ _ (4:ℝ) _).mul 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 this.mul tendsto_one_div_add_at_top_nhds_0_nat,
       simp only [mul_zero],
-    convert tendsto.add eq₁ eq₂, simp only [add_zero],
+    convert eq₁.add 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⟩,

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_const_nhds.mul 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,7 @@ 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_pow_at_top_nhds_0_of_lt_1 h₁ h₂).sub tendsto_const_nhds).mul 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 *

src/data/padics/hensel.lean

@@ -302,7 +302,7 @@ private lemma newton_seq_dist_to_a : ∀ n : ℕ, 0 < n → ∥newton_seq n - a
 private lemma bound' : tendsto (λ n : ℕ, ∥F.derivative.eval a∥ * T^(2^n)) at_top (𝓝 0) :=
 begin
   rw ←mul_zero (∥F.derivative.eval a∥),
-  exact tendsto.mul (tendsto_const_nhds)
+  exact tendsto_const_nhds.mul
                     (tendsto.comp
                       (tendsto_pow_at_top_nhds_0_of_lt_1 (norm_nonneg _) (T_lt_one hnorm))
                       (tendsto_pow_at_top_at_top_of_gt_1_nat (by norm_num)))
@@ -364,7 +364,7 @@ tendsto.congr'
 private lemma newton_seq_dist_tendsto' :
   tendsto (λ n, ∥newton_cau_seq n - a∥) at_top (𝓝 ∥soln - a∥) :=
 tendsto.comp (continuous_iff_continuous_at.1 continuous_norm _)
-             (tendsto.sub (tendsto_limit _) tendsto_const_nhds)
+             ((tendsto_limit _).sub tendsto_const_nhds)
 
 
 private lemma soln_dist_to_a : ∥soln - a∥ = ∥F.eval a∥ / ∥F.derivative.eval a∥ :=

src/data/real/hyperreal.lean

@@ -69,7 +69,7 @@ end
 
 lemma neg_lt_of_tendsto_zero_of_pos {f : ℕ → ℝ} (hf : tendsto f at_top (𝓝 0)) :
   ∀ {r : ℝ}, r > 0 → (-r : ℝ*) < of_seq f :=
-λ r hr, have hg : _ := tendsto.neg hf,
+λ r hr, have hg : _ := hf.neg,
 neg_lt_of_neg_lt (by rw [neg_zero] at hg; exact lt_of_tendsto_zero_of_pos hg hr)
 
 lemma gt_of_tendsto_zero_of_neg {f : ℕ → ℝ} (hf : tendsto f at_top (𝓝 0)) :
@@ -649,7 +649,7 @@ end
 theorem is_st_of_tendsto {f : ℕ → ℝ} {r : ℝ} (hf : tendsto f at_top (𝓝 r)) :
   is_st (of_seq f) r :=
 have hg : tendsto (λ n, f n - r) at_top (𝓝 0) :=
-  (sub_self r) ▸ (tendsto.sub hf tendsto_const_nhds),
+  (sub_self r) ▸ (hf.sub tendsto_const_nhds),
 by rw [←(zero_add r), ←(sub_add_cancel f (λ n, r))];
 exact is_st_add (infinitesimal_of_tendsto_zero hg) (is_st_refl_real r)
 

src/measure_theory/decomposition.lean

@@ -152,7 +152,7 @@ begin
   have γ_le_d_s : γ ≤ d s,
   { have hγ : tendsto (λm:ℕ, γ - 2 * (1/2)^m) at_top (𝓝 γ),
     { suffices : tendsto (λm:ℕ, γ - 2 * (1/2)^m) at_top (𝓝 (γ - 2 * 0)), { simpa },
-      exact (tendsto.sub tendsto_const_nhds $ tendsto.mul tendsto_const_nhds $
+      exact (tendsto_const_nhds.sub $ tendsto_const_nhds.mul $
         tendsto_pow_at_top_nhds_0_of_lt_1
           (le_of_lt $ half_pos $ zero_lt_one) (half_lt_self zero_lt_one)) },
     have hd : tendsto (λm, d (⋂n, f m n)) at_top (𝓝 (d (⋃ m, ⋂ n, f m n))),

src/topology/algebra/group.lean

@@ -52,7 +52,7 @@ lemma continuous_on.inv [topological_group α] [topological_space β] {f : β 
 continuous_inv.comp_continuous_on hf
 
 @[to_additive]
-lemma tendsto.inv [topological_group α] {f : β → α} {x : filter β} {a : α}
+lemma filter.tendsto.inv [topological_group α] {f : β → α} {x : filter β} {a : α}
   (hf : tendsto f x (𝓝 a)) : tendsto (λx, (f x)⁻¹) x (𝓝 a⁻¹) :=
 tendsto.comp (continuous_iff_continuous_at.mp (topological_group.continuous_inv α) a) hf
 
@@ -116,7 +116,7 @@ lemma exists_nhds_split_inv [topological_group α] {s : set α} (hs : s ∈ 𝓝
   ∃ V ∈ 𝓝 (1 : α), ∀ v w ∈ V, v * w⁻¹ ∈ s :=
 begin
   have : tendsto (λa:α×α, a.1 * (a.2)⁻¹) ((𝓝 (1:α)).prod (𝓝 (1:α))) (𝓝 1),
-  { simpa using tendsto.mul (@tendsto_fst α α (𝓝 1) (𝓝 1)) (tendsto.inv tendsto_snd) },
+  { simpa using (@tendsto_fst α α (𝓝 1) (𝓝 1)).mul tendsto_snd.inv },
   have : ((λa:α×α, a.1 * (a.2)⁻¹) ⁻¹' s) ∈ (𝓝 (1:α)).prod (𝓝 (1:α)) :=
     this (by simpa using hs),
   rcases mem_prod_iff.1 this with ⟨V₁, H₁, V₂, H₂, H⟩,
@@ -140,7 +140,7 @@ variable (α)
 lemma nhds_one_symm [topological_group α] : comap (λr:α, r⁻¹) (𝓝 (1 : α)) = 𝓝 (1 : α) :=
 begin
   have lim : tendsto (λr:α, r⁻¹) (𝓝 1) (𝓝 1),
-  { simpa using tendsto.inv (@tendsto_id α (𝓝 1)) },
+  { simpa using (@tendsto_id α (𝓝 1)).inv },
   refine comap_eq_of_inverse _ _ lim lim,
   { funext x, simp },
 end
@@ -153,9 +153,9 @@ begin
   refine comap_eq_of_inverse (λy:α, y * x) _ _ _,
   { funext x; simp },
   { suffices : tendsto (λy:α, y * x⁻¹) (𝓝 x) (𝓝 (x * x⁻¹)), { simpa },
-    exact tendsto.mul tendsto_id tendsto_const_nhds },
+    exact tendsto_id.mul tendsto_const_nhds },
   { suffices : tendsto (λy:α, y * x) (𝓝 1) (𝓝 (1 * x)), { simpa },
-    exact tendsto.mul tendsto_id tendsto_const_nhds }
+    exact tendsto_id.mul tendsto_const_nhds }
 end
 
 @[to_additive]
@@ -237,9 +237,9 @@ lemma continuous_on.sub [topological_add_group α] [topological_space β] {f : 
   (hf : continuous_on f s) (hg : continuous_on g s) : continuous_on (λx, f x - g x) s :=
 continuous_sub.comp_continuous_on (hf.prod hg)
 
-lemma tendsto.sub [topological_add_group α] {f : β → α} {g : β → α} {x : filter β} {a b : α}
+lemma filter.tendsto.sub [topological_add_group α] {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)) :=
-by simp; exact tendsto.add hf (tendsto.neg hg)
+by simp; exact hf.add hg.neg
 
 lemma nhds_translation [topological_add_group α] (x : α) : comap (λy:α, y - x) (𝓝 0) = 𝓝 x :=
 nhds_translation_add_neg x

src/topology/algebra/infinite_sum.lean

@@ -129,7 +129,7 @@ lemma tendsto_sum_nat_of_has_sum {f : ℕ → α} (h : has_sum f a) :
 variable [topological_add_monoid α]
 
 lemma has_sum_add (hf : has_sum f a) (hg : has_sum g b) : has_sum (λb, f b + g b) (a + b) :=
-by simp [has_sum, sum_add_distrib]; exact tendsto.add hf hg
+by simp [has_sum, sum_add_distrib]; exact hf.add hg
 
 lemma summable_add (hf : summable f) (hg : summable g) : summable (λb, f b + g b) :=
 summable_spec $ has_sum_add (has_sum_tsum hf)(has_sum_tsum hg)

src/topology/algebra/monoid.lean

@@ -68,7 +68,7 @@ lemma tendsto_mul {a b : α} : tendsto (λp:α×α, p.fst * p.snd) (𝓝 (a, b))
 continuous_iff_continuous_at.mp (topological_monoid.continuous_mul α) (a, b)
 
 @[to_additive]
-lemma tendsto.mul {f : β → α} {g : β → α} {x : filter β} {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)
@@ -81,8 +81,7 @@ lemma tendsto_list_prod {f : γ → β → α} {x : filter β} {a : γ → α} :
 | (f :: l) h :=
   begin
     simp,
-    exact tendsto.mul
-      (h f (list.mem_cons_self _ _))
+    exact (h f (list.mem_cons_self _ _)).mul
       (tendsto_list_prod l (assume c hc, h c (list.mem_cons_of_mem _ hc)))
   end
 

src/topology/algebra/uniform_group.lean

@@ -197,7 +197,7 @@ have tendsto
     ((λp:(G×G), p.1 - p.2) ∘ (λp:(G×G)×(G×G), (p.1.2 - p.1.1, p.2.2 - p.2.1)))
     (comap (λp:(G×G)×(G×G), (p.1.2 - p.1.1, p.2.2 - p.2.1)) ((𝓝 0).prod (𝓝 0)))
     (𝓝 (0 - 0)) :=
-  (tendsto.sub tendsto_fst tendsto_snd).comp tendsto_comap,
+  (tendsto_fst.sub tendsto_snd).comp tendsto_comap,
 begin
   constructor,
   rw [uniform_continuous, uniformity_prod_eq_prod, tendsto_map'_iff,

src/topology/instances/nnreal.lean

@@ -76,7 +76,7 @@ tendsto.comp (continuous_iff_continuous_at.1 continuous_of_real _) h
 lemma tendsto.sub {f : filter α} {m n : α → nnreal} {r p : nnreal}
   (hm : tendsto m f (𝓝 r)) (hn : tendsto n f (𝓝 p)) :
   tendsto (λa, m a - n a) f (𝓝 (r - p)) :=
-tendsto_of_real $ tendsto.sub (tendsto_coe.2 hm) (tendsto_coe.2 hn)
+tendsto_of_real $ (tendsto_coe.2 hm).sub (tendsto_coe.2 hn)
 
 lemma continuous_sub : continuous (λp:nnreal×nnreal, p.1 - p.2) :=
 continuous_subtype_mk _ $

src/topology/instances/real.lean

@@ -397,7 +397,7 @@ lemma real.intermediate_value' {f : ℝ → ℝ} {a b t : ℝ}
   (hf : ∀ x, a ≤ x → x ≤ b → tendsto f (𝓝 x) (𝓝 (f x)))
   (ha : t ≤ f a) (hb : f b ≤ t) (hab : a ≤ b) : ∃ x : ℝ, a ≤ x ∧ x ≤ b ∧ f x = t :=
 let ⟨x, hx₁, hx₂, hx₃⟩ := @real.intermediate_value
-  (λ x, - f x) a b (-t) (λ x hax hxb, tendsto.neg (hf x hax hxb))
+  (λ x, - f x) a b (-t) (λ x hax hxb, (hf x hax hxb).neg)
   (neg_le_neg ha) (neg_le_neg hb) hab in
 ⟨x, hx₁, hx₂, neg_inj hx₃⟩
 

src/topology/metric_space/gromov_hausdorff_realized.lean

@@ -241,7 +241,7 @@ begin
     exact ⟨candidates_nonneg hf, candidates_le_max_var hf⟩ },
   { refine equicontinuous_of_continuity_modulus (λt, 2 * max_var α β * t) _ _ _,
     { have : tendsto (λ (t : ℝ), 2 * (max_var α β : ℝ) * t) (𝓝 0) (𝓝 (2 * max_var α β * 0)) :=
-        tendsto.mul tendsto_const_nhds tendsto_id,
+        tendsto_const_nhds.mul tendsto_id,
       simpa using this },
     { assume x y f hf,
       exact candidates_lipschitz hf _ _ } }