Theorem: norm_iteratedFDerivWithin_prod_le (ForML/FDerivProd.lean)

State before:
case empty
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
hf : ∀ i ∈ ∅, ContDiffOn 𝕜 N (f i) s
n : ℕ
hn : ↑n ≤ N
⊢ ‖iteratedFDerivWithin 𝕜 n (fun x => ∏ j in ∅, f j x) s x‖ ≤
    ∑ p in Finset.sym ∅ n,
      ↑(Multiset.multinomial ↑p) * ∏ j in ∅, ‖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 _ _ hs hx]
State after:
no goals

State before:
case empty.zero
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
hf : ∀ i ∈ ∅, ContDiffOn 𝕜 N (f i) s
hn : ↑Nat.zero ≤ N
⊢ ‖iteratedFDerivWithin 𝕜 Nat.zero (fun x => ∏ j in ∅, f j x) s x‖ ≤
    ∑ p in Finset.sym ∅ Nat.zero,
      ↑(Multiset.multinomial ↑p) * ∏ j in ∅, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
Tactic:
simp [Sym.eq_nil_of_card_zero]
State after:
no goals

State before:
case empty.succ
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
hf : ∀ i ∈ ∅, ContDiffOn 𝕜 N (f i) s
n : ℕ
hn : ↑(Nat.succ n) ≤ N
⊢ ‖iteratedFDerivWithin 𝕜 (Nat.succ n) (fun x => ∏ j in ∅, f j x) s x‖ ≤
    ∑ p in Finset.sym ∅ (Nat.succ n),
      ↑(Multiset.multinomial ↑p) * ∏ j in ∅, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
Tactic:
simp [iteratedFDerivWithin_succ_const _ _ hs hx]
State after:
no goals

State before:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞
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 in u, f j x) s x‖ ≤
          ∑ p in Finset.sym u n,
            ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
hf : ∀ i_1 ∈ insert i u, ContDiffOn 𝕜 N (f i_1) s
n : ℕ
hn : ↑n ≤ N
⊢ ‖iteratedFDerivWithin 𝕜 n (fun x => ∏ j in insert i u, f j x) s x‖ ≤
    ∑ p in Finset.sym (insert i u) n,
      ↑(Multiset.multinomial ↑p) * ∏ j in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
Tactic:
conv => lhs; simp only [Finset.prod_insert hi]
State after:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞
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 in u, f j x) s x‖ ≤
          ∑ p in Finset.sym u n,
            ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
hf : ∀ i_1 ∈ insert i u, ContDiffOn 𝕜 N (f i_1) s
n : ℕ
hn : ↑n ≤ N
⊢ ‖iteratedFDerivWithin 𝕜 n (fun x => f i x * ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym (insert i u) n,
      ↑(Multiset.multinomial ↑p) * ∏ j in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖

State before:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞
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 in u, f j x) s x‖ ≤
          ∑ p in Finset.sym u n,
            ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
hf : ∀ i_1 ∈ insert i u, ContDiffOn 𝕜 N (f i_1) s
n : ℕ
hn : ↑n ≤ N
⊢ ‖iteratedFDerivWithin 𝕜 n (fun x => f i x * ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym (insert i u) n,
      ↑(Multiset.multinomial ↑p) * ∏ j in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
Tactic:
simp only [Finset.mem_insert, forall_eq_or_imp] at hf
State after:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞
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 in u, f j x) s x‖ ≤
          ∑ p in Finset.sym u n,
            ↑(Multiset.multinomial ↑p) * ∏ j in 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
⊢ ‖iteratedFDerivWithin 𝕜 n (fun x => f i x * ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym (insert i u) n,
      ↑(Multiset.multinomial ↑p) * ∏ j in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖

State before:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞
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 in u, f j x) s x‖ ≤
          ∑ p in Finset.sym u n,
            ↑(Multiset.multinomial ↑p) * ∏ j in 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
