-- 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'
u : Finset ι
f : ι → E → A'
N : ℕ∞ω
hf : ∀ i ∈ u, ContDiffOn 𝕜 N (f i) s
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
empty :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → 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 ∈ ∅, f j x) s x) ≤
      ∑ p ∈ Finset.sym ∅ n,
        HMul.hMul (α := ℝ) (↑(↑p : Multiset ι).countPerms : ℝ)
          (∏ j ∈ ∅,
            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))
insert :
  ∀ (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)))
    (hf : ∀ i_1 ∈ Insert.insert i u, ContDiffOn 𝕜 N (f i_1) 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 ∈ Insert.insert i u, f j x) s x) ≤
      ∑ p ∈ (Insert.insert i u).sym n,
        HMul.hMul (α := ℝ) (↑(↑p : Multiset ι).countPerms : ℝ)
          (∏ j ∈ Insert.insert i 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))
⊢ 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))

Tactic:
induction u using Finset.induction generalizing n with
  | empty =>
    cases n with
    | zero => simp [Sym.eq_nil_of_card_zero]
    | succ n => simp [iteratedFDerivWithin_succ_const]
  | insert i u hi IH =>
    conv => lhs; simp only [Finset.prod_insert hi]
    simp only [Finset.mem_insert, forall_eq_or_imp] at hf
    refine le_trans (norm_iteratedFDerivWithin_mul_le hf.1 (contDiffOn_prod hf.2) hs hx hn) ?_
    rw [← Finset.sum_coe_sort (Finset.sym _ _)]
    rw [Finset.sum_equiv (Finset.symInsertEquiv hi) (t := Finset.univ)
      (g := (fun v ↦ v.countPerms *
          ∏ j ∈ insert i u, ‖iteratedFDerivWithin 𝕜 (v.count j) (f j) s x‖) ∘
        Sym.toMultiset ∘ Subtype.val ∘ (Finset.symInsertEquiv hi).symm)
      (by simp) (by simp only [← comp_apply (g := Finset.symInsertEquiv hi), comp_assoc]; simp)]
    rw [← Finset.univ_sigma_univ, Finset.sum_sigma, Finset.sum_range]
    simp +instances only [comp_apply, Finset.symInsertEquiv_symm_apply_coe]
    gcongr with m _
    specialize IH hf.2 (n := n - m) (le_trans (by exact_mod_cast n.sub_le m) hn)
    grw [IH]
    rw [Finset.mul_sum, ← Finset.sum_coe_sort]
    refine Finset.sum_le_sum ?_
    simp only [Finset.mem_univ, forall_true_left, Subtype.forall, Finset.mem_sym_iff]
    intro p hp
    refine le_of_eq ?_
    rw [Finset.prod_insert hi]
    have hip : i ∉ p := mt (hp i) hi
    rw [Sym.count_coe_fill_self_of_notMem hip, Sym.countPerms_coe_fill_of_notMem hip]
    suffices ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j p) (f j) s x‖ =
        ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j (Sym.fill i m p)) (f j) s x‖ by
      rw [this, Nat.cast_mul]
      ring
    refine Finset.prod_congr rfl ?_
    intro j hj
    have hji : j ≠ i := mt (· ▸ hj) hi
    rw [Sym.count_coe_fill_of_ne hji]

Premises used: Finset.mem_univ, Finset.mul_sum, forall_true_left, Finset.mem_sym_iff, Fin.succ, iteratedFDerivWithin_succ_const, Finset.sum_sigma, Subtype.forall, Insert.insert, Finset.mem_insert, Finset.prod_congr, forall_eq_or_imp, Finset.univ_sigma_univ, Finset.sum_range, Sym.eq_nil_of_card_zero, Finset.sum_le_sum, Function.comp_apply, Finset.sym, Finset.symInsertEquiv_symm_apply_coe, le_of_eq, Finset.sum_coe_sort, rfl