-- Mathlib/Analysis/Calculus/ContDiff/Bounds.lean
theorem norm_iteratedFDerivWithin_prod_le [DecidableEq ι] [NormOneClass A'] {u : Finset ι}
    {f : ι → E → A'} {N : WithTop ℕ∞} (hf : ∀ i ∈ u, ContDiffOn 𝕜 N (f i) s)
    (hs : UniqueDiffOn 𝕜 s) {x : E} (hx : x ∈ s) {n : ℕ} (hn : n ≤ N) :
    ‖iteratedFDerivWithin 𝕜 n (∏ j ∈ u, f j ·) s x‖ ≤
      ∑ p ∈ u.sym n, (p : Multiset ι).multinomial *
        ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j p) (f j) s x‖

Proof state:
case insert
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
s : Set E
ι : Type u_2
A' : Type u_4
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : WithTop ℕ∞
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)
a✝ : m ∈ Finset.univ
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j ∈ u, f j x) s x‖ ≤
    ∑ p ∈ u.sym (n - ↑m), ↑(↑p).multinomial * ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
hip : i ∉ p
⊢ ∏ 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‖

Tactic:
refine Finset.prod_congr rfl ?_

Result:
case insert
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
s : Set E
ι : Type u_2
A' : Type u_4
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : WithTop ℕ∞
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)
a✝ : m ∈ Finset.univ
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j ∈ u, f j x) s x‖ ≤
    ∑ p ∈ u.sym (n - ↑m), ↑(↑p).multinomial * ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
hip : i ∉ p
⊢ ∀ x_1 ∈ u,
    ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑p) (f x_1) s x‖ =
      ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑(Sym.fill i m p)) (f x_1) s x‖

Proof state:
case empty
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
s : Set E
ι : Type u_2
A' : Type u_4
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : WithTop ℕ∞
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
hf : ∀ i ∈ ∅, ContDiffOn 𝕜 N (f i) s
n : ℕ
hn : ↑n ≤ N
⊢ ‖iteratedFDerivWithin 𝕜 n (fun x => ∏ j ∈ ∅, f j x) s x‖ ≤
    ∑ p ∈ ∅.sym n, ↑(↑p).multinomial * ∏ j ∈ ∅, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖

Tactic:
cases n with
| zero => simp [Sym.eq_nil_of_card_zero]
| succ n => simp [iteratedFDerivWithin_succ_const]

Result:
no goals

Proof state:
case insert
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
s : Set E
ι : Type u_2
A' : Type u_4
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : WithTop ℕ∞
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)
a✝ : m ∈ Finset.univ
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j ∈ u, f j x) s x‖ ≤
    ∑ p ∈ u.sym (n - ↑m), ↑(↑p).multinomial * ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
⊢ ↑(n.choose ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
      ∑ p ∈ u.sym (n - ↑m), ↑(↑p).multinomial * ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖ ≤
    ∑ x_1 : { x // x ∈ u.sym (n - ↑m) },
      ↑(↑(Sym.fill i m ↑x_1)).multinomial *
        ∏ x_2 ∈ insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_2 ↑(Sym.fill i m ↑x_1)) (f x_2) s x‖

Tactic:
rw [Finset.mul_sum, ← Finset.sum_coe_sort]

Result:
case insert
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
s : Set E
ι : Type u_2
A' : Type u_4
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : WithTop ℕ∞
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)
a✝ : m ∈ Finset.univ
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j ∈ u, f j x) s x‖ ≤
    ∑ p ∈ u.sym (n - ↑m), ↑(↑p).multinomial * ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
⊢ ∑ i_1 : { x // x ∈ u.sym (n - ↑m) },
      ↑(n.choose ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
        (↑(↑↑i_1).multinomial * ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑↑i_1) (f j) s x‖) ≤
    ∑ x_1 : { x // x ∈ u.sym (n - ↑m) },
      ↑(↑(Sym.fill i m ↑x_1)).multinomial *
        ∏ x_2 ∈ insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_2 ↑(Sym.fill i m ↑x_1)) (f x_2) s x‖

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
s : Set E
ι : Type u_2
A' : Type u_4
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : WithTop ℕ∞
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)
a✝ : m ∈ Finset.univ
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j ∈ u, f j x) s x‖ ≤
    ∑ p ∈ u.sym (n - ↑m), ↑(↑p).multinomial * ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
⊢ 0 ≤ ↑(n.choose ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖

Tactic:
simp [mul_nonneg]

Result:
no goals

Proof state:
case empty.zero
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
s : Set E
ι : Type u_2
A' : Type u_4
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : WithTop ℕ∞
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
hf : ∀ i ∈ ∅, ContDiffOn 𝕜 N (f i) s
hn : ↑0 ≤ N
⊢ ‖iteratedFDerivWithin 𝕜 0 (fun x => ∏ j ∈ ∅, f j x) s x‖ ≤
    ∑ p ∈ ∅.sym 0, ↑(↑p).multinomial * ∏ j ∈ ∅, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖

Tactic:
simp [Sym.eq_nil_of_card_zero]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
s : Set E
ι : Type u_2
A' : Type u_4
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : WithTop ℕ∞
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
i : ι
u : Finset ι
hi : i ∉ u
IH :
  (∀ i ∈ u, ContDiffOn 𝕜 N (f i) s) →
    ∀ {n : ℕ},
      ↑n ≤ N →
        ‖iteratedFDerivWithin 𝕜 n (fun x => ∏ j ∈ u, f j x) s x‖ ≤
          ∑ p ∈ u.sym n, ↑(↑p).multinomial * ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
n : ℕ
hn : ↑n ≤ N
hf : ContDiffOn 𝕜 N (f i) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 N (f a) s
⊢ ∀ i_1 ∈ Finset.univ,
    ↑(↑↑i_1).multinomial * ∏ j ∈ insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑↑i_1) (f j) s x‖ =
      ((fun v => ↑v.multinomial * ∏ j ∈ insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j v) (f j) s x‖) ∘
          Sym.toMultiset ∘ Subtype.val ∘ ⇑(Finset.symInsertEquiv hi).symm ∘ ⇑(Finset.symInsertEquiv hi))
        i_1

Tactic:
simp

Result:
no goals