-- Mathlib/Analysis/Calculus/ContDiff/Operations.lean
theorem iteratedFDerivWithin_sum_apply {ι : Type*} {f : ι → E → F} {u : Finset ι} {i : ℕ} {x : E}
    (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) (h : ∀ j ∈ u, ContDiffWithinAt 𝕜 i (f j) s x) :
    iteratedFDerivWithin 𝕜 i (∑ j ∈ u, f j ·) s x =
      ∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x

Proof state:
case cons
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
ι : Type u_3
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
a : ι
u : Finset ι
ha : a ∉ u
IH :
  (∀ j ∈ u, ContDiffWithinAt 𝕜 (↑i) (f j) s x) →
    iteratedFDerivWithin 𝕜 i (fun x => ∑ j ∈ u, f j x) s x = ∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x
h : ContDiffWithinAt 𝕜 (↑i) (f a) s x ∧ ∀ a ∈ u, ContDiffWithinAt 𝕜 (↑i) (f a) s x
⊢ iteratedFDerivWithin 𝕜 i (fun x => f a x + ∑ j ∈ u, f j x) s x =
    iteratedFDerivWithin 𝕜 i (f a) s x + ∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x

Tactic:
rw [iteratedFDerivWithin_add_apply' h.1 (ContDiffWithinAt.sum h.2) hs hx, IH h.2]

Result:
no goals

Proof state:
case empty
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
ι : Type u_3
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : ∀ j ∈ ∅, ContDiffWithinAt 𝕜 (↑i) (f j) s x
⊢ iteratedFDerivWithin 𝕜 i (fun x => ∑ j ∈ ∅, f j x) s x = ∑ j ∈ ∅, iteratedFDerivWithin 𝕜 i (f j) s x

Tactic:
ext

Result:
case empty.H
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
ι : Type u_3
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : ∀ j ∈ ∅, ContDiffWithinAt 𝕜 (↑i) (f j) s x
x✝ : Fin i → E
⊢ (iteratedFDerivWithin 𝕜 i (fun x => ∑ j ∈ ∅, f j x) s x) x✝ = (∑ j ∈ ∅, iteratedFDerivWithin 𝕜 i (f j) s x) x✝

Proof state:
case cons
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
ι : Type u_3
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
a : ι
u : Finset ι
ha : a ∉ u
IH :
  (∀ j ∈ u, ContDiffWithinAt 𝕜 (↑i) (f j) s x) →
    iteratedFDerivWithin 𝕜 i (fun x => ∑ j ∈ u, f j x) s x = ∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x
h : ∀ j ∈ Finset.cons a u ha, ContDiffWithinAt 𝕜 (↑i) (f j) s x
⊢ iteratedFDerivWithin 𝕜 i (fun x => ∑ j ∈ Finset.cons a u ha, f j x) s x =
    ∑ j ∈ Finset.cons a u ha, iteratedFDerivWithin 𝕜 i (f j) s x

Tactic:
simp only [Finset.mem_cons, forall_eq_or_imp] at h

Result:
case cons
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
ι : Type u_3
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
a : ι
u : Finset ι
ha : a ∉ u
IH :
  (∀ j ∈ u, ContDiffWithinAt 𝕜 (↑i) (f j) s x) →
    iteratedFDerivWithin 𝕜 i (fun x => ∑ j ∈ u, f j x) s x = ∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x
h : ContDiffWithinAt 𝕜 (↑i) (f a) s x ∧ ∀ a ∈ u, ContDiffWithinAt 𝕜 (↑i) (f a) s x
⊢ iteratedFDerivWithin 𝕜 i (fun x => ∑ j ∈ Finset.cons a u ha, f j x) s x =
    ∑ j ∈ Finset.cons a u ha, iteratedFDerivWithin 𝕜 i (f j) s x

Proof state:
case empty.H
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
ι : Type u_3
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : ∀ j ∈ ∅, ContDiffWithinAt 𝕜 (↑i) (f j) s x
x✝ : Fin i → E
⊢ (iteratedFDerivWithin 𝕜 i (fun x => ∑ j ∈ ∅, f j x) s x) x✝ = (∑ j ∈ ∅, iteratedFDerivWithin 𝕜 i (f j) s x) x✝

Tactic:
simp [hs, hx]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
ι : Type u_3
f : ι → E → F
u : Finset ι
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : ∀ j ∈ u, ContDiffWithinAt 𝕜 (↑i) (f j) s x
⊢ iteratedFDerivWithin 𝕜 i (fun x => ∑ j ∈ u, f j x) s x = ∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x

Tactic:
induction u using Finset.cons_induction with
| empty => ext; simp [hs, hx]
| cons a u ha IH =>
  simp only [Finset.mem_cons, forall_eq_or_imp] at h
  simp only [Finset.sum_cons]
  rw [iteratedFDerivWithin_add_apply' h.1 (ContDiffWithinAt.sum h.2) hs hx, IH h.2]

Result:
no goals

Proof state:
case cons
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
ι : Type u_3
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
a : ι
u : Finset ι
ha : a ∉ u
IH :
  (∀ j ∈ u, ContDiffWithinAt 𝕜 (↑i) (f j) s x) →
    iteratedFDerivWithin 𝕜 i (fun x => ∑ j ∈ u, f j x) s x = ∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x
h : ContDiffWithinAt 𝕜 (↑i) (f a) s x ∧ ∀ a ∈ u, ContDiffWithinAt 𝕜 (↑i) (f a) s x
⊢ iteratedFDerivWithin 𝕜 i (fun x => ∑ j ∈ Finset.cons a u ha, f j x) s x =
    ∑ j ∈ Finset.cons a u ha, iteratedFDerivWithin 𝕜 i (f j) s x

Tactic:
simp only [Finset.sum_cons]

Result:
case cons
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
ι : Type u_3
f : ι → E → F
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
a : ι
u : Finset ι
ha : a ∉ u
IH :
  (∀ j ∈ u, ContDiffWithinAt 𝕜 (↑i) (f j) s x) →
    iteratedFDerivWithin 𝕜 i (fun x => ∑ j ∈ u, f j x) s x = ∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x
h : ContDiffWithinAt 𝕜 (↑i) (f a) s x ∧ ∀ a ∈ u, ContDiffWithinAt 𝕜 (↑i) (f a) s x
⊢ iteratedFDerivWithin 𝕜 i (fun x => f a x + ∑ j ∈ u, f j x) s x =
    iteratedFDerivWithin 𝕜 i (f a) s x + ∑ j ∈ u, iteratedFDerivWithin 𝕜 i (f j) s x