-- Mathlib/Analysis/Analytic/Uniqueness.lean
theorem HasFPowerSeriesAt.apply_eq_zero {p : FormalMultilinearSeries 𝕜 E F} {x : E}
    (h : HasFPowerSeriesAt 0 p x) (n : ℕ) : ∀ y : E, (p n fun _ => y) = 0

Proof state:
case h.refine_1
𝕜 : 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
x : E
h : HasFPowerSeriesAt 0 p x
n k : ℕ
hk : ∀ m < k, ∀ (y : E), ((p m) fun x => y) = 0
z : E
b : ℕ
hb : b ∈ Finset.range (k + 1)
hnb : b ≠ k
this : b ≤ k
⊢ ((p b) fun x => z) = 0

Tactic:
simp only [hk b (this.lt_of_ne hnb), Pi.zero_apply]

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
x : E
n k : ℕ
hk : ∀ m < k, ∀ (y : E), ((p m) fun x => y) = 0
psum_eq : p.partialSum (k + 1) = fun y => (p k) fun x => y
h : (fun x => (p k) fun x_1 => x) =O[𝓝 0] fun y => ‖y‖ ^ k.succ
⊢ ∀ (y : E), ((p k) fun x => y) = 0

Tactic:
exact h.continuousMultilinearMap_apply_eq_zero

Result:
no goals

Proof state:
case h.refine_2
𝕜 : 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
x : E
h : HasFPowerSeriesAt 0 p x
n k : ℕ
hk : ∀ m < k, ∀ (y : E), ((p m) fun x => y) = 0
z : E
hn : k ∉ Finset.range (k + 1)
⊢ ((p k) fun x => z) = 0

Tactic:
exact False.elim (hn (Finset.mem_range.mpr (lt_add_one k)))

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
x : E
n k : ℕ
hk : ∀ m < k, ∀ (y : E), ((p m) fun x => y) = 0
psum_eq : p.partialSum (k + 1) = fun y => (p k) fun x => y
h : (fun y => 0 (x + y) - p.partialSum k.succ y) =O[𝓝 0] fun y => ‖y‖ ^ k.succ
⊢ ∀ (y : E), ((p k) fun x => y) = 0

Tactic:
simp only [psum_eq, zero_sub, Pi.zero_apply, Asymptotics.isBigO_neg_left] at h

Result:
𝕜 : 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
x : E
n k : ℕ
hk : ∀ m < k, ∀ (y : E), ((p m) fun x => y) = 0
psum_eq : p.partialSum (k + 1) = fun y => (p k) fun x => y
h : (fun x => (p k) fun x_1 => x) =O[𝓝 0] fun y => ‖y‖ ^ k.succ
⊢ ∀ (y : E), ((p k) fun x => y) = 0

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
x : E
h : HasFPowerSeriesAt 0 p x
n k : ℕ
hk : ∀ m < k, ∀ (y : E), ((p m) fun x => y) = 0
⊢ p.partialSum (k + 1) = fun y => (p k) fun x => y

Tactic:
funext z

Result:
case 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
x : E
h : HasFPowerSeriesAt 0 p x
n k : ℕ
hk : ∀ m < k, ∀ (y : E), ((p m) fun x => y) = 0
z : E
⊢ p.partialSum (k + 1) z = (p k) fun x => z

Proof state:
case 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
x : E
h : HasFPowerSeriesAt 0 p x
n k : ℕ
hk : ∀ m < k, ∀ (y : E), ((p m) fun x => y) = 0
z : E
⊢ p.partialSum (k + 1) z = (p k) fun x => z

Tactic:
refine Finset.sum_eq_single _ (fun b hb hnb => ?_) fun hn => ?_

Result:
case h.refine_1
𝕜 : 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
x : E
h : HasFPowerSeriesAt 0 p x
n k : ℕ
hk : ∀ m < k, ∀ (y : E), ((p m) fun x => y) = 0
z : E
b : ℕ
hb : b ∈ Finset.range (k + 1)
hnb : b ≠ k
⊢ ((p b) fun x => z) = 0

case h.refine_2
𝕜 : 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
x : E
h : HasFPowerSeriesAt 0 p x
n k : ℕ
hk : ∀ m < k, ∀ (y : E), ((p m) fun x => y) = 0
z : E
hn : k ∉ Finset.range (k + 1)
⊢ ((p k) fun x => z) = 0

Proof state:
case h.refine_1
𝕜 : 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
x : E
h : HasFPowerSeriesAt 0 p x
n k : ℕ
hk : ∀ m < k, ∀ (y : E), ((p m) fun x => y) = 0
z : E
b : ℕ
hb : b ∈ Finset.range (k + 1)
hnb : b ≠ k
⊢ ((p b) fun x => z) = 0

Tactic:
have := Finset.mem_range_succ_iff.mp hb

Result:
case h.refine_1
𝕜 : 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
x : E
h : HasFPowerSeriesAt 0 p x
n k : ℕ
hk : ∀ m < k, ∀ (y : E), ((p m) fun x => y) = 0
z : E
b : ℕ
hb : b ∈ Finset.range (k + 1)
hnb : b ≠ k
this : b ≤ k
⊢ ((p b) fun x => z) = 0

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
x : E
h : HasFPowerSeriesAt 0 p x
n : ℕ
⊢ ∀ (y : E), ((p n) fun x => y) = 0

Tactic:
refine Nat.strong_induction_on n fun k hk => ?_

Result:
𝕜 : 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
x : E
h : HasFPowerSeriesAt 0 p x
n k : ℕ
hk : ∀ m < k, ∀ (y : E), ((p m) fun x => y) = 0
⊢ ∀ (y : E), ((p k) fun x => y) = 0

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
x : E
h : HasFPowerSeriesAt 0 p x
n k : ℕ
hk : ∀ m < k, ∀ (y : E), ((p m) fun x => y) = 0
psum_eq : p.partialSum (k + 1) = fun y => (p k) fun x => y
⊢ ∀ (y : E), ((p k) fun x => y) = 0

Tactic:
replace h := h.isBigO_sub_partialSum_pow k.succ

Result:
𝕜 : 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
x : E
n k : ℕ
hk : ∀ m < k, ∀ (y : E), ((p m) fun x => y) = 0
psum_eq : p.partialSum (k + 1) = fun y => (p k) fun x => y
h : (fun y => 0 (x + y) - p.partialSum k.succ y) =O[𝓝 0] fun y => ‖y‖ ^ k.succ
⊢ ∀ (y : E), ((p k) fun x => y) = 0