-- Mathlib/Analysis/Analytic/Inverse.lean
theorem radius_rightInv_pos_of_radius_pos_aux2 {x : E} {n : ℕ} (hn : 2 ≤ n + 1)
    (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) {r a C : ℝ} (hr : 0 ≤ r) (ha : 0 ≤ a)
    (hC : 0 ≤ C) (hp : ∀ n, ‖p n‖ ≤ C * r ^ n) :
    ∑ k ∈ Ico 1 (n + 1), a ^ k * ‖p.rightInv i x k‖ ≤
      ‖(i.symm : F →L[𝕜] E)‖ * a +
        ‖(i.symm : F →L[𝕜] E)‖ * C *
          ∑ k ∈ Ico 2 (n + 1), (r * ∑ j ∈ Ico 1 n, a ^ j * ‖p.rightInv i x j‖) ^ k :=
  let I := ‖(i.symm : F →L[𝕜] E)‖
  calc
    ∑ k ∈ Ico 1 (n + 1), a ^ k * ‖p.rightInv i x k‖ =
        a * I + ∑ k ∈ Ico 2 (n + 1), a ^ k * ‖p.rightInv i x k‖

Proof state:
case bc.h.h.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
n : ℕ
hn : 2 ≤ n + 1
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
r a C : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
hC : 0 ≤ C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖↑i.symm‖
j : ℕ
a✝ : j ∈ Ico 2 (n + 1)
⊢ ‖∑ c ∈ {c | 1 < c.length}.toFinset, p.compAlongComposition (p.rightInv i x) c‖ ≤
    ∑ c ∈ {c | 1 < c.length}.toFinset, C * r ^ c.length * ∏ j_1 : Fin c.length, ‖p.rightInv i x (c.blocksFun j_1)‖

Tactic:
apply (norm_sum_le _ _).trans

Result:
case bc.h.h.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
n : ℕ
hn : 2 ≤ n + 1
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
r a C : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
hC : 0 ≤ C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖↑i.symm‖
j : ℕ
a✝ : j ∈ Ico 2 (n + 1)
⊢ ∑ i_1 ∈ {c | 1 < c.length}.toFinset, ‖p.compAlongComposition (p.rightInv i x) i_1‖ ≤
    ∑ c ∈ {c | 1 < c.length}.toFinset, C * r ^ c.length * ∏ j_1 : Fin c.length, ‖p.rightInv i x (c.blocksFun j_1)‖

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
n : ℕ
hn : 2 ≤ n + 1
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
r a C : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
hC : 0 ≤ C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖↑i.symm‖
⊢ ‖↑i.symm‖ * a +
      ‖↑i.symm‖ *
        (C *
          ∑ i_1 ∈ Ico 2 (n + 1),
            a ^ i_1 *
              ∑ i_2 ∈ {c | 1 < c.length}.toFinset,
                r ^ i_2.length * ∏ j : Fin i_2.length, ‖p.rightInv i x (i_2.blocksFun j)‖) =
    ‖↑i.symm‖ * a +
      C *
        (‖↑i.symm‖ *
          ∑ k ∈ Ico 2 (n + 1),
            a ^ k *
              ∑ c ∈ {c | 1 < c.length}.toFinset, r ^ c.length * ∏ j : Fin c.length, ‖p.rightInv i x (c.blocksFun j)‖)

Tactic:
ring

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
n : ℕ
hn : 2 ≤ n + 1
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
r a C : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
hC : 0 ≤ C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖↑i.symm‖
⊢ a * I +
      ∑ k ∈ Ico 2 (n + 1),
        a ^ k *
          ‖(↑i.symm).compContinuousMultilinearMap
              (∑ c ∈ {c | 1 < c.length}.toFinset, p.compAlongComposition (p.rightInv i x) c)‖ ≤
    a * ‖↑i.symm‖ +
      ∑ k ∈ Ico 2 (n + 1),
        a ^ k *
          (I *
            ∑ c ∈ {c | 1 < c.length}.toFinset, C * r ^ c.length * ∏ j : Fin c.length, ‖p.rightInv i x (c.blocksFun j)‖)

Tactic:
gcongr with j

Result:
case bc.h.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
n : ℕ
hn : 2 ≤ n + 1
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
r a C : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
hC : 0 ≤ C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖↑i.symm‖
j : ℕ
a✝ : j ∈ Ico 2 (n + 1)
⊢ ‖(↑i.symm).compContinuousMultilinearMap
        (∑ c ∈ {c | 1 < c.length}.toFinset, p.compAlongComposition (p.rightInv i x) c)‖ ≤
    I * ∑ c ∈ {c | 1 < c.length}.toFinset, C * r ^ c.length * ∏ j_1 : Fin c.length, ‖p.rightInv i x (c.blocksFun j_1)‖

Proof state:
case bc.h.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
n : ℕ
hn : 2 ≤ n + 1
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
r a C : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
hC : 0 ≤ C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖↑i.symm‖
j : ℕ
a✝ : j ∈ Ico 2 (n + 1)
⊢ ‖(↑i.symm).compContinuousMultilinearMap
        (∑ c ∈ {c | 1 < c.length}.toFinset, p.compAlongComposition (p.rightInv i x) c)‖ ≤
    I * ∑ c ∈ {c | 1 < c.length}.toFinset, C * r ^ c.length * ∏ j_1 : Fin c.length, ‖p.rightInv i x (c.blocksFun j_1)‖

Tactic:
apply (ContinuousLinearMap.norm_compContinuousMultilinearMap_le _ _).trans

Result:
case bc.h.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
n : ℕ
hn : 2 ≤ n + 1
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
r a C : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
hC : 0 ≤ C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖↑i.symm‖
j : ℕ
a✝ : j ∈ Ico 2 (n + 1)
⊢ ‖↑i.symm‖ * ‖∑ c ∈ {c | 1 < c.length}.toFinset, p.compAlongComposition (p.rightInv i x) c‖ ≤
    I * ∑ c ∈ {c | 1 < c.length}.toFinset, C * r ^ c.length * ∏ j_1 : Fin c.length, ‖p.rightInv i x (c.blocksFun j_1)‖

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
n : ℕ
hn : 2 ≤ n + 1
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
r a C : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
hC : 0 ≤ C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖↑i.symm‖
⊢ I * a +
      I * C *
        ∑ k ∈ Ico 2 (n + 1),
          a ^ k *
            ∑ c ∈ {c | 1 < c.length}.toFinset, r ^ c.length * ∏ j : Fin c.length, ‖p.rightInv i x (c.blocksFun j)‖ ≤
    I * a + I * C * ∑ k ∈ Ico 2 (n + 1), (r * ∑ j ∈ Ico 1 n, a ^ j * ‖p.rightInv i x j‖) ^ k

Tactic:
gcongr _ + _ * _ * ?_

Result:
case bc.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
n : ℕ
hn : 2 ≤ n + 1
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
r a C : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
hC : 0 ≤ C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖↑i.symm‖
⊢ ∑ k ∈ Ico 2 (n + 1),
      a ^ k * ∑ c ∈ {c | 1 < c.length}.toFinset, r ^ c.length * ∏ j : Fin c.length, ‖p.rightInv i x (c.blocksFun j)‖ ≤
    ∑ k ∈ Ico 2 (n + 1), (r * ∑ j ∈ Ico 1 n, a ^ j * ‖p.rightInv i x j‖) ^ k