-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
theorem iteratedFDeriv_zero_apply_diag : iteratedFDeriv 𝕜 0 f x = p 0

Proof state:
case H
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
x✝ : Fin 0 → E
⊢ (iteratedFDeriv 𝕜 0 f x) x✝ = (p 0) x✝

Tactic:
convert (h.hasSum <| EMetric.mem_ball_self h.r_pos).tsum_eq.symm

Result:
case h.e'_2
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
x✝ : Fin 0 → E
⊢ (iteratedFDeriv 𝕜 0 f x) x✝ = f (x + 0)

case h.e'_3
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
x✝ : Fin 0 → E
⊢ (p 0) x✝ = ∑' (b : ℕ), (p b) fun x => 0

Proof state:
case h.e'_3
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
x✝ : Fin 0 → E
⊢ (p 0) x✝ = (p 0) fun x => 0

Tactic:
exact congr(p 0 $(Subsingleton.elim _ _))

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
⊢ iteratedFDeriv 𝕜 0 f x = p 0

Tactic:
ext

Result:
case H
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
x✝ : Fin 0 → E
⊢ (iteratedFDeriv 𝕜 0 f x) x✝ = (p 0) x✝

Proof state:
case h.e'_2
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
x✝ : Fin 0 → E
⊢ (iteratedFDeriv 𝕜 0 f x) x✝ = f (x + 0)

Tactic:
rw [iteratedFDeriv_zero_apply, add_zero]

Result:
no goals

Proof state:
case h.e'_3
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
x✝ : Fin 0 → E
⊢ (p 0) x✝ = ∑' (b : ℕ), (p b) fun x => 0

Tactic:
rw [tsum_eq_single 0 fun n hn ↦ by haveI := NeZero.mk hn; exact (p n).map_zero]

Result:
case h.e'_3
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
x✝ : Fin 0 → E
⊢ (p 0) x✝ = (p 0) fun x => 0

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
x✝ : Fin 0 → E
n : ℕ
hn : n ≠ 0
⊢ ((p n) fun x => 0) = 0

Tactic:
haveI := NeZero.mk hn

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
x✝ : Fin 0 → E
n : ℕ
hn : n ≠ 0
this : NeZero n
⊢ ((p n) fun x => 0) = 0

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
x✝ : Fin 0 → E
n : ℕ
hn : n ≠ 0
this : NeZero n
⊢ ((p n) fun x => 0) = 0

Tactic:
exact (p n).map_zero

Result:
no goals