⊢ ‖iteratedFDerivWithin 𝕜 n (fun x => f i x * ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym (insert i u) n,
      ↑(Multiset.multinomial ↑p) * ∏ j in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
Tactic:
refine le_trans (norm_iteratedFDerivWithin_mul_le hf.1 (contDiffOn_prod hf.2) hs hx hn) ?_
State after:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞
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 in u, f j x) s x‖ ≤
          ∑ p in Finset.sym u n,
            ↑(Multiset.multinomial ↑p) * ∏ j in 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 in Finset.range (n + 1),
      ↑(Nat.choose n i_1) * ‖iteratedFDerivWithin 𝕜 i_1 (f i) s x‖ *
        ‖iteratedFDerivWithin 𝕜 (n - i_1) (fun y => ∏ i in u, f i y) s x‖ ≤
    ∑ p in Finset.sym (insert i u) n,
      ↑(Multiset.multinomial ↑p) * ∏ j in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖

State before:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞
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 in u, f j x) s x‖ ≤
          ∑ p in Finset.sym u n,
            ↑(Multiset.multinomial ↑p) * ∏ j in 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 in Finset.range (n + 1),
      ↑(Nat.choose n i_1) * ‖iteratedFDerivWithin 𝕜 i_1 (f i) s x‖ *
        ‖iteratedFDerivWithin 𝕜 (n - i_1) (fun y => ∏ i in u, f i y) s x‖ ≤
    ∑ p in Finset.sym (insert i u) n,
      ↑(Multiset.multinomial ↑p) * ∏ j in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
Tactic:
rw [← Finset.sum_coe_sort (Finset.sym _ _)]
State after:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞
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 in u, f j x) s x‖ ≤
          ∑ p in Finset.sym u n,
            ↑(Multiset.multinomial ↑p) * ∏ j in 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 in Finset.range (n + 1),
      ↑(Nat.choose n i_1) * ‖iteratedFDerivWithin 𝕜 i_1 (f i) s x‖ *
        ‖iteratedFDerivWithin 𝕜 (n - i_1) (fun y => ∏ i in u, f i y) s x‖ ≤
    ∑ i_1 : { x // x ∈ Finset.sym (insert i u) n },
      ↑(Multiset.multinomial ↑↑i_1) * ∏ j in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑↑i_1) (f j) s x‖

State before:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞
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 in u, f j x) s x‖ ≤
          ∑ p in Finset.sym u n,
            ↑(Multiset.multinomial ↑p) * ∏ j in 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 in Finset.range (n + 1),
      ↑(Nat.choose n i_1) * ‖iteratedFDerivWithin 𝕜 i_1 (f i) s x‖ *
        ‖iteratedFDerivWithin 𝕜 (n - i_1) (fun y => ∏ i in u, f i y) s x‖ ≤
    ∑ i_1 : { x // x ∈ Finset.sym (insert i u) n },
      ↑(Multiset.multinomial ↑↑i_1) * ∏ j in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑↑i_1) (f j) s x‖
Tactic:
rw [Finset.sum_equiv (Finset.symInsertEquiv hi) (t := Finset.univ)
  (g := (fun v ↦ v.multinomial *
      ∏ j in 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)]
State after:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞
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 in u, f j x) s x‖ ≤
          ∑ p in Finset.sym u n,
            ↑(Multiset.multinomial ↑p) * ∏ j in 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 in Finset.range (n + 1),
      ↑(Nat.choose n i_1) * ‖iteratedFDerivWithin 𝕜 i_1 (f i) s x‖ *
        ‖iteratedFDerivWithin 𝕜 (n - i_1) (fun y => ∏ i in u, f i y) s x‖ ≤
    ∑ i_1 : (i : Fin (n + 1)) × { x // x ∈ Finset.sym u (n - ↑i) },
      ((fun v =>
            ↑(Multiset.multinomial v) * ∏ j in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j v) (f j) s x‖) ∘
          Sym.toMultiset ∘ Subtype.val ∘ ⇑(Finset.symInsertEquiv hi).symm)
        i_1

