-- 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 : ℕ
hn : ∀ (m : ℕ), n ≤ 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)
k : ℕ
this :
  ∀ (m : ℕ) (hm : m ∉ Finset.range n),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F)
      ((p.changeOriginSeries k m : (a : (i : Fin m) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F)
        fun (x_1 : Fin m) ↦ x)
      0
⊢ 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))
    (∑' (a : ℕ),
      ((p.changeOriginSeries k a : (a : (i : Fin a) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F)
            fun (x_1 : Fin a) ↦ x :
          (a : (i : Fin k) → E) → F)
        fun (x : Fin k) ↦ y)

Tactic:
(summable_of_ne_finset_zero (s := Finset.range n) fun m hm ↦ ?_).hasSum.sigma_of_hasSum
      (hfkl k) (summable_of_hasFiniteSupport <| finsupp.preimage sigma_mk_injective.injOn)

Premises used: Function.Injective.injOn, summable_of_hasFiniteSupport, Summable.hasSum, summable_of_ne_finset_zero, sigma_mk_injective, HasSum.sigma_of_hasSum, Set.Finite.preimage