simp only [Finset.sum_insert ha]
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
ι : Type u_3
inst✝ : DecidableEq ι
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
a : ι
u : Finset ι
ha : a ∉ u
IH :
  (∀ j ∈ u, ContDiffOn 𝕜 (↑i) (f j) s) →
    iteratedFDerivWithin 𝕜 i (fun x => ∑ j in u, f j x) s x = ∑ j in u, iteratedFDerivWithin 𝕜 i (f j) s x
h : ContDiffOn 𝕜 (↑i) (f a) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 (↑i) (f a) s
⊢ iteratedFDerivWithin 𝕜 i (fun x => ∑ j in insert a u, f j x) s x =
    ∑ j in insert a u, iteratedFDerivWithin 𝕜 i (f j) s x
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
ι : Type u_3
inst✝ : DecidableEq ι
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
a : ι
u : Finset ι
ha : a ∉ u
IH :
  (∀ j ∈ u, ContDiffOn 𝕜 (↑i) (f j) s) →
    iteratedFDerivWithin 𝕜 i (fun x => ∑ j in u, f j x) s x = ∑ j in u, iteratedFDerivWithin 𝕜 i (f j) s x
h : ContDiffOn 𝕜 (↑i) (f a) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 (↑i) (f a) s
⊢ iteratedFDerivWithin 𝕜 i (fun x => f a x + ∑ j in u, f j x) s x =
    iteratedFDerivWithin 𝕜 i (f a) s x + ∑ j in u, iteratedFDerivWithin 𝕜 i (f j) s x