State before:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞
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 in u, f j x) s x‖ ≤
          ∑ p in Finset.sym u n,
            ↑(Multiset.multinomial ↑p) * ∏ j in 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 in Finset.range (n + 1),
      ↑(Nat.choose n i_1) * ‖iteratedFDerivWithin 𝕜 i_1 (f i) s x‖ *
        ‖iteratedFDerivWithin 𝕜 (n - i_1) (fun y => ∏ i in u, f i y) s x‖ ≤
    ∑ i_1 : (i : Fin (n + 1)) × { x // x ∈ Finset.sym u (n - ↑i) },
      ((fun v =>
            ↑(Multiset.multinomial v) * ∏ j in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j v) (f j) s x‖) ∘
          Sym.toMultiset ∘ Subtype.val ∘ ⇑(Finset.symInsertEquiv hi).symm)
        i_1
Tactic:
rw [← Finset.univ_sigma_univ, Finset.sum_sigma, Finset.sum_range]
State after:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞
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 in u, f j x) s x‖ ≤
          ∑ p in Finset.sym u n,
            ↑(Multiset.multinomial ↑p) * ∏ j in 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 : Fin (n + 1),
      ↑(Nat.choose n ↑i_1) * ‖iteratedFDerivWithin 𝕜 (↑i_1) (f i) s x‖ *
        ‖iteratedFDerivWithin 𝕜 (n - ↑i_1) (fun y => ∏ i in u, f i y) s x‖ ≤
    ∑ a : Fin (n + 1),
      ∑ s_1 : { x // x ∈ Finset.sym u (n - ↑a) },
        ((fun v =>
              ↑(Multiset.multinomial v) * ∏ j in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j v) (f j) s x‖) ∘
            Sym.toMultiset ∘ Subtype.val ∘ ⇑(Finset.symInsertEquiv hi).symm)
          { fst := a, snd := s_1 }

State before:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞
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 in u, f j x) s x‖ ≤
          ∑ p in Finset.sym u n,
            ↑(Multiset.multinomial ↑p) * ∏ j in 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 : Fin (n + 1),
      ↑(Nat.choose n ↑i_1) * ‖iteratedFDerivWithin 𝕜 (↑i_1) (f i) s x‖ *
        ‖iteratedFDerivWithin 𝕜 (n - ↑i_1) (fun y => ∏ i in u, f i y) s x‖ ≤
    ∑ a : Fin (n + 1),
      ∑ s_1 : { x // x ∈ Finset.sym u (n - ↑a) },
        ((fun v =>
              ↑(Multiset.multinomial v) * ∏ j in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j v) (f j) s x‖) ∘
            Sym.toMultiset ∘ Subtype.val ∘ ⇑(Finset.symInsertEquiv hi).symm)
          { fst := a, snd := s_1 }
Tactic:
simp only [comp_apply, Finset.symInsertEquiv_symm_apply_coe]
State after:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞
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 in u, f j x) s x‖ ≤
          ∑ p in Finset.sym u n,
            ↑(Multiset.multinomial ↑p) * ∏ j in 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
⊢ ∑ x_1 : Fin (n + 1),
      ↑(Nat.choose n ↑x_1) * ‖iteratedFDerivWithin 𝕜 (↑x_1) (f i) s x‖ *
        ‖iteratedFDerivWithin 𝕜 (n - ↑x_1) (fun y => ∏ i in u, f i y) s x‖ ≤
    ∑ x_1 : Fin (n + 1),
      ∑ x_2 : { x // x ∈ Finset.sym u (n - ↑x_1) },
        ↑(Multiset.multinomial ↑(Sym.fill i x_1 ↑x_2)) *
          ∏ x_3 in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_3 ↑(Sym.fill i x_1 ↑x_2)) (f x_3) s x‖

State before:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞
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 in u, f j x) s x‖ ≤
          ∑ p in Finset.sym u n,
            ↑(Multiset.multinomial ↑p) * ∏ j in 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
⊢ ∑ x_1 : Fin (n + 1),
      ↑(Nat.choose n ↑x_1) * ‖iteratedFDerivWithin 𝕜 (↑x_1) (f i) s x‖ *
        ‖iteratedFDerivWithin 𝕜 (n - ↑x_1) (fun y => ∏ i in u, f i y) s x‖ ≤
    ∑ x_1 : Fin (n + 1),
      ∑ x_2 : { x // x ∈ Finset.sym u (n - ↑x_1) },
        ↑(Multiset.multinomial ↑(Sym.fill i x_1 ↑x_2)) *
          ∏ x_3 in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_3 ↑(Sym.fill i x_1 ↑x_2)) (f x_3) s x‖
