-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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
n_1 : ℕ
hn : ∀ (m : ℕ), n_1 ≤ m → p m = 0
x y : E
f : (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) → F :=
  fun (s : (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) ↦
    ((p.changeOriginSeriesTerm (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 }))
              (↑(s.snd (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }).snd (β := fun (l : ℕ) ↦
                    { s_1 :
                      Finset
                        (Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) + l)) //
                      s_1.card = l })) :
                Finset (Fin (s.fst + s.snd.fst)))
              ⋯ :
            (a : (i : Fin s.snd.fst) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin s.fst) ↦ E) F)
          fun
            (x_1 :
              Fin
                (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 }))) ↦
          x :
        (a : (i : Fin s.fst) → E) → F)
      fun (x : Fin (s.fst (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }))) ↦ y
finsupp : (Function.support f).Finite
hfkl :
  ∀ (k l : ℕ),
    HasSum.{u_3, 0} (α := F)
      (fun (x : { s : Finset (Fin (k + l)) // s.card = l }) ↦
        f
          (Sigma.mk (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) k
            (Sigma.mk (β := fun (l : ℕ) ↦ { s : Finset (Fin (k + l)) // s.card = l }) l x)))
      (((p.changeOriginSeries k l : (a : (i : Fin l) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F)
              fun (x_1 : Fin l) ↦ x :
            (a : (i : Fin k) → E) → F)
          fun (x : Fin k) ↦ y :
        F)
hfk :
  ∀ (k : ℕ),
    HasSum.{u_3, 0} (α := F)
      (fun (x : (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) ↦
        f (Sigma.mk (β := fun (k : ℕ) ↦ (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l }) k x))
      ((p.changeOrigin x k : (a : (i : Fin k) → E) → F) fun (x : Fin k) ↦ y : F)
hf : HasSum f ((p.changeOrigin x).sum y)
n : ℕ
simp_rw :
  HasSum.{u_3, 0} (α := F)
    (fun (c : Finset (Fin n)) ↦
      Function.comp (α := (n : ℕ) × Finset (Fin n)) f
        (⇑changeOriginIndexEquiv.symm :
          (a : (n : ℕ) × Finset (Fin n)) → (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
        (Sigma.mk (β := fun (b : ℕ) ↦ Finset (Fin b)) n c))
    (∑ x_1 : Finset (Fin n),
      ((p.changeOriginSeriesTerm
                (Sigma.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 })
                    (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin n)) n x_1)))
                (Sigma.fst (β := fun (l : ℕ) ↦
                  { s :
                    Finset
                      (Fin
                        (Sigma.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 })
                              (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin n)) n x_1)) +
                          l)) //
                    s.card = l })
                  (Sigma.snd (β := 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 })
                      (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin n)) n x_1))))
                (↑(Sigma.snd (β := fun (l : ℕ) ↦
                        { s :
                          Finset
                            (Fin
                              (Sigma.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 })
                                    (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin n)) n x_1)) +
                                l)) //
                          s.card = l })
                        (Sigma.snd (β := 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 })
                            (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin n)) n x_1))) :
                      { s :
                        Finset
                          (Fin
                            (HAdd.hAdd (α := ℕ)
                              (Sigma.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 })
                                  (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin n)) n x_1)))
                              (Sigma.fst (β := fun (l : ℕ) ↦
                                { s :
                                  Finset
                                    (Fin
                                      (Sigma.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 })
                                            (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin n)) n x_1)) +
                                        l)) //
                                  s.card = l })
                                (Sigma.snd (β := 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 })
                                    (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin n)) n x_1)))))) //
                        s.card =
                          Sigma.fst (β := fun (l : ℕ) ↦
                            { s :
                              Finset
                                (Fin
                                  (Sigma.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 })
                                        (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin n)) n x_1)) +
                                    l)) //
                              s.card = l })
                            (Sigma.snd (β := 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 })
                                (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin n)) n x_1))) }) :
                  Finset
                    (Fin
                      (((changeOriginIndexEquiv.symm :
                              (a : (n : ℕ) × Finset (Fin n)) →
                                (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                            ⟨n, x_1⟩).fst +
                        ((changeOriginIndexEquiv.symm :
                                (a : (n : ℕ) × Finset (Fin n)) →
                                  (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                              ⟨n, x_1⟩).snd.fst)))
                ⋯ :
              (a :
                  (i :
                      Fin
                        ((changeOriginIndexEquiv.symm :
                                (a : (n : ℕ) × Finset (Fin n)) →
                                  (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                              ⟨n, x_1⟩).snd.fst) →
                    E) →
                ContinuousMultilinearMap 𝕜
                  (fun
                      (i :
                        Fin
                          ((changeOriginIndexEquiv.symm :
                                (a : (n : ℕ) × Finset (Fin n)) →
                                  (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                              ⟨n, x_1⟩).fst) ↦
                    E)
                  F)
            fun
              (x_2 :
                Fin
                  (Sigma.fst (β := fun (l : ℕ) ↦
                    { s :
                      Finset
                        (Fin
                          (Sigma.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 })
                                (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin n)) n x_1)) +
                            l)) //
                      s.card = l })
                    (Sigma.snd (β := 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 })
                        (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin n)) n x_1))))) ↦
            x :
          (a :
              (i :
                  Fin
                    ((changeOriginIndexEquiv.symm :
                          (a : (n : ℕ) × Finset (Fin n)) →
                            (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
                        ⟨n, x_1⟩).fst) →
                E) →
            F)
        fun
          (x :
            Fin
              (Sigma.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 })
                  (Sigma.mk (β := fun (n : ℕ) ↦ Finset (Fin n)) n x_1)))) ↦
        y)
⊢ HasSum.{u_3, 0} (α := F)
    (fun (c : Finset (Fin n)) ↦
      Function.comp (α := (n : ℕ) × Finset (Fin n)) f
        (⇑changeOriginIndexEquiv.symm :
          (a : (n : ℕ) × Finset (Fin n)) → (k : ℕ) × (l : ℕ) × { s : Finset (Fin (k + l)) // s.card = l })
        (Sigma.mk (β := fun (b : ℕ) ↦ Finset (Fin b)) n c))
    (∑ s : Finset (Fin n),
      (p n : (a : (i : Fin n) → E) → F)
        (s.piecewise (π := fun (i : Fin n) ↦ E) (fun (x_1 : Fin n) ↦ x) fun (x : Fin n) ↦ y))

Tactic:
simp_rw [← changeOriginSeriesTerm_changeOriginIndexEquiv_symm]

Premises used: FormalMultilinearSeries.changeOriginSeriesTerm_changeOriginIndexEquiv_symm