-- Mathlib/Analysis/Analytic/IteratedFDeriv.lean
lemma FormalMultilinearSeries.iteratedFDerivSeries_eq_zero {k n : ℕ}
    (h : p (n + k) = 0) : p.iteratedFDerivSeries k n = 0

Proof state:
case zero.H.H
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
h : p (n + 0) = 0
x✝¹ : Fin n → E
x✝ : Fin 0 → E
⊢ ((p.iteratedFDerivSeries 0 n) x✝¹) x✝ = (0 x✝¹) x✝

Tactic:
have : p n = 0 := p.congr_zero rfl h

Result:
case zero.H.H
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
h : p (n + 0) = 0
x✝¹ : Fin n → E
x✝ : Fin 0 → E
this : p n = 0
⊢ ((p.iteratedFDerivSeries 0 n) x✝¹) x✝ = (0 x✝¹) x✝

Proof state:
case succ.H.H
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
k : ℕ
ih : ∀ {n : ℕ}, p (n + k) = 0 → p.iteratedFDerivSeries k n = 0
n : ℕ
h : p (n + (k + 1)) = 0
x✝¹ : Fin n → E
x✝ : Fin (k + 1) → E
⊢ ((p.iteratedFDerivSeries (k + 1) n) x✝¹) x✝ = (0 x✝¹) x✝

Tactic:
simp only [iteratedFDerivSeries, Nat.succ_eq_add_one,
  ContinuousLinearMap.compFormalMultilinearSeries_apply,
  ContinuousLinearMap.compContinuousMultilinearMap_coe, ContinuousLinearEquiv.coe_coe,
  LinearIsometryEquiv.coe_toContinuousLinearEquiv, Function.comp_apply,
  continuousMultilinearCurryLeftEquiv_symm_apply, ContinuousMultilinearMap.zero_apply,
  ContinuousLinearMap.zero_apply,
  derivSeries_eq_zero _ (ih (p.congr_zero (Nat.succ_add_eq_add_succ _ _).symm h))]

Result:
no goals

Proof state:
case zero
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
h : p (n + 0) = 0
⊢ p.iteratedFDerivSeries 0 n = 0

Tactic:
ext

Result:
case zero.H.H
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
h : p (n + 0) = 0
x✝¹ : Fin n → E
x✝ : Fin 0 → E
⊢ ((p.iteratedFDerivSeries 0 n) x✝¹) x✝ = (0 x✝¹) x✝

Proof state:
case zero.H.H
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
h : p (n + 0) = 0
x✝¹ : Fin n → E
x✝ : Fin 0 → E
this : p n = 0
⊢ ((p.iteratedFDerivSeries 0 n) x✝¹) x✝ = (0 x✝¹) x✝

Tactic:
simp [FormalMultilinearSeries.iteratedFDerivSeries, this]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
k n : ℕ
h : p (n + k) = 0
⊢ p.iteratedFDerivSeries k n = 0

Tactic:
induction k generalizing n with
| zero =>
  ext
  have : p n = 0 := p.congr_zero rfl h
  simp [FormalMultilinearSeries.iteratedFDerivSeries, this]
| succ k ih =>
  ext
  simp only [iteratedFDerivSeries, Nat.succ_eq_add_one,
    ContinuousLinearMap.compFormalMultilinearSeries_apply,
    ContinuousLinearMap.compContinuousMultilinearMap_coe, ContinuousLinearEquiv.coe_coe,
    LinearIsometryEquiv.coe_toContinuousLinearEquiv, Function.comp_apply,
    continuousMultilinearCurryLeftEquiv_symm_apply, ContinuousMultilinearMap.zero_apply,
    ContinuousLinearMap.zero_apply,
    derivSeries_eq_zero _ (ih (p.congr_zero (Nat.succ_add_eq_add_succ _ _).symm h))]

Result:
no goals

Proof state:
case succ
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
k : ℕ
ih : ∀ {n : ℕ}, p (n + k) = 0 → p.iteratedFDerivSeries k n = 0
n : ℕ
h : p (n + (k + 1)) = 0
⊢ p.iteratedFDerivSeries (k + 1) n = 0

Tactic:
ext

Result:
case succ.H.H
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
k : ℕ
ih : ∀ {n : ℕ}, p (n + k) = 0 → p.iteratedFDerivSeries k n = 0
n : ℕ
h : p (n + (k + 1)) = 0
x✝¹ : Fin n → E
x✝ : Fin (k + 1) → E
⊢ ((p.iteratedFDerivSeries (k + 1) n) x✝¹) x✝ = (0 x✝¹) x✝