Tactic:
refine Finset.sum_le_sum ?_
State after:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞
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 in u, f j x) s x‖ ≤
          ∑ p in Finset.sym u n,
            ↑(Multiset.multinomial ↑p) * ∏ j in 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,
    ↑(Nat.choose n ↑i_1) * ‖iteratedFDerivWithin 𝕜 (↑i_1) (f i) s x‖ *
        ‖iteratedFDerivWithin 𝕜 (n - ↑i_1) (fun y => ∏ i in u, f i y) s x‖ ≤
      ∑ x_1 : { x // x ∈ Finset.sym u (n - ↑i_1) },
        ↑(Multiset.multinomial ↑(Sym.fill i i_1 ↑x_1)) *
          ∏ x_2 in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_2 ↑(Sym.fill i i_1 ↑x_1)) (f x_2) s x‖

State before:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞
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 in u, f j x) s x‖ ≤
          ∑ p in Finset.sym u n,
            ↑(Multiset.multinomial ↑p) * ∏ j in 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,
    ↑(Nat.choose n ↑i_1) * ‖iteratedFDerivWithin 𝕜 (↑i_1) (f i) s x‖ *
        ‖iteratedFDerivWithin 𝕜 (n - ↑i_1) (fun y => ∏ i in u, f i y) s x‖ ≤
      ∑ x_1 : { x // x ∈ Finset.sym u (n - ↑i_1) },
        ↑(Multiset.multinomial ↑(Sym.fill i i_1 ↑x_1)) *
          ∏ x_2 in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_2 ↑(Sym.fill i i_1 ↑x_1)) (f x_2) s x‖
Tactic:
simp only [Finset.mem_univ, forall_true_left]
State after:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞
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 in u, f j x) s x‖ ≤
          ∑ p in Finset.sym u n,
            ↑(Multiset.multinomial ↑p) * ∏ j in 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 : Fin (n + 1)),
    ↑(Nat.choose n ↑i_1) * ‖iteratedFDerivWithin 𝕜 (↑i_1) (f i) s x‖ *
        ‖iteratedFDerivWithin 𝕜 (n - ↑i_1) (fun y => ∏ i in u, f i y) s x‖ ≤
      ∑ x_1 : { x // x ∈ Finset.sym u (n - ↑i_1) },
        ↑(Multiset.multinomial ↑(Sym.fill i i_1 ↑x_1)) *
          ∏ x_2 in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_2 ↑(Sym.fill i i_1 ↑x_1)) (f x_2) s x‖

State before:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞
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 in u, f j x) s x‖ ≤
          ∑ p in Finset.sym u n,
            ↑(Multiset.multinomial ↑p) * ∏ j in 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 : Fin (n + 1)),
    ↑(Nat.choose n ↑i_1) * ‖iteratedFDerivWithin 𝕜 (↑i_1) (f i) s x‖ *
        ‖iteratedFDerivWithin 𝕜 (n - ↑i_1) (fun y => ∏ i in u, f i y) s x‖ ≤
      ∑ x_1 : { x // x ∈ Finset.sym u (n - ↑i_1) },
        ↑(Multiset.multinomial ↑(Sym.fill i i_1 ↑x_1)) *
          ∏ x_2 in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_2 ↑(Sym.fill i i_1 ↑x_1)) (f x_2) s x‖
Tactic:
intro m
State after:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞
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 in u, f j x) s x‖ ≤
          ∑ p in Finset.sym u n,
            ↑(Multiset.multinomial ↑p) * ∏ j in 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
m : Fin (n + 1)
⊢ ↑(Nat.choose n ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
      ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun y => ∏ i in u, f i y) s x‖ ≤
    ∑ x_1 : { x // x ∈ Finset.sym u (n - ↑m) },
      ↑(Multiset.multinomial ↑(Sym.fill i m ↑x_1)) *
        ∏ x_2 in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_2 ↑(Sym.fill i m ↑x_1)) (f x_2) s x‖

State before:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞
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 in u, f j x) s x‖ ≤
          ∑ p in Finset.sym u n,
            ↑(Multiset.multinomial ↑p) * ∏ j in 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
