-- 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))
p : Sym ι (n - (↑m : ℕ))
hp : ∀ a ∈ p, a ∈ u
hip : i ∉ p
⊢ (↑(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 (α := ℝ) (↑(↑p : Multiset ι).countPerms : ℝ)
        (∏ x_1 ∈ u,
          norm (E :=
            ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (Multiset.count x_1 (↑p : Multiset ι))) ↦ E) A')
            (iteratedFDerivWithin 𝕜 (Multiset.count x_1 (↑p : Multiset ι)) (f x_1) s x)) =
    (↑(↑(Sym.fill i m p) : Multiset ι).countPerms : ℝ) *
      (norm (E :=
          ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜
            (fun (i : Fin (Multiset.count i (↑(Sym.fill i m p) : Multiset ι))) ↦ E) A')
          (iteratedFDerivWithin 𝕜 (Multiset.count i (↑(Sym.fill i m p) : Multiset ι)) (f i) s x) *
        ∏ x_1 ∈ u,
          norm (E :=
            ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜
              (fun (i : Fin (Multiset.count x_1 (↑(Sym.fill i m p) : Multiset ι))) ↦ E) A')
            (iteratedFDerivWithin 𝕜 (Multiset.count x_1 (↑(Sym.fill i m p) : Multiset ι)) (f x_1) s x))
have insert : (↑(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 (α := ℝ) (↑(↑p : Multiset ι).countPerms : ℝ)
      (∏ x_1 ∈ u,
        norm (E :=
          ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (Multiset.count x_1 (↑p : Multiset ι))) ↦ E) A')
          (iteratedFDerivWithin 𝕜 (Multiset.count x_1 (↑p : Multiset ι)) (f x_1) s x)) =
  (↑(n.choose (↑m : ℕ) * (↑p : Multiset ι).countPerms) : ℝ) *
    (norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (↑m : ℕ)) ↦ E) A')
        (iteratedFDerivWithin 𝕜 (↑m : ℕ) (f i) s x) *
      ∏ x_1 ∈ u,
        norm (E :=
          ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜
            (fun (i : Fin (Multiset.count x_1 (↑(Sym.fill i m p) : Multiset ι))) ↦ E) A')
          (iteratedFDerivWithin 𝕜 (Multiset.count x_1 (↑(Sym.fill i m p) : Multiset ι)) (f x_1) s x))
Tactic: rw [Sym.count_coe_fill_self_of_notMem hip, Sym.countPerms_coe_fill_of_notMem hip]