chore(InfiniteSum): use dot notation (#8358)

## Rename

- `summable_of_norm_bounded` -> `Summable.of_norm_bounded`;
- `summable_of_norm_bounded_eventually` -> `Summable.of_norm_bounded_eventually`;
- `summable_of_nnnorm_bounded` -> `Summable.of_nnnorm_bounded`;
- `summable_of_summable_norm` -> `Summable.of_norm`;
- `summable_of_summable_nnnorm` -> `Summable.of_nnnorm`;

## New lemmas

- `Summable.of_norm_bounded_eventually_nat`
- `Summable.norm`

## Misc changes

- Golf a few proofs.

Mathlib/Analysis/Analytic/Basic.lean

@@ -279,14 +279,14 @@ theorem not_summable_norm_of_radius_lt_nnnorm (p : FormalMultilinearSeries 𝕜
 theorem summable_norm_mul_pow (p : FormalMultilinearSeries 𝕜 E F) {r : ℝ≥0} (h : ↑r < p.radius) :
     Summable fun n : ℕ => ‖p n‖ * (r : ℝ) ^ n := by
   obtain ⟨a, ha : a ∈ Ioo (0 : ℝ) 1, C, - : 0 < C, hp⟩ := p.norm_mul_pow_le_mul_pow_of_lt_radius h
-  exact summable_of_nonneg_of_le (fun n => mul_nonneg (norm_nonneg _) (pow_nonneg r.coe_nonneg _))
+  exact .of_nonneg_of_le (fun n => mul_nonneg (norm_nonneg _) (pow_nonneg r.coe_nonneg _))
     hp ((summable_geometric_of_lt_1 ha.1.le ha.2).mul_left _)
 #align formal_multilinear_series.summable_norm_mul_pow FormalMultilinearSeries.summable_norm_mul_pow
 
 theorem summable_norm_apply (p : FormalMultilinearSeries 𝕜 E F) {x : E}
     (hx : x ∈ EMetric.ball (0 : E) p.radius) : Summable fun n : ℕ => ‖p n fun _ => x‖ := by
   rw [mem_emetric_ball_zero_iff] at hx
-  refine' summable_of_nonneg_of_le
+  refine' .of_nonneg_of_le
     (fun _ => norm_nonneg _) (fun n => ((p n).le_op_norm _).trans_eq _) (p.summable_norm_mul_pow hx)
   simp
 #align formal_multilinear_series.summable_norm_apply FormalMultilinearSeries.summable_norm_apply
@@ -300,7 +300,7 @@ theorem summable_nnnorm_mul_pow (p : FormalMultilinearSeries 𝕜 E F) {r : ℝ
 
 protected theorem summable [CompleteSpace F] (p : FormalMultilinearSeries 𝕜 E F) {x : E}
     (hx : x ∈ EMetric.ball (0 : E) p.radius) : Summable fun n : ℕ => p n fun _ => x :=
-  summable_of_summable_norm (p.summable_norm_apply hx)
+  (p.summable_norm_apply hx).of_norm
 #align formal_multilinear_series.summable FormalMultilinearSeries.summable
 
 theorem radius_eq_top_of_summable_norm (p : FormalMultilinearSeries 𝕜 E F)
@@ -314,7 +314,7 @@ theorem radius_eq_top_iff_summable_norm (p : FormalMultilinearSeries 𝕜 E F) :
   · intro h r
     obtain ⟨a, ha : a ∈ Ioo (0 : ℝ) 1, C, - : 0 < C, hp⟩ := p.norm_mul_pow_le_mul_pow_of_lt_radius
       (show (r : ℝ≥0∞) < p.radius from h.symm ▸ ENNReal.coe_lt_top)
-    refine' summable_of_norm_bounded
+    refine' .of_norm_bounded
       (fun n => (C : ℝ) * a ^ n) ((summable_geometric_of_lt_1 ha.1.le ha.2).mul_left _) fun n => _
     specialize hp n
     rwa [Real.norm_of_nonneg (mul_nonneg (norm_nonneg _) (pow_nonneg r.coe_nonneg n))]
@@ -1312,7 +1312,7 @@ theorem changeOrigin_eval (h : (‖x‖₊ + ‖y‖₊ : ℝ≥0∞) < p.radius
   set f : (Σk l : ℕ, { s : Finset (Fin (k + l)) // s.card = l }) → F := fun s =>
     p.changeOriginSeriesTerm s.1 s.2.1 s.2.2 s.2.2.2 (fun _ => x) fun _ => y
   have hsf : Summable f := by
-    refine' summable_of_nnnorm_bounded _ (p.changeOriginSeries_summable_aux₁ h) _
+    refine' .of_nnnorm_bounded _ (p.changeOriginSeries_summable_aux₁ h) _
     rintro ⟨k, l, s, hs⟩
     dsimp only [Subtype.coe_mk]
     exact p.nnnorm_changeOriginSeriesTerm_apply_le _ _ _ _ _ _
@@ -1325,7 +1325,7 @@ theorem changeOrigin_eval (h : (‖x‖₊ + ‖y‖₊ : ℝ≥0∞) < p.radius
       refine' HasSum.sigma_of_hasSum this (fun l => _) _
       · simp only [changeOriginSeries, ContinuousMultilinearMap.sum_apply]
         apply hasSum_fintype
-      · refine' summable_of_nnnorm_bounded _
+      · refine' .of_nnnorm_bounded _
           (p.changeOriginSeries_summable_aux₂ (mem_emetric_ball_zero_iff.1 x_mem_ball) k) fun s => _
         refine' (ContinuousMultilinearMap.le_op_nnnorm _ _).trans_eq _
         simp

Mathlib/Analysis/Asymptotics/Asymptotics.lean

@@ -2218,7 +2218,7 @@ open Asymptotics
 theorem summable_of_isBigO {ι E} [NormedAddCommGroup E] [CompleteSpace E] {f : ι → E} {g : ι → ℝ}
     (hg : Summable g) (h : f =O[cofinite] g) : Summable f :=
   let ⟨C, hC⟩ := h.isBigOWith
-  summable_of_norm_bounded_eventually (fun x => C * ‖g x‖) (hg.abs.mul_left _) hC.bound
+  .of_norm_bounded_eventually (fun x => C * ‖g x‖) (hg.abs.mul_left _) hC.bound
 set_option linter.uppercaseLean3 false in
 #align summable_of_is_O summable_of_isBigO
 

Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean

@@ -157,9 +157,8 @@ theorem IsOpen.exists_smooth_support_eq {s : Set E} (hs : IsOpen s) :
       _ ≤ M⁻¹ * δ n * M := (mul_le_mul_of_nonneg_left ((hR i x).trans (IR i hi)) (by positivity))
       _ = δ n := by field_simp
   choose r rpos hr using this
-  have S : ∀ x, Summable fun n => (r n • g n) x := by
-    intro x
-    refine' summable_of_nnnorm_bounded _ δc.summable fun n => _
+  have S : ∀ x, Summable fun n => (r n • g n) x := fun x ↦ by
+    refine' .of_nnnorm_bounded _ δc.summable fun n => _
     rw [← NNReal.coe_le_coe, coe_nnnorm]
     simpa only [norm_iteratedFDeriv_zero] using hr n 0 (zero_le n) x
   refine' ⟨fun x => ∑' n, (r n • g n) x, _, _, _⟩

Mathlib/Analysis/Calculus/Series.lean

@@ -43,8 +43,8 @@ theorem tendstoUniformlyOn_tsum {f : α → β → F} (hu : Summable u) {s : Set
   refine' tendstoUniformlyOn_iff.2 fun ε εpos => _
   filter_upwards [(tendsto_order.1 (tendsto_tsum_compl_atTop_zero u)).2 _ εpos] with t ht x hx
   have A : Summable fun n => ‖f n x‖ :=
-    summable_of_nonneg_of_le (fun n => norm_nonneg _) (fun n => hfu n x hx) hu
-  rw [dist_eq_norm, ← sum_add_tsum_subtype_compl (summable_of_summable_norm A) t, add_sub_cancel']
+    .of_nonneg_of_le (fun _ ↦ norm_nonneg _) (fun n => hfu n x hx) hu
+  rw [dist_eq_norm, ← sum_add_tsum_subtype_compl A.of_norm t, add_sub_cancel']
   apply lt_of_le_of_lt _ ht
   apply (norm_tsum_le_tsum_norm (A.subtype _)).trans
   exact tsum_le_tsum (fun n => hfu _ _ hx) (A.subtype _) (hu.subtype _)
@@ -202,7 +202,7 @@ theorem iteratedFDeriv_tsum (hf : ∀ i, ContDiff 𝕜 N (f i))
     exact (continuousMultilinearCurryFin0 𝕜 E F).symm.toContinuousLinearEquiv.map_tsum
   · have h'k : (k : ℕ∞) < N := lt_of_lt_of_le (WithTop.coe_lt_coe.2 (Nat.lt_succ_self _)) hk
     have A : Summable fun n => iteratedFDeriv 𝕜 k (f n) 0 :=
-      summable_of_norm_bounded (v k) (hv k h'k.le) fun n => h'f k n 0 h'k.le
+      .of_norm_bounded (v k) (hv k h'k.le) fun n => h'f k n 0 h'k.le
     simp_rw [iteratedFDeriv_succ_eq_comp_left, IH h'k.le]
     rw [fderiv_tsum (hv _ hk) (fun n => (hf n).differentiable_iteratedFDeriv h'k) _ A]
     · ext1 x
@@ -279,7 +279,7 @@ theorem contDiff_tsum_of_eventually (hf : ∀ i, ContDiff 𝕜 N (f i))
         fun x => ∑' i : { i // i ∉ T }, f i x := by
       ext1 x
       refine' (sum_add_tsum_subtype_compl _ T).symm
-      refine' summable_of_norm_bounded_eventually _ (hv 0 (zero_le _)) _
+      refine' .of_norm_bounded_eventually _ (hv 0 (zero_le _)) _
       filter_upwards [h'f 0 (zero_le _)] with i hi
       simpa only [norm_iteratedFDeriv_zero] using hi x
     rw [this]

Mathlib/Analysis/Fourier/AddCircle.lean

@@ -504,9 +504,9 @@ theorem hasSum_fourier_series_of_summable (h : Summable (fourierCoeff f)) :
     HasSum (fun i => fourierCoeff f i • fourier i) f := by
   have sum_L2 := hasSum_fourier_series_L2 (toLp (E := ℂ) 2 haarAddCircle ℂ f)
   simp_rw [fourierCoeff_toLp] at sum_L2
-  refine' ContinuousMap.hasSum_of_hasSum_Lp (summable_of_summable_norm _) sum_L2
-  simp_rw [norm_smul, fourier_norm, mul_one, summable_norm_iff]
-  exact h
+  refine ContinuousMap.hasSum_of_hasSum_Lp (.of_norm ?_) sum_L2
+  simp_rw [norm_smul, fourier_norm, mul_one]
+  exact h.norm
 #align has_sum_fourier_series_of_summable hasSum_fourier_series_of_summable
 
 /-- If the sequence of Fourier coefficients of `f` is summable, then the Fourier series of `f`

Mathlib/Analysis/InnerProductSpace/l2Space.lean

@@ -111,7 +111,7 @@ namespace lp
 
 theorem summable_inner (f g : lp G 2) : Summable fun i => ⟪f i, g i⟫ := by
   -- Apply the Direct Comparison Test, comparing with ∑' i, ‖f i‖ * ‖g i‖ (summable by Hölder)
-  refine' summable_of_norm_bounded (fun i => ‖f i‖ * ‖g i‖) (lp.summable_mul _ f g) _
+  refine' .of_norm_bounded (fun i => ‖f i‖ * ‖g i‖) (lp.summable_mul _ f g) _
   · rw [Real.isConjugateExponent_iff] <;> norm_num
   intro i
   -- Then apply Cauchy-Schwarz pointwise

Mathlib/Analysis/Normed/Field/InfiniteSum.lean

@@ -36,24 +36,23 @@ theorem Summable.mul_of_nonneg {f : ι → ℝ} {g : ι' → ℝ} (hf : Summable
 
 theorem Summable.mul_norm {f : ι → R} {g : ι' → R} (hf : Summable fun x => ‖f x‖)
     (hg : Summable fun x => ‖g x‖) : Summable fun x : ι × ι' => ‖f x.1 * g x.2‖ :=
-  summable_of_nonneg_of_le (fun x => norm_nonneg (f x.1 * g x.2))
+  .of_nonneg_of_le (fun _ ↦ norm_nonneg _)
     (fun x => norm_mul_le (f x.1) (g x.2))
     (hf.mul_of_nonneg hg (fun x => norm_nonneg <| f x) fun x => norm_nonneg <| g x : _)
 #align summable.mul_norm Summable.mul_norm
 
 theorem summable_mul_of_summable_norm [CompleteSpace R] {f : ι → R} {g : ι' → R}
     (hf : Summable fun x => ‖f x‖) (hg : Summable fun x => ‖g x‖) :
     Summable fun x : ι × ι' => f x.1 * g x.2 :=
-  summable_of_summable_norm (hf.mul_norm hg)
+  (hf.mul_norm hg).of_norm
 #align summable_mul_of_summable_norm summable_mul_of_summable_norm
 
 /-- Product of two infinites sums indexed by arbitrary types.
     See also `tsum_mul_tsum` if `f` and `g` are *not* absolutely summable. -/
 theorem tsum_mul_tsum_of_summable_norm [CompleteSpace R] {f : ι → R} {g : ι' → R}
     (hf : Summable fun x => ‖f x‖) (hg : Summable fun x => ‖g x‖) :
     ((∑' x, f x) * ∑' y, g y) = ∑' z : ι × ι', f z.1 * g z.2 :=
-  tsum_mul_tsum (summable_of_summable_norm hf) (summable_of_summable_norm hg)
-    (summable_mul_of_summable_norm hf hg)
+  tsum_mul_tsum hf.of_norm hg.of_norm (summable_mul_of_summable_norm hf hg)
 #align tsum_mul_tsum_of_summable_norm tsum_mul_tsum_of_summable_norm
 
 /-! ### `ℕ`-indexed families (Cauchy product)
@@ -77,8 +76,7 @@ theorem summable_norm_sum_mul_antidiagonal_of_summable_norm {f g : ℕ → R}
   have :=
     summable_sum_mul_antidiagonal_of_summable_mul
       (Summable.mul_of_nonneg hf hg (fun _ => norm_nonneg _) fun _ => norm_nonneg _)
-  refine' summable_of_nonneg_of_le (fun _ => norm_nonneg _) _ this
-  intro n
+  refine this.of_nonneg_of_le (fun _ => norm_nonneg _) (fun n ↦ ?_)
   calc
     ‖∑ kl in antidiagonal n, f kl.1 * g kl.2‖ ≤ ∑ kl in antidiagonal n, ‖f kl.1 * g kl.2‖ :=
       norm_sum_le _ _
@@ -92,8 +90,7 @@ theorem summable_norm_sum_mul_antidiagonal_of_summable_norm {f g : ℕ → R}
 theorem tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm [CompleteSpace R] {f g : ℕ → R}
     (hf : Summable fun x => ‖f x‖) (hg : Summable fun x => ‖g x‖) :
     ((∑' n, f n) * ∑' n, g n) = ∑' n, ∑ kl in antidiagonal n, f kl.1 * g kl.2 :=
-  tsum_mul_tsum_eq_tsum_sum_antidiagonal (summable_of_summable_norm hf)
-    (summable_of_summable_norm hg) (summable_mul_of_summable_norm hf hg)
+  tsum_mul_tsum_eq_tsum_sum_antidiagonal hf.of_norm hg.of_norm (summable_mul_of_summable_norm hf hg)
 #align tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm
 
 theorem summable_norm_sum_mul_range_of_summable_norm {f g : ℕ → R} (hf : Summable fun x => ‖f x‖)

Mathlib/Analysis/Normed/Group/InfiniteSum.lean

@@ -110,11 +110,11 @@ theorem hasSum_iff_tendsto_nat_of_summable_norm {f : ℕ → E} {a : E} (hf : Su
 
 /-- The direct comparison test for series:  if the norm of `f` is bounded by a real function `g`
 which is summable, then `f` is summable. -/
-theorem summable_of_norm_bounded [CompleteSpace E] {f : ι → E} (g : ι → ℝ) (hg : Summable g)
+theorem Summable.of_norm_bounded [CompleteSpace E] {f : ι → E} (g : ι → ℝ) (hg : Summable g)
     (h : ∀ i, ‖f i‖ ≤ g i) : Summable f := by
   rw [summable_iff_cauchySeq_finset]
   exact cauchySeq_finset_of_norm_bounded g hg h
-#align summable_of_norm_bounded summable_of_norm_bounded
+#align summable_of_norm_bounded Summable.of_norm_bounded
 
 theorem HasSum.norm_le_of_bounded {f : ι → E} {g : ι → ℝ} {a : E} {b : ℝ} (hf : HasSum f a)
     (hg : HasSum g b) (h : ∀ i, ‖f i‖ ≤ g i) : ‖a‖ ≤ b := by
@@ -160,21 +160,26 @@ variable [CompleteSpace E]
 
 /-- Variant of the direct comparison test for series:  if the norm of `f` is eventually bounded by a
 real function `g` which is summable, then `f` is summable. -/
-theorem summable_of_norm_bounded_eventually {f : ι → E} (g : ι → ℝ) (hg : Summable g)
+theorem Summable.of_norm_bounded_eventually {f : ι → E} (g : ι → ℝ) (hg : Summable g)
     (h : ∀ᶠ i in cofinite, ‖f i‖ ≤ g i) : Summable f :=
   summable_iff_cauchySeq_finset.2 <| cauchySeq_finset_of_norm_bounded_eventually hg h
-#align summable_of_norm_bounded_eventually summable_of_norm_bounded_eventually
+#align summable_of_norm_bounded_eventually Summable.of_norm_bounded_eventually
 
-theorem summable_of_nnnorm_bounded {f : ι → E} (g : ι → ℝ≥0) (hg : Summable g)
+/-- Variant of the direct comparison test for series:  if the norm of `f` is eventually bounded by a
+real function `g` which is summable, then `f` is summable. -/
+theorem Summable.of_norm_bounded_eventually_nat {f : ℕ → E} (g : ℕ → ℝ) (hg : Summable g)
+    (h : ∀ᶠ i in atTop, ‖f i‖ ≤ g i) : Summable f :=
+  .of_norm_bounded_eventually g hg <| Nat.cofinite_eq_atTop ▸ h
+
+theorem Summable.of_nnnorm_bounded {f : ι → E} (g : ι → ℝ≥0) (hg : Summable g)
     (h : ∀ i, ‖f i‖₊ ≤ g i) : Summable f :=
-  summable_of_norm_bounded (fun i => (g i : ℝ)) (NNReal.summable_coe.2 hg) fun i => by
-    exact_mod_cast h i
-#align summable_of_nnnorm_bounded summable_of_nnnorm_bounded
+  .of_norm_bounded (fun i => (g i : ℝ)) (NNReal.summable_coe.2 hg) h
+#align summable_of_nnnorm_bounded Summable.of_nnnorm_bounded
 
-theorem summable_of_summable_norm {f : ι → E} (hf : Summable fun a => ‖f a‖) : Summable f :=
-  summable_of_norm_bounded _ hf fun _i => le_rfl
-#align summable_of_summable_norm summable_of_summable_norm
+theorem Summable.of_norm {f : ι → E} (hf : Summable fun a => ‖f a‖) : Summable f :=
+  .of_norm_bounded _ hf fun _i => le_rfl
+#align summable_of_summable_norm Summable.of_norm
 
-theorem summable_of_summable_nnnorm {f : ι → E} (hf : Summable fun a => ‖f a‖₊) : Summable f :=
-  summable_of_nnnorm_bounded _ hf fun _i => le_rfl
-#align summable_of_summable_nnnorm summable_of_summable_nnnorm
+theorem Summable.of_nnnorm {f : ι → E} (hf : Summable fun a => ‖f a‖₊) : Summable f :=
+  .of_nnnorm_bounded _ hf fun _i => le_rfl
+#align summable_of_summable_nnnorm Summable.of_nnnorm

Mathlib/Analysis/NormedSpace/Banach.lean

@@ -199,15 +199,15 @@ theorem exists_preimage_norm_le (surj : Surjective f) :
       C * ‖h^[n] y‖ ≤ C * ((1 / 2) ^ n * ‖y‖) := mul_le_mul_of_nonneg_left (hnle n) C0
       _ = (1 / 2) ^ n * (C * ‖y‖) := by ring
   have sNu : Summable fun n => ‖u n‖ := by
-    refine' summable_of_nonneg_of_le (fun n => norm_nonneg _) ule _
+    refine' .of_nonneg_of_le (fun n => norm_nonneg _) ule _
     exact Summable.mul_right _ (summable_geometric_of_lt_1 (by norm_num) (by norm_num))
-  have su : Summable u := summable_of_summable_norm sNu
+  have su : Summable u := sNu.of_norm
   let x := tsum u
   have x_ineq : ‖x‖ ≤ (2 * C + 1) * ‖y‖ :=
     calc
       ‖x‖ ≤ ∑' n, ‖u n‖ := norm_tsum_le_tsum_norm sNu
       _ ≤ ∑' n, (1 / 2) ^ n * (C * ‖y‖) :=
-        (tsum_le_tsum ule sNu (Summable.mul_right _ summable_geometric_two))
+        tsum_le_tsum ule sNu (Summable.mul_right _ summable_geometric_two)
       _ = (∑' n, (1 / 2) ^ n) * (C * ‖y‖) := tsum_mul_right
       _ = 2 * C * ‖y‖ := by rw [tsum_geometric_two, mul_assoc]
       _ ≤ 2 * C * ‖y‖ + ‖y‖ := (le_add_of_nonneg_right (norm_nonneg y))

Mathlib/Analysis/NormedSpace/Exponential.lean

@@ -213,13 +213,13 @@ variable [CompleteSpace 𝔸]
 theorem expSeries_summable_of_mem_ball (x : 𝔸)
     (hx : x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) :
     Summable fun n => expSeries 𝕂 𝔸 n fun _ => x :=
-  summable_of_summable_norm (norm_expSeries_summable_of_mem_ball x hx)
+  (norm_expSeries_summable_of_mem_ball x hx).of_norm
 #align exp_series_summable_of_mem_ball expSeries_summable_of_mem_ball
 
 theorem expSeries_summable_of_mem_ball' (x : 𝔸)
     (hx : x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) :
     Summable fun n => (n !⁻¹ : 𝕂) • x ^ n :=
-  summable_of_summable_norm (norm_expSeries_summable_of_mem_ball' x hx)
+  (norm_expSeries_summable_of_mem_ball' x hx).of_norm
 #align exp_series_summable_of_mem_ball' expSeries_summable_of_mem_ball'
 
 theorem expSeries_hasSum_exp_of_mem_ball (x : 𝔸)
@@ -342,7 +342,7 @@ theorem norm_expSeries_div_summable_of_mem_ball (x : 𝔸)
 
 theorem expSeries_div_summable_of_mem_ball [CompleteSpace 𝔸] (x : 𝔸)
     (hx : x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) : Summable fun n => x ^ n / n ! :=
-  summable_of_summable_norm (norm_expSeries_div_summable_of_mem_ball 𝕂 x hx)
+  (norm_expSeries_div_summable_of_mem_ball 𝕂 x hx).of_norm
 #align exp_series_div_summable_of_mem_ball expSeries_div_summable_of_mem_ball
 
 theorem expSeries_div_hasSum_exp_of_mem_ball [CompleteSpace 𝔸] (x : 𝔸)
@@ -389,7 +389,7 @@ variable [NormedRing 𝔹] [NormedAlgebra 𝕂 𝔹]
 has an infinite radius of convergence. -/
 theorem expSeries_radius_eq_top : (expSeries 𝕂 𝔸).radius = ∞ := by
   refine' (expSeries 𝕂 𝔸).radius_eq_top_of_summable_norm fun r => _
-  refine' summable_of_norm_bounded_eventually _ (Real.summable_pow_div_factorial r) _
+  refine' .of_norm_bounded_eventually _ (Real.summable_pow_div_factorial r) _
   filter_upwards [eventually_cofinite_ne 0] with n hn
   rw [norm_mul, norm_norm (expSeries 𝕂 𝔸 n), expSeries]
   rw [norm_smul (n ! : 𝕂)⁻¹ (ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸)]
@@ -420,11 +420,11 @@ section CompleteAlgebra
 variable [CompleteSpace 𝔸]
 
 theorem expSeries_summable (x : 𝔸) : Summable fun n => expSeries 𝕂 𝔸 n fun _ => x :=
-  summable_of_summable_norm (norm_expSeries_summable x)
+  (norm_expSeries_summable x).of_norm
 #align exp_series_summable expSeries_summable
 
 theorem expSeries_summable' (x : 𝔸) : Summable fun n => (n !⁻¹ : 𝕂) • x ^ n :=
-  summable_of_summable_norm (norm_expSeries_summable' x)
+  (norm_expSeries_summable' x).of_norm
 #align exp_series_summable' expSeries_summable'
 
 theorem expSeries_hasSum_exp (x : 𝔸) : HasSum (fun n => expSeries 𝕂 𝔸 n fun _ => x) (exp 𝕂 x) :=
@@ -589,7 +589,7 @@ theorem norm_expSeries_div_summable (x : 𝔸) : Summable fun n => ‖(x ^ n / n
 variable [CompleteSpace 𝔸]
 
 theorem expSeries_div_summable (x : 𝔸) : Summable fun n => x ^ n / n ! :=
-  summable_of_summable_norm (norm_expSeries_div_summable 𝕂 x)
+  (norm_expSeries_div_summable 𝕂 x).of_norm
 #align exp_series_div_summable expSeries_div_summable
 
 theorem expSeries_div_hasSum_exp (x : 𝔸) : HasSum (fun n => x ^ n / n !) (exp 𝕂 x) :=