-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
ι : Type u_2
A' : Type u_4
inst_3 : NormedCommRing A'
inst_4 : NormedAlgebra 𝕜 A'
inst_5 : DecidableEq ι
inst_6 : NormOneClass A'
f : ι → E → A'
N : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
i : ι
u : Finset ι
hi : i ∉ u
IH :
  ∀ (hf : ∀ i ∈ u, ContDiffOn 𝕜 N (f i) s) {n : ℕ} (hn : (↑n : ℕ∞ω) ≤ N),
    norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin n) ↦ E) A')
        (iteratedFDerivWithin 𝕜 n (fun (x : E) ↦ ∏ j ∈ u, f j x) s x) ≤
      ∑ p ∈ u.sym n,
        HMul.hMul (α := ℝ) (↑(↑p : Multiset ι).countPerms : ℝ)
          (∏ j ∈ u,
            norm (E :=
              ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (Multiset.count j (↑p : Multiset ι))) ↦ E) A')
              (iteratedFDerivWithin 𝕜 (Multiset.count j (↑p : Multiset ι)) (f j) s x))
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
hf : ContDiffOn 𝕜 N (f i) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 N (f a) s
insert :
  LE.le (α := ℝ)
    (∑ i_1 : Fin (n + 1),
      (↑(n.choose (↑i_1 : ℕ)) : ℝ) *
          norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (↑i_1 : ℕ)) ↦ E) A')
            (iteratedFDerivWithin 𝕜 (↑i_1 : ℕ) (f i) s x) *
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (n - (↑i_1 : ℕ))) ↦ E) A')
          (iteratedFDerivWithin 𝕜 (n - (↑i_1 : ℕ)) (fun (y : E) ↦ ∏ i ∈ u, f i y) s x))
    (∑ a : Fin (n + 1),
      ∑ s_1 : ↥(u.sym (n - (↑a : ℕ))),
        comp (α := (i : Fin (n + 1)) × ↥(u.sym (n - (↑i : ℕ))))
          (fun (v : Multiset ι) ↦
            HMul.hMul (α := ℝ) (↑v.countPerms : ℝ)
              (∏ j ∈ Insert.insert i u,
                norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (Multiset.count j v)) ↦ E) A')
                  (iteratedFDerivWithin 𝕜 (Multiset.count j v) (f j) s x)))
          (comp (β := Sym ι n) Sym.toMultiset
            (comp (β := ↥((Insert.insert i u).sym n))
              (Subtype.val (p := fun (x : Sym ι n) ↦ x ∈ (Insert.insert i u).sym n))
              (⇑(Equiv.symm (Finset.symInsertEquiv hi)) :
                (a : (i : Fin (n + 1)) × ↥(u.sym (n - (↑i : ℕ)))) → ↥((Insert.insert i u).sym n))))
          (Sigma.mk (β := fun (i : Fin (n + 1)) ↦ ↥(u.sym (n - (↑i : ℕ)))) a s_1))
⊢ LE.le (α := ℝ)
    (∑ i_1 ∈ Finset.range (n + 1),
      (↑(n.choose i_1) : ℝ) *
          norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin i_1) ↦ E) A')
            (iteratedFDerivWithin 𝕜 i_1 (f i) s x) *
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (n - i_1)) ↦ E) A')
          (iteratedFDerivWithin 𝕜 (n - i_1) (fun (y : E) ↦ ∏ i ∈ u, f i y) s x))
    (∑ i_1 : (i : Fin (n + 1)) × ↥(u.sym (n - (↑i : ℕ))),
      ((fun (v : Multiset ι) ↦
            HMul.hMul (α := ℝ) (↑v.countPerms : ℝ)
              (∏ j ∈ Insert.insert i u,
                norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (Multiset.count j v)) ↦ E) A')
                  (iteratedFDerivWithin 𝕜 (Multiset.count j v) (f j) s x))) ∘
          comp (β := Sym ι n) Sym.toMultiset
            (comp (β := ↥((Insert.insert i u).sym n))
              (Subtype.val (p := fun (x : Sym ι n) ↦ x ∈ (Insert.insert i u).sym n))
              (⇑(Equiv.symm (Finset.symInsertEquiv hi)) :
                (a : (i : Fin (n + 1)) × ↥(u.sym (n - (↑i : ℕ)))) → ↥((Insert.insert i u).sym n))))
        i_1)

Tactic:
rw [← Finset.univ_sigma_univ, Finset.sum_sigma, Finset.sum_range]

Premises used: Finset.sum_sigma, Finset.univ_sigma_univ, Finset.sum_range