m : Fin (n + 1)
⊢ ↑(Nat.choose n ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
      ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun y => ∏ i in u, f i y) s x‖ ≤
    ∑ x_1 : { x // x ∈ Finset.sym u (n - ↑m) },
      ↑(Multiset.multinomial ↑(Sym.fill i m ↑x_1)) *
        ∏ x_2 in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_2 ↑(Sym.fill i m ↑x_1)) (f x_2) s x‖
Tactic:
specialize IH hf.2 (n := n - m) (le_trans (WithTop.coe_le_coe.mpr (n.sub_le m)) hn)
State after:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : 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)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
⊢ ↑(Nat.choose n ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
      ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun y => ∏ i in u, f i y) s x‖ ≤
    ∑ x_1 : { x // x ∈ Finset.sym u (n - ↑m) },
      ↑(Multiset.multinomial ↑(Sym.fill i m ↑x_1)) *
        ∏ x_2 in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_2 ↑(Sym.fill i m ↑x_1)) (f x_2) s x‖

State before:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : 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)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
⊢ ↑(Nat.choose n ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
      ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun y => ∏ i in u, f i y) s x‖ ≤
    ∑ x_1 : { x // x ∈ Finset.sym u (n - ↑m) },
      ↑(Multiset.multinomial ↑(Sym.fill i m ↑x_1)) *
        ∏ x_2 in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_2 ↑(Sym.fill i m ↑x_1)) (f x_2) s x‖
Tactic:
refine le_trans (mul_le_mul_of_nonneg_left IH (by simp [mul_nonneg])) ?_
State after:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : 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)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
⊢ ↑(Nat.choose n ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
      ∑ p in Finset.sym u (n - ↑m),
        ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖ ≤
    ∑ x_1 : { x // x ∈ Finset.sym u (n - ↑m) },
      ↑(Multiset.multinomial ↑(Sym.fill i m ↑x_1)) *
        ∏ x_2 in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_2 ↑(Sym.fill i m ↑x_1)) (f x_2) s x‖

State before:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : 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)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
⊢ ↑(Nat.choose n ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
      ∑ p in Finset.sym u (n - ↑m),
        ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖ ≤
    ∑ x_1 : { x // x ∈ Finset.sym u (n - ↑m) },
      ↑(Multiset.multinomial ↑(Sym.fill i m ↑x_1)) *
        ∏ x_2 in 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]
State after:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : 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)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
⊢ ∑ i_1 : { x // x ∈ Finset.sym u (n - ↑m) },
      ↑(Nat.choose n ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
        (↑(Multiset.multinomial ↑↑i_1) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑↑i_1) (f j) s x‖) ≤
    ∑ x_1 : { x // x ∈ Finset.sym u (n - ↑m) },
      ↑(Multiset.multinomial ↑(Sym.fill i m ↑x_1)) *
        ∏ x_2 in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_2 ↑(Sym.fill i m ↑x_1)) (f x_2) s x‖

State before:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : 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)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
⊢ ∑ i_1 : { x // x ∈ Finset.sym u (n - ↑m) },
      ↑(Nat.choose n ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
        (↑(Multiset.multinomial ↑↑i_1) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑↑i_1) (f j) s x‖) ≤
    ∑ x_1 : { x // x ∈ Finset.sym u (n - ↑m) },
      ↑(Multiset.multinomial ↑(Sym.fill i m ↑x_1)) *
        ∏ x_2 in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_2 ↑(Sym.fill i m ↑x_1)) (f x_2) s x‖
Tactic:
refine Finset.sum_le_sum ?_
State after:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : 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)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
⊢ ∀ i_1 ∈ Finset.univ,
    ↑(Nat.choose n ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
        (↑(Multiset.multinomial ↑↑i_1) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑↑i_1) (f j) s x‖) ≤
      ↑(Multiset.multinomial ↑(Sym.fill i m ↑i_1)) *
        ∏ x_1 in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑(Sym.fill i m ↑i_1)) (f x_1) s x‖

