-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Bounds (goal)
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
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
hf : ContDiffOn 𝕜 N (f i) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 N (f a) s
m : Fin (n + 1)
h : Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ m
IH :
  norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (n - (↑m : ℕ))) ↦ E) A')
      (iteratedFDerivWithin 𝕜 (n - (↑m : ℕ)) (fun (x : E) ↦ ∏ j ∈ u, f j x) s x) ≤
    ∑ p ∈ u.sym (n - (↑m : ℕ)),
      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))
⊢ LE.le (α := ℝ)
    (∑ i_1 : ↥(u.sym (n - (↑m : ℕ))),
      (↑(n.choose (↑m : ℕ)) : ℝ) *
          norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (↑m : ℕ)) ↦ E) A')
            (iteratedFDerivWithin 𝕜 (↑m : ℕ) (f i) s x) *
        HMul.hMul (α := ℝ) (↑(↑(↑i_1 : Sym ι (n - (↑m : ℕ))) : Multiset ι).countPerms : ℝ)
          (∏ j ∈ u,
            norm (E :=
              ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜
                (fun (i : Fin (Multiset.count j (↑(↑i_1 : Sym ι (n - (↑m : ℕ))) : Multiset ι))) ↦ E) A')
              (iteratedFDerivWithin 𝕜 (Multiset.count j (↑(↑i_1 : Sym ι (n - (↑m : ℕ))) : Multiset ι)) (f j) s x)))
    (∑ x_1 : ↥(u.sym (n - (↑m : ℕ))),
      HMul.hMul (α := ℝ) (↑(↑(Sym.fill i m (↑x_1 : Sym ι (n - (↑m : ℕ)))) : Multiset ι).countPerms : ℝ)
        (∏ x_2 ∈ insert i u,
          norm (E :=
            ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜
              (fun (i : Fin (Multiset.count x_2 (↑(Sym.fill i m (↑x_1 : Sym ι (n - (↑m : ℕ)))) : Multiset ι))) ↦ E) A')
            (iteratedFDerivWithin 𝕜 (Multiset.count x_2 (↑(Sym.fill i m (↑x_1 : Sym ι (n - (↑m : ℕ)))) : Multiset ι))
              (f x_2) s x)))
have insert : ∀ (i_1 : ↥(u.sym (n - (↑m : ℕ)))),
  Membership.mem (γ := Finset ↥(u.sym (n - (↑m : ℕ)))) Finset.univ i_1 →
    (↑(n.choose (↑m : ℕ)) : ℝ) *
          norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (↑m : ℕ)) ↦ E) A')
            (iteratedFDerivWithin 𝕜 (↑m : ℕ) (f i) s x) *
        HMul.hMul (α := ℝ) (↑(↑(↑i_1 : Sym ι (n - (↑m : ℕ))) : Multiset ι).countPerms : ℝ)
          (∏ j ∈ u,
            norm (E :=
              ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜
                (fun (i : Fin (Multiset.count j (↑(↑i_1 : Sym ι (n - (↑m : ℕ))) : Multiset ι))) ↦ E) A')
              (iteratedFDerivWithin 𝕜 (Multiset.count j (↑(↑i_1 : Sym ι (n - (↑m : ℕ))) : Multiset ι)) (f j) s x)) ≤
      HMul.hMul (α := ℝ) (↑(↑(Sym.fill i m (↑i_1 : Sym ι (n - (↑m : ℕ)))) : Multiset ι).countPerms : ℝ)
        (∏ x_1 ∈ insert i u,
          norm (E :=
            ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜
              (fun (i : Fin (Multiset.count x_1 (↑(Sym.fill i m (↑i_1 : Sym ι (n - (↑m : ℕ)))) : Multiset ι))) ↦ E) A')
            (iteratedFDerivWithin 𝕜 (Multiset.count x_1 (↑(Sym.fill i m (↑i_1 : Sym ι (n - (↑m : ℕ)))) : Multiset ι))
              (f x_1) s x))
Tactic: refine Finset.sum_le_sum ?_