-- Lean 4 proof step from Mathlib.Analysis.Analytic.ChangeOrigin (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r r' : ℝ≥0
hr : (↑r : ℝ≥0∞) + (↑r' : ℝ≥0∞) < p.radius
this :
  ∀ (n : ℕ),
    HasSum
      (fun (s : Finset (Fin n)) ↦
        nnnorm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n - s.card + s.card)) ↦ E) F)
              (p (n - s.card + s.card)) *
            r ^ s.card *
          r' ^ (n - s.card))
      (‖p n‖₊ * (r + r') ^ n)
⊢ Summable (α := ℝ≥0) fun (x : ℕ) ↦
    ∑' (y : Finset (Fin x)),
      nnnorm (E :=
            ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜
              (fun
                  (i :
                    Fin
                      (Sigma.fst (β := fun (n : ℕ) ↦ Finset (Fin n))
                            (Sigma.mk (β := fun (x : ℕ) ↦ Finset (Fin x)) x y) -
                          Finset.card (α :=
                            Fin
                              (Sigma.fst (β := fun (n : ℕ) ↦ Finset (Fin n))
                                (Sigma.mk (β := fun (x : ℕ) ↦ Finset (Fin x)) x y)))
                            (Sigma.snd (β := fun (n : ℕ) ↦ Finset (Fin n))
                              (Sigma.mk (β := fun (x : ℕ) ↦ Finset (Fin x)) x y)) +
                        Finset.card (α :=
                          Fin
                            (Sigma.fst (β := fun (n : ℕ) ↦ Finset (Fin n))
                              (Sigma.mk (β := fun (x : ℕ) ↦ Finset (Fin x)) x y)))
                          (Sigma.snd (β := fun (n : ℕ) ↦ Finset (Fin n))
                            (Sigma.mk (β := fun (x : ℕ) ↦ Finset (Fin x)) x y)))) ↦
                E)
              F)
            (p
              (Sigma.fst (β := fun (n : ℕ) ↦ Finset (Fin n)) (Sigma.mk (β := fun (x : ℕ) ↦ Finset (Fin x)) x y) -
                  Finset.card (α :=
                    Fin
                      (Sigma.fst (β := fun (n : ℕ) ↦ Finset (Fin n))
                        (Sigma.mk (β := fun (x : ℕ) ↦ Finset (Fin x)) x y)))
                    (Sigma.snd (β := fun (n : ℕ) ↦ Finset (Fin n)) (Sigma.mk (β := fun (x : ℕ) ↦ Finset (Fin x)) x y)) +
                Finset.card (α :=
                  Fin
                    (Sigma.fst (β := fun (n : ℕ) ↦ Finset (Fin n)) (Sigma.mk (β := fun (x : ℕ) ↦ Finset (Fin x)) x y)))
                  (Sigma.snd (β := fun (n : ℕ) ↦ Finset (Fin n)) (Sigma.mk (β := fun (x : ℕ) ↦ Finset (Fin x)) x y)))) *
          r ^
            Finset.card (α :=
              Fin (Sigma.fst (β := fun (n : ℕ) ↦ Finset (Fin n)) (Sigma.mk (β := fun (x : ℕ) ↦ Finset (Fin x)) x y)))
              (Sigma.snd (β := fun (n : ℕ) ↦ Finset (Fin n)) (Sigma.mk (β := fun (x : ℕ) ↦ Finset (Fin x)) x y)) *
        r' ^
          (Sigma.fst (β := fun (n : ℕ) ↦ Finset (Fin n)) (Sigma.mk (β := fun (x : ℕ) ↦ Finset (Fin x)) x y) -
            Finset.card (α :=
              Fin (Sigma.fst (β := fun (n : ℕ) ↦ Finset (Fin n)) (Sigma.mk (β := fun (x : ℕ) ↦ Finset (Fin x)) x y)))
              (Sigma.snd (β := fun (n : ℕ) ↦ Finset (Fin n)) (Sigma.mk (β := fun (x : ℕ) ↦ Finset (Fin x)) x y)))
have simp : Summable (α := ℝ≥0) fun (x : ℕ) ↦ ‖p x‖₊ * (r + r') ^ x
Tactic: simp only [(this _).tsum_eq]