State before:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : 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)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
⊢ ∀ i_1 ∈ Finset.univ,
    ↑(Nat.choose n ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
        (↑(Multiset.multinomial ↑↑i_1) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑↑i_1) (f j) s x‖) ≤
      ↑(Multiset.multinomial ↑(Sym.fill i m ↑i_1)) *
        ∏ x_1 in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑(Sym.fill i m ↑i_1)) (f x_1) s x‖
Tactic:
simp only [Finset.mem_univ, forall_true_left, Subtype.forall, Finset.mem_sym_iff]
State after:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : 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)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
⊢ ∀ (a : Sym ι (n - ↑m)),
    (∀ a_1 ∈ a, a_1 ∈ u) →
      ↑(Nat.choose n ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
          (↑(Multiset.multinomial ↑a) * ∏ x_1 in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑a) (f x_1) s x‖) ≤
        ↑(Multiset.multinomial ↑(Sym.fill i m a)) *
          ∏ x_1 in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑(Sym.fill i m a)) (f x_1) s x‖

State before:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : 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)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
⊢ ∀ (a : Sym ι (n - ↑m)),
    (∀ a_1 ∈ a, a_1 ∈ u) →
      ↑(Nat.choose n ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
          (↑(Multiset.multinomial ↑a) * ∏ x_1 in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑a) (f x_1) s x‖) ≤
        ↑(Multiset.multinomial ↑(Sym.fill i m a)) *
          ∏ x_1 in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑(Sym.fill i m a)) (f x_1) s x‖
Tactic:
intro p hp
State after:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : 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)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
⊢ ↑(Nat.choose n ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
      (↑(Multiset.multinomial ↑p) * ∏ x_1 in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑p) (f x_1) s x‖) ≤
    ↑(Multiset.multinomial ↑(Sym.fill i m p)) *
      ∏ x_1 in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑(Sym.fill i m p)) (f x_1) s x‖

State before:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : 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)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
⊢ ↑(Nat.choose n ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
      (↑(Multiset.multinomial ↑p) * ∏ x_1 in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑p) (f x_1) s x‖) ≤
    ↑(Multiset.multinomial ↑(Sym.fill i m p)) *
      ∏ x_1 in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑(Sym.fill i m p)) (f x_1) s x‖
Tactic:
refine le_of_eq ?_
State after:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : 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)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
⊢ ↑(Nat.choose n ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
      (↑(Multiset.multinomial ↑p) * ∏ x_1 in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑p) (f x_1) s x‖) =
    ↑(Multiset.multinomial ↑(Sym.fill i m p)) *
      ∏ x_1 in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑(Sym.fill i m p)) (f x_1) s x‖

State before:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : 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)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
⊢ ↑(Nat.choose n ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
      (↑(Multiset.multinomial ↑p) * ∏ x_1 in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑p) (f x_1) s x‖) =
    ↑(Multiset.multinomial ↑(Sym.fill i m p)) *
      ∏ x_1 in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑(Sym.fill i m p)) (f x_1) s x‖
Tactic:
rw [Finset.prod_insert hi]
State after:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : 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)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
⊢ ↑(Nat.choose n ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
      (↑(Multiset.multinomial ↑p) * ∏ x_1 in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑p) (f x_1) s x‖) =
    ↑(Multiset.multinomial ↑(Sym.fill i m p)) *
      (‖iteratedFDerivWithin 𝕜 (Multiset.count i ↑(Sym.fill i m p)) (f i) s x‖ *
        ∏ x_1 in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑(Sym.fill i m p)) (f x_1) s x‖)

State before:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : 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)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
⊢ ↑(Nat.choose n ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
      (↑(Multiset.multinomial ↑p) * ∏ x_1 in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑p) (f x_1) s x‖) =
    ↑(Multiset.multinomial ↑(Sym.fill i m p)) *
      (‖iteratedFDerivWithin 𝕜 (Multiset.count i ↑(Sym.fill i m p)) (f i) s x‖ *
        ∏ x_1 in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑(Sym.fill i m p)) (f x_1) s x‖)
