-- 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 : (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)
have 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)))
Tactic: refine NNReal.summable_sigma.2 ⟨fun n => (this n).summable, ?_⟩