chore(topology/algebra/*): tendsto namespacing (#6528)

Correct a few lemmas which I noticed were namespaced as `tendsto.***` rather than `filter.tendsto.***`, and thus couldn't be used with projection notation.

Also use the projection notation, where now permitted.

[Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Search.20for.20all.20declarations.20in.20a.20namespace)



Co-authored-by: Patrick Massot <patrickmassot@free.fr>

src/analysis/special_functions/exp_log.lean

@@ -750,7 +750,7 @@ lemma tendsto_div_pow_mul_exp_add_at_top (b c : ℝ) (n : ℕ) (hb : 0 ≠ b) (h
 begin
   have H : ∀ d e, 0 < d → tendsto (λ (x:ℝ), x^n / (d * (exp x) + e)) at_top (𝓝 0),
   { intros b' c' h,
-    convert tendsto.inv_tendsto_at_top (tendsto_mul_exp_add_div_pow_at_top b' c' n h hn),
+    convert (tendsto_mul_exp_add_div_pow_at_top b' c' n h hn).inv_tendsto_at_top ,
     ext x,
     simpa only [pi.inv_apply] using inv_div.symm },
   cases lt_or_gt_of_ne hb,

src/analysis/special_functions/polynomials.lean

@@ -83,8 +83,7 @@ begin
   rw ←  nat_degree_lt_nat_degree_iff hP at hdeg,
   refine (is_equivalent_at_top_div P Q).symm.tendsto_nhds _,
   rw ← mul_zero,
-  refine tendsto.const_mul _ _,
-  apply tendsto_fpow_at_top_zero,
+  refine (tendsto_fpow_at_top_zero _).const_mul _,
   linarith
 end
 

src/analysis/special_functions/pow.lean

@@ -138,7 +138,7 @@ begin
     rw [log_zero, mul_zero],
     refine (has_strict_deriv_at_const _ 0).congr_of_eventually_eq _,
     exact (is_open_ne.eventually_mem h).mono (λ y hy, (zero_cpow hy).symm) },
-  { simpa only [cpow_def_of_ne_zero hx, mul_one] 
+  { simpa only [cpow_def_of_ne_zero hx, mul_one]
       using ((has_strict_deriv_at_id y).const_mul (log x)).cexp }
 end
 
@@ -516,10 +516,10 @@ end
 lemma mul_rpow {x y z : ℝ} (h : 0 ≤ x) (h₁ : 0 ≤ y) : (x*y)^z = x^z * y^z :=
 begin
   iterate 3 { rw real.rpow_def_of_nonneg }, split_ifs; simp * at *,
-  { have hx : 0 < x, 
+  { have hx : 0 < x,
     { cases lt_or_eq_of_le h with h₂ h₂, { exact h₂ },
       exfalso, apply h_2, exact eq.symm h₂ },
-    have hy : 0 < y, 
+    have hy : 0 < y,
     { cases lt_or_eq_of_le h₁ with h₂ h₂, { exact h₂ },
       exfalso, apply h_3, exact eq.symm h₂ },
     rw [log_mul (ne_of_gt hx) (ne_of_gt hy), add_mul, exp_add]},
@@ -957,7 +957,7 @@ end
 /-- The function `x ^ (-y)` tends to `0` at `+∞` for any positive real `y`. -/
 lemma tendsto_rpow_neg_at_top {y : ℝ} (hy : 0 < y) : tendsto (λ x : ℝ, x ^ (-y)) at_top (𝓝 0) :=
 tendsto.congr' (eventually_eq_of_mem (Ioi_mem_at_top 0) (λ x hx, (rpow_neg (le_of_lt hx) y).symm))
-  (tendsto.inv_tendsto_at_top (tendsto_rpow_at_top hy))
+  (tendsto_rpow_at_top hy).inv_tendsto_at_top
 
 /-- The function `x ^ (a / (b * x + c))` tends to `1` at `+∞`, for any real numbers `a`, `b`, and
 `c` such that `b` is nonzero. -/

src/analysis/special_functions/trigonometric.lean

@@ -2695,8 +2695,8 @@ begin
   { refine tendsto_inf.2 ⟨tendsto.mono_left _ inf_le_left, tendsto_principal.2 _⟩,
     exacts [continuous_cos.tendsto' x 0 hx,
       hx ▸ (has_deriv_at_cos _).eventually_ne (neg_ne_zero.2 A)] },
-  exact tendsto.mul_at_top (norm_pos_iff.2 A) continuous_sin.continuous_within_at.norm
-    (tendsto.inv_tendsto_zero $ tendsto_norm_nhds_within_zero.comp B),
+  exact continuous_sin.continuous_within_at.norm.mul_at_top (norm_pos_iff.2 A)
+    (tendsto_norm_nhds_within_zero.comp B).inv_tendsto_zero,
 end
 
 lemma tendsto_abs_tan_at_top (k : ℤ) :
@@ -3038,7 +3038,7 @@ end
 
 lemma tendsto_tan_pi_div_two : tendsto tan (𝓝[Iio (π/2)] (π/2)) at_top :=
 begin
-  convert (tendsto.inv_tendsto_zero tendsto_cos_pi_div_two).at_top_mul zero_lt_one
+  convert tendsto_cos_pi_div_two.inv_tendsto_zero.at_top_mul zero_lt_one
             tendsto_sin_pi_div_two,
   simp only [pi.inv_apply, ← div_eq_inv_mul, ← tan_eq_sin_div_cos]
 end
@@ -3056,7 +3056,7 @@ end
 
 lemma tendsto_tan_neg_pi_div_two : tendsto tan (𝓝[Ioi (-(π/2))] (-(π/2))) at_bot :=
 begin
-  convert (tendsto.inv_tendsto_zero tendsto_cos_neg_pi_div_two).at_top_mul_neg (by norm_num)
+  convert tendsto_cos_neg_pi_div_two.inv_tendsto_zero.at_top_mul_neg (by norm_num)
             tendsto_sin_neg_pi_div_two,
   simp only [pi.inv_apply, ← div_eq_inv_mul, ← tan_eq_sin_div_cos]
 end

src/data/real/pi.lean

@@ -189,8 +189,8 @@ begin
   --     constructed from `u` tends to `0` at `+∞`
   let u := λ k : ℕ, (k:nnreal) ^ (-1 / (2 * (k:ℝ) + 1)),
   have H : tendsto (λ k : ℕ, (1:ℝ) - (u k) + (u k) ^ (2 * (k:ℝ) + 1)) at_top (𝓝 0),
-  { convert (tendsto.const_add (1:ℝ) (((tendsto_rpow_div_mul_add (-1) 2 1 (by norm_num)).neg).add
-      tendsto_inv_at_top_zero)).comp tendsto_coe_nat_at_top_at_top,
+  { convert (((tendsto_rpow_div_mul_add (-1) 2 1 $ by norm_num).neg.const_add 1).add
+      tendsto_inv_at_top_zero).comp tendsto_coe_nat_at_top_at_top,
     { ext k,
       simp only [nnreal.coe_nat_cast, function.comp_app, nnreal.coe_rpow],
       rw [← rpow_mul (nat.cast_nonneg k) ((-1)/(2*(k:ℝ)+1)) (2*(k:ℝ)+1),

src/topology/algebra/monoid.lean

@@ -76,12 +76,12 @@ lemma filter.tendsto.mul {f : α → M} {g : α → M} {x : filter α} {a b : M}
 tendsto_mul.comp (hf.prod_mk_nhds hg)
 
 @[to_additive]
-lemma tendsto.const_mul (b : M) {c : M} {f : α → M} {l : filter α}
+lemma filter.tendsto.const_mul (b : M) {c : M} {f : α → M} {l : filter α}
   (h : tendsto (λ (k:α), f k) l (𝓝 c)) : tendsto (λ (k:α), b * f k) l (𝓝 (b * c)) :=
 tendsto_const_nhds.mul h
 
 @[to_additive]
-lemma tendsto.mul_const (b : M) {c : M} {f : α → M} {l : filter α}
+lemma filter.tendsto.mul_const (b : M) {c : M} {f : α → M} {l : filter α}
   (h : tendsto (λ (k:α), f k) l (𝓝 c)) : tendsto (λ (k:α), f k * b) l (𝓝 (c * b)) :=
 h.mul tendsto_const_nhds
 

src/topology/algebra/ordered.lean

@@ -568,11 +568,13 @@ lemma continuous_min : continuous (λ p : α × α, min p.1 p.2) := continuous_f
 
 lemma continuous_max : continuous (λ p : α × α, max p.1 p.2) := continuous_fst.max continuous_snd
 
-lemma tendsto.max {b : filter β} {a₁ a₂ : α} (hf : tendsto f b (𝓝 a₁)) (hg : tendsto g b (𝓝 a₂)) :
+lemma filter.tendsto.max {b : filter β} {a₁ a₂ : α} (hf : tendsto f b (𝓝 a₁))
+  (hg : tendsto g b (𝓝 a₂)) :
   tendsto (λb, max (f b) (g b)) b (𝓝 (max a₁ a₂)) :=
 (continuous_max.tendsto (a₁, a₂)).comp (hf.prod_mk_nhds hg)
 
-lemma tendsto.min {b : filter β} {a₁ a₂ : α} (hf : tendsto f b (𝓝 a₁)) (hg : tendsto g b (𝓝 a₂)) :
+lemma filter.tendsto.min {b : filter β} {a₁ a₂ : α} (hf : tendsto f b (𝓝 a₁))
+  (hg : tendsto g b (𝓝 a₂)) :
   tendsto (λb, min (f b) (g b)) b (𝓝 (min a₁ a₂)) :=
 (continuous_min.tendsto (a₁, a₂)).comp (hf.prod_mk_nhds hg)
 
@@ -1599,16 +1601,18 @@ lemma filter.tendsto.div_at_top [has_continuous_mul α] {f g : β → α} {l : f
   (h : tendsto f l (𝓝 a)) (hg : tendsto g l at_top) : tendsto (λ x, f x / g x) l (𝓝 0) :=
 by { simp only [div_eq_mul_inv], exact mul_zero a ▸ h.mul (tendsto_inv_at_top_zero.comp hg) }
 
-lemma tendsto.inv_tendsto_at_top (h : tendsto f l at_top) : tendsto (f⁻¹) l (𝓝 0) :=
+lemma filter.tendsto.inv_tendsto_at_top (h : tendsto f l at_top) : tendsto (f⁻¹) l (𝓝 0) :=
 tendsto_inv_at_top_zero.comp h
 
-lemma tendsto.inv_tendsto_zero (h : tendsto f l (𝓝[set.Ioi 0] 0)) : tendsto (f⁻¹) l at_top :=
+lemma filter.tendsto.inv_tendsto_zero (h : tendsto f l (𝓝[set.Ioi 0] 0)) :
+  tendsto (f⁻¹) l at_top :=
 tendsto_inv_zero_at_top.comp h
 
 /-- The function `x^(-n)` tends to `0` at `+∞` for any positive natural `n`.
 A version for positive real powers exists as `tendsto_rpow_neg_at_top`. -/
 lemma tendsto_pow_neg_at_top {n : ℕ} (hn : 1 ≤ n) : tendsto (λ x : α, x ^ (-(n:ℤ))) at_top (𝓝 0) :=
-tendsto.congr (λ x, (fpow_neg x n).symm) (tendsto.inv_tendsto_at_top (tendsto_pow_at_top hn))
+tendsto.congr (λ x, (fpow_neg x n).symm)
+  (filter.tendsto.inv_tendsto_at_top (tendsto_pow_at_top hn))
 
 lemma tendsto_fpow_at_top_zero {n : ℤ} (hn : n < 0) :
   tendsto (λ x : α, x^n) at_top (𝓝 0) :=