-- Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean
lemma AnalyticAt.hasFPowerSeriesAt {𝕜 : Type*} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
    [CharZero 𝕜] {f : 𝕜 → 𝕜} {x : 𝕜} (h : AnalyticAt 𝕜 f x) :
    HasFPowerSeriesAt f
      (FormalMultilinearSeries.ofScalars 𝕜 (fun n ↦ iteratedDeriv n f x / n.factorial)) x

Proof state:
case h.e'_10.intro.h.H
𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
r : ENNReal
hpr : HasFPowerSeriesOnBall f p x r
n : ℕ
u : Fin n → 𝕜
⊢ (FormalMultilinearSeries.ofScalars 𝕜 (fun n => iteratedDeriv n f x / ↑n.factorial) n) u = (p n) u

Tactic:
have h_fact_smul := hpr.factorial_smul 1

Result:
case h.e'_10.intro.h.H
𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
r : ENNReal
hpr : HasFPowerSeriesOnBall f p x r
n : ℕ
u : Fin n → 𝕜
h_fact_smul : ∀ (n : ℕ), (n.factorial • (p n) fun x => 1) = (iteratedFDeriv 𝕜 n f x) fun x => 1
⊢ (FormalMultilinearSeries.ofScalars 𝕜 (fun n => iteratedDeriv n f x / ↑n.factorial) n) u = (p n) u

Proof state:
case h.e'_10.intro
𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
r : ENNReal
hpr : HasFPowerSeriesOnBall f p x r
⊢ (FormalMultilinearSeries.ofScalars 𝕜 fun n => iteratedDeriv n f x / ↑n.factorial) = p

Tactic:
ext n u

Result:
case h.e'_10.intro.h.H
𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
r : ENNReal
hpr : HasFPowerSeriesOnBall f p x r
n : ℕ
u : Fin n → 𝕜
⊢ (FormalMultilinearSeries.ofScalars 𝕜 (fun n => iteratedDeriv n f x / ↑n.factorial) n) u = (p n) u

Proof state:
case intro
𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
hp : HasFPowerSeriesAt f p x
⊢ HasFPowerSeriesAt f (FormalMultilinearSeries.ofScalars 𝕜 fun n => iteratedDeriv n f x / ↑n.factorial) x

Tactic:
convert hp

Result:
case h.e'_10
𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
hp : HasFPowerSeriesAt f p x
⊢ (FormalMultilinearSeries.ofScalars 𝕜 fun n => iteratedDeriv n f x / ↑n.factorial) = p

Proof state:
case h.e'_10.intro.h.H
𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
r : ENNReal
hpr : HasFPowerSeriesOnBall f p x r
n : ℕ
u : Fin n → 𝕜
h_fact_smul : ∀ (n : ℕ), ↑n.factorial * p.coeff n = (iteratedFDeriv 𝕜 n f x) fun x => 1
⊢ iteratedDeriv n f x / ↑n.factorial = p.coeff n ∨ ∏ i : Fin n, u i = 0

Tactic:
left

Result:
case h.e'_10.intro.h.H.h
𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
r : ENNReal
hpr : HasFPowerSeriesOnBall f p x r
n : ℕ
u : Fin n → 𝕜
h_fact_smul : ∀ (n : ℕ), ↑n.factorial * p.coeff n = (iteratedFDeriv 𝕜 n f x) fun x => 1
⊢ iteratedDeriv n f x / ↑n.factorial = p.coeff n

Proof state:
case h.e'_10.intro.h.H.h
𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
r : ENNReal
hpr : HasFPowerSeriesOnBall f p x r
n : ℕ
u : Fin n → 𝕜
h_fact_smul : ∀ (n : ℕ), ↑n.factorial * p.coeff n = (iteratedFDeriv 𝕜 n f x) fun x => 1
⊢ iteratedDeriv n f x / ↑n.factorial = p.coeff n

Tactic:
rw [div_eq_iff, mul_comm, h_fact_smul, ← iteratedDeriv_eq_iteratedFDeriv]

