no goals
𝕜 : Type u_3
E : Type u_1
F : Type u_2
G : Type ?u.1254141
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 E F
x y : E
r R : ℝ≥0
k l : ℕ
⊢ ∑ a : { s // Finset.card s = l }, ‖changeOriginSeriesTerm p k l ↑a (_ : Finset.card ↑a = l)‖₊ =
    ∑' (x : { s // Finset.card s = l }), ‖p (k + l)‖₊
simp_rw [tsum_fintype, nnnorm_changeOriginSeriesTerm (p := p) (k := k) (l := l)]