-- Module: Mathlib.Analysis.Analytic.ChangeOrigin
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)
refine :
  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)))
⊢ Summable (α := ℝ≥0) fun (x : (n : ℕ) × Finset (Fin n)) ↦
    nnnorm (E :=
          ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜
            (fun
                (i :
                  Fin
                    (x.fst (β := fun (n : ℕ) ↦ Finset (Fin n)) - x.snd (β := fun (n : ℕ) ↦ Finset (Fin n)).card +
                      x.snd (β := fun (n : ℕ) ↦ Finset (Fin n)).card)) ↦
              E)
            F)
          (p
            (x.fst (β := fun (n : ℕ) ↦ Finset (Fin n)) - x.snd (β := fun (n : ℕ) ↦ Finset (Fin n)).card +
              x.snd (β := fun (n : ℕ) ↦ Finset (Fin n)).card)) *
        r ^ x.snd (β := fun (n : ℕ) ↦ Finset (Fin n)).card *
      r' ^ (x.fst (β := fun (n : ℕ) ↦ Finset (Fin n)) - x.snd (β := fun (n : ℕ) ↦ Finset (Fin n)).card)

Tactic:
refine NNReal.summable_sigma.2 ⟨fun n => (this n).summable, ?_⟩

Premises used: Iff.mpr, NNReal.summable_sigma, And.intro