-- 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
dsimp :
  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)
⊢ Summable (α := ℝ≥0) (β := (n : ℕ) × Finset (Fin n))
    ((fun (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) ↦
        nnnorm (E :=
              ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜
                (fun
                    (i :
                      Fin
                        (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) +
                          s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).fst (β :=
                            fun (l : ℕ) ↦
                            { s_1 :
                              Finset
                                (Fin
                                  (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) +
                                    l)) //
                              s_1.card = l }))) ↦
                  E)
                F)
              (p
                (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) +
                  s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).fst (β :=
                    fun (l : ℕ) ↦
                    { s_1 :
                      Finset
                        (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                      s_1.card = l }))) *
            r ^
              s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).fst (β := fun (l : ℕ) ↦
                { s_1 :
                  Finset (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                  s_1.card = l }) *
          r' ^ s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })) ∘
      (⇑changeOriginIndexEquiv.symm :
        (a : (n : ℕ) × Finset (Fin n)) → (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }))

Tactic:
dsimp only [Function.comp_def, changeOriginIndexEquiv_symm_apply_fst,
    changeOriginIndexEquiv_symm_apply_snd_fst]

Premises used: FormalMultilinearSeries.changeOriginIndexEquiv_symm_apply_fst, FormalMultilinearSeries.changeOriginIndexEquiv_symm_apply_snd_fst, Function.comp_def