Result:
case h.e'_10.intro.h.H.h
𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
r : ENNReal
hpr : HasFPowerSeriesOnBall f p x r
n : ℕ
u : Fin n → 𝕜
h_fact_smul : ∀ (n : ℕ), ↑n.factorial * p.coeff n = (iteratedFDeriv 𝕜 n f x) fun x => 1
⊢ ↑n.factorial ≠ 0

Proof state:
case h.e'_10
𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
hp : HasFPowerSeriesAt f p x
⊢ (FormalMultilinearSeries.ofScalars 𝕜 fun n => iteratedDeriv n f x / ↑n.factorial) = p

Tactic:
obtain ⟨r, hpr⟩ := hp

Result:
case h.e'_10.intro
𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
r : ENNReal
hpr : HasFPowerSeriesOnBall f p x r
⊢ (FormalMultilinearSeries.ofScalars 𝕜 fun n => iteratedDeriv n f x / ↑n.factorial) = p

Proof state:
case h.e'_10.intro.h.H
𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
r : ENNReal
hpr : HasFPowerSeriesOnBall f p x r
n : ℕ
u : Fin n → 𝕜
h_fact_smul : ∀ (n : ℕ), ↑n.factorial * p.coeff n = (iteratedFDeriv 𝕜 n f x) fun x => 1
⊢ (FormalMultilinearSeries.ofScalars 𝕜 (fun n => iteratedDeriv n f x / ↑n.factorial) n) u = (p n) u

Tactic:
simp only [FormalMultilinearSeries.apply_eq_prod_smul_coeff,
  FormalMultilinearSeries.coeff_ofScalars, smul_eq_mul, mul_eq_mul_left_iff]

Result:
case h.e'_10.intro.h.H
𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
r : ENNReal
hpr : HasFPowerSeriesOnBall f p x r
n : ℕ
u : Fin n → 𝕜
h_fact_smul : ∀ (n : ℕ), ↑n.factorial * p.coeff n = (iteratedFDeriv 𝕜 n f x) fun x => 1
⊢ iteratedDeriv n f x / ↑n.factorial = p.coeff n ∨ ∏ i : Fin n, u i = 0

Proof state:
𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
h : AnalyticAt 𝕜 f x
⊢ HasFPowerSeriesAt f (FormalMultilinearSeries.ofScalars 𝕜 fun n => iteratedDeriv n f x / ↑n.factorial) x

Tactic:
obtain ⟨p, hp⟩ := h

Result:
case intro
𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
hp : HasFPowerSeriesAt f p x
⊢ HasFPowerSeriesAt f (FormalMultilinearSeries.ofScalars 𝕜 fun n => iteratedDeriv n f x / ↑n.factorial) x

Proof state:
case h.e'_10.intro.h.H
𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
r : ENNReal
hpr : HasFPowerSeriesOnBall f p x r
n : ℕ
u : Fin n → 𝕜
h_fact_smul : ∀ (n : ℕ), (n.factorial • (p n) fun x => 1) = (iteratedFDeriv 𝕜 n f x) fun x => 1
⊢ (FormalMultilinearSeries.ofScalars 𝕜 (fun n => iteratedDeriv n f x / ↑n.factorial) n) u = (p n) u

Tactic:
simp only [FormalMultilinearSeries.apply_eq_prod_smul_coeff, Finset.prod_const, Finset.card_univ,
  Fintype.card_fin, smul_eq_mul, nsmul_eq_mul, one_pow, one_mul] at h_fact_smul

Result:
case h.e'_10.intro.h.H
𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
r : ENNReal
hpr : HasFPowerSeriesOnBall f p x r
n : ℕ
u : Fin n → 𝕜
h_fact_smul : ∀ (n : ℕ), ↑n.factorial * p.coeff n = (iteratedFDeriv 𝕜 n f x) fun x => 1
⊢ (FormalMultilinearSeries.ofScalars 𝕜 (fun n => iteratedDeriv n f x / ↑n.factorial) n) u = (p n) u