Tactic:
have hip : i ∉ p := fun h ↦ hi <| hp i h
State after:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : 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)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
hip : i ∉ p
⊢ ↑(Nat.choose n ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
      (↑(Multiset.multinomial ↑p) * ∏ x_1 in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑p) (f x_1) s x‖) =
    ↑(Multiset.multinomial ↑(Sym.fill i m p)) *
      (‖iteratedFDerivWithin 𝕜 (Multiset.count i ↑(Sym.fill i m p)) (f i) s x‖ *
        ∏ x_1 in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑(Sym.fill i m p)) (f x_1) s x‖)

State before:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : 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)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
hip : i ∉ p
⊢ ↑(Nat.choose n ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
      (↑(Multiset.multinomial ↑p) * ∏ x_1 in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑p) (f x_1) s x‖) =
    ↑(Multiset.multinomial ↑(Sym.fill i m p)) *
      (‖iteratedFDerivWithin 𝕜 (Multiset.count i ↑(Sym.fill i m p)) (f i) s x‖ *
        ∏ x_1 in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑(Sym.fill i m p)) (f x_1) s x‖)
Tactic:
rw [Sym.count_coe_fill_self_of_not_mem hip, Sym.multinomial_coe_fill_of_not_mem hip]
State after:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : 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)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
hip : i ∉ p
⊢ ↑(Nat.choose n ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
      (↑(Multiset.multinomial ↑p) * ∏ x_1 in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑p) (f x_1) s x‖) =
    ↑(Nat.choose n ↑m * Multiset.multinomial ↑p) *
      (‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
        ∏ x_1 in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑(Sym.fill i m p)) (f x_1) s x‖)

State before:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : 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)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
hip : i ∉ p
⊢ ↑(Nat.choose n ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
      (↑(Multiset.multinomial ↑p) * ∏ x_1 in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑p) (f x_1) s x‖) =
    ↑(Nat.choose n ↑m * Multiset.multinomial ↑p) *
      (‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
        ∏ x_1 in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑(Sym.fill i m p)) (f x_1) s x‖)
Tactic:
suffices : ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j p) (f j) s x‖ =
    ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j (Sym.fill i m p)) (f j) s x‖
State after:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : 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)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
hip : i ∉ p
this :
  ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖ =
    ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑(Sym.fill i m p)) (f j) s x‖
⊢ ↑(Nat.choose n ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
      (↑(Multiset.multinomial ↑p) * ∏ x_1 in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑p) (f x_1) s x‖) =
    ↑(Nat.choose n ↑m * Multiset.multinomial ↑p) *
      (‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
        ∏ x_1 in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑(Sym.fill i m p)) (f x_1) s x‖)

case this
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : 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)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
hip : i ∉ p
⊢ ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖ =
    ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑(Sym.fill i m p)) (f j) s x‖

State before:
case this
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : 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)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
hip : i ∉ p
⊢ ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖ =
    ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑(Sym.fill i m p)) (f j) s x‖
Tactic:
refine Finset.prod_congr rfl ?_
State after:
case this
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : 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)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in 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‖

State before:
case this
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : 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)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in 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‖
Tactic:
intro j hj
State after:
case this
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : 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)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
hip : i ∉ p
j : ι
hj : j ∈ u
⊢ ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖ =
    ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑(Sym.fill i m p)) (f j) s x‖

State before:
case this
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : 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)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
hip : i ∉ p
j : ι
hj : j ∈ u
⊢ ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖ =
    ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑(Sym.fill i m p)) (f j) s x‖
Tactic:
have hji : j ≠ i := fun h ↦ hi <| by simpa [h] using hj
State after:
case this
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : 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)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
hip : i ∉ p
j : ι
hj : j ∈ u
hji : j ≠ i
⊢ ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖ =
    ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑(Sym.fill i m p)) (f j) s x‖

State before:
case this
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : 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)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
hip : i ∉ p
j : ι
hj : j ∈ u
hji : j ≠ i
⊢ ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖ =
    ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑(Sym.fill i m p)) (f j) s x‖
Tactic:
rw [Sym.count_coe_fill_of_ne hji]
State after:
no goals

