-- 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))
⊢ ∀ (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))
have insert : ∀ (a : Sym ι (n - (↑m : ℕ))) (b : ∀ a_1 ∈ a, a_1 ∈ u),
  (↑(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 (α := ℝ) (↑(↑a : Multiset ι).countPerms : ℝ)
        (∏ x_1 ∈ u,
          norm (E :=
            ContinuousMultilinearMap.{u_1, 0, uE, u_4} 𝕜 (fun (i : Fin (Multiset.count x_1 (↑a : Multiset ι))) ↦ E) A')
            (iteratedFDerivWithin 𝕜 (Multiset.count x_1 (↑a : Multiset ι)) (f x_1) s x)) ≤
    HMul.hMul (α := ℝ) (↑(↑(Sym.fill i m a) : 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 a) : Multiset ι))) ↦ E) A')
          (iteratedFDerivWithin 𝕜 (Multiset.count x_1 (↑(Sym.fill i m a) : Multiset ι)) (f x_1) s x))
Tactic: simp only [Finset.mem_univ, forall_true_left, Subtype.forall, Finset.mem_sym_iff]