-- Mathlib/Analysis/Analytic/ChangeOrigin.lean
theorem derivSeries_eq_zero {n : ℕ} (hp : p (n + 1) = 0) : p.derivSeries n = 0

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

Tactic:
apply Finset.sum_eq_zero (fun s hs ↦ ?_)

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hp : p (n + 1) = 0
s : { s // s.card = n }
hs : s ∈ Finset.univ
⊢ p.changeOriginSeriesTerm 1 n ↑s ⋯ = 0

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

Tactic:
simp [derivSeries, this]

Result:
no goals

Proof state:
case H.H
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hp : p (n + 1) = 0
s : { s // s.card = n }
hs : s ∈ Finset.univ
v : Fin n → E
x✝ : Fin 1 → E
this : p (1 + n) = 0
⊢ ((p.changeOriginSeriesTerm 1 n ↑s ⋯) v) x✝ = (0 v) x✝

Tactic:
simp [changeOriginSeriesTerm, ContinuousMultilinearMap.curryFinFinset_apply,
  ContinuousMultilinearMap.zero_apply, this]

Result:
no goals

Proof state:
case H.H
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hp : p (n + 1) = 0
s : { s // s.card = n }
hs : s ∈ Finset.univ
v : Fin n → E
x✝ : Fin 1 → E
⊢ ((p.changeOriginSeriesTerm 1 n ↑s ⋯) v) x✝ = (0 v) x✝

Tactic:
have : p (1 + n) = 0 := p.congr_zero (by abel) hp

Result:
case H.H
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hp : p (n + 1) = 0
s : { s // s.card = n }
hs : s ∈ Finset.univ
v : Fin n → E
x✝ : Fin 1 → E
this : p (1 + n) = 0
⊢ ((p.changeOriginSeriesTerm 1 n ↑s ⋯) v) x✝ = (0 v) x✝

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

Tactic:
suffices p.changeOriginSeries 1 n = 0 by ext v; simp [derivSeries, this]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hp : p (n + 1) = 0
⊢ p.changeOriginSeries 1 n = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hp : p (n + 1) = 0
s : { s // s.card = n }
hs : s ∈ Finset.univ
v : Fin n → E
x✝ : Fin 1 → E
⊢ n + 1 = 1 + n

Tactic:
abel

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hp : p (n + 1) = 0
s : { s // s.card = n }
hs : s ∈ Finset.univ
⊢ p.changeOriginSeriesTerm 1 n ↑s ⋯ = 0

Tactic:
ext v

Result:
case H.H
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hp : p (n + 1) = 0
s : { s // s.card = n }
hs : s ∈ Finset.univ
v : Fin n → E
x✝ : Fin 1 → E
⊢ ((p.changeOriginSeriesTerm 1 n ↑s ⋯) v) x✝ = (0 v) x✝

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hp : p (n + 1) = 0
this : p.changeOriginSeries 1 n = 0
⊢ p.derivSeries n = 0

Tactic:
ext v

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