State before:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞
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 in u, f j x) s x‖ ≤
          ∑ p in Finset.sym u n,
            ↑(Multiset.multinomial ↑p) * ∏ j in 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 : { x // x ∈ Finset.sym (insert i u) n }), i_1 ∈ Finset.univ ↔ (Finset.symInsertEquiv hi) i_1 ∈ Finset.univ
Tactic:
simp
State after:
no goals

State before:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞
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 in u, f j x) s x‖ ≤
          ∑ p in Finset.sym u n,
            ↑(Multiset.multinomial ↑p) * ∏ j in 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,
    ↑(Multiset.multinomial ↑↑i_1) * ∏ j in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑↑i_1) (f j) s x‖ =
      ((fun v =>
            ↑(Multiset.multinomial v) * ∏ j in 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 only [← comp_apply (g := Finset.symInsertEquiv hi), comp.assoc]
State after:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞
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 in u, f j x) s x‖ ≤
          ∑ p in Finset.sym u n,
            ↑(Multiset.multinomial ↑p) * ∏ j in 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,
    ↑(Multiset.multinomial ↑↑i_1) *
        ∏ x_1 in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑↑i_1) (f x_1) s x‖ =
      ((fun v =>
            ↑(Multiset.multinomial v) *
              ∏ x_1 in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 v) (f x_1) s x‖) ∘
          Sym.toMultiset ∘ Subtype.val ∘ ⇑(Finset.symInsertEquiv hi).symm ∘ ⇑(Finset.symInsertEquiv hi))
        i_1

State before:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞
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 in u, f j x) s x‖ ≤
          ∑ p in Finset.sym u n,
            ↑(Multiset.multinomial ↑p) * ∏ j in 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,
    ↑(Multiset.multinomial ↑↑i_1) *
        ∏ x_1 in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑↑i_1) (f x_1) s x‖ =
      ((fun v =>
            ↑(Multiset.multinomial v) *
              ∏ x_1 in insert i u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 v) (f x_1) s x‖) ∘
          Sym.toMultiset ∘ Subtype.val ∘ ⇑(Finset.symInsertEquiv hi).symm ∘ ⇑(Finset.symInsertEquiv hi))
        i_1
Tactic:
simp
State after:
no goals

State before:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : 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)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
⊢ 0 ≤ ↑(Nat.choose n ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖
Tactic:
simp [mul_nonneg]
State after:
no goals

State before:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : 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)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
hip : i ∉ p
this :
  ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖ =
    ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑(Sym.fill i m p)) (f j) s x‖
⊢ ↑(Nat.choose n ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
      (↑(Multiset.multinomial ↑p) * ∏ x_1 in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑p) (f x_1) s x‖) =
    ↑(Nat.choose n ↑m * Multiset.multinomial ↑p) *
      (‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
        ∏ x_1 in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑(Sym.fill i m p)) (f x_1) s x‖)
Tactic:
rw [this, Nat.cast_mul]
State after:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : 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)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
hip : i ∉ p
this :
  ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖ =
    ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑(Sym.fill i m p)) (f j) s x‖
⊢ ↑(Nat.choose n ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
      (↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑(Sym.fill i m p)) (f j) s x‖) =
    ↑(Nat.choose n ↑m) * ↑(Multiset.multinomial ↑p) *
      (‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
        ∏ x_1 in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑(Sym.fill i m p)) (f x_1) s x‖)

State before:
case insert
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : 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)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
hip : i ∉ p
this :
  ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖ =
    ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑(Sym.fill i m p)) (f j) s x‖
⊢ ↑(Nat.choose n ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
      (↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑(Sym.fill i m p)) (f j) s x‖) =
    ↑(Nat.choose n ↑m) * ↑(Multiset.multinomial ↑p) *
      (‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
        ∏ x_1 in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑(Sym.fill i m p)) (f x_1) s x‖)
Tactic:
ring
State after:
no goals

State before:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
D : Type uD
inst✝¹³ : NormedAddCommGroup D
inst✝¹² : NormedSpace 𝕜 D
E : Type uE
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type uF
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type uG
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
X : Type u_2
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f✝ f₁ : E → F
g : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n✝ : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
A' : Type u_3
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : 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)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x => ∏ j in u, f j x) s x‖ ≤
    ∑ p in Finset.sym u (n - ↑m),
      ↑(Multiset.multinomial ↑p) * ∏ j in u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
hip : i ∉ p
j : ι
hj : j ∈ u
h : j = i
⊢ i ∈ u
Tactic:
simpa [h] using hj
State after:
no goals