case h
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1132100
G : Type ?u.1132103
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 𝕜 E
x : 𝕜
h : HasFPowerSeriesAt 0 p x
n : ℕ
⊢ p n = OfNat.ofNat 0 n
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1132100
G : Type ?u.1132103
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 𝕜 E
x : 𝕜
h : HasFPowerSeriesAt 0 p x
⊢ p = 0
funext n
case h.H
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1132100
G : Type ?u.1132103
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 𝕜 E
x✝ : 𝕜
h : HasFPowerSeriesAt 0 p x✝
n : ℕ
x : Fin n → 𝕜
⊢ ↑(p n) x = ↑(OfNat.ofNat 0 n) x
case h
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1132100
G : Type ?u.1132103
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 𝕜 E
x : 𝕜
h : HasFPowerSeriesAt 0 p x
n : ℕ
⊢ p n = OfNat.ofNat 0 n
ext x
case h.H
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1132100
G : Type ?u.1132103
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 𝕜 E
x✝ : 𝕜
h : HasFPowerSeriesAt 0 p x✝
n : ℕ
x : Fin n → 𝕜
⊢ ↑(ContinuousMultilinearMap.mkPiField 𝕜 (Fin n) (↑(p n) fun x => 1)) x = ↑(OfNat.ofNat 0 n) x
case h.H
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1132100
G : Type ?u.1132103
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 𝕜 E
x✝ : 𝕜
h : HasFPowerSeriesAt 0 p x✝
n : ℕ
x : Fin n → 𝕜
⊢ ↑(p n) x = ↑(OfNat.ofNat 0 n) x
rw [← mkPiField_apply_one_eq_self (p n)]
case h.H.refine_2
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1132100
G : Type ?u.1132103
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 𝕜 E
x✝ : 𝕜
h : HasFPowerSeriesAt 0 p x✝
n : ℕ
x : Fin n → 𝕜
this : ?h.H.refine_1 ∨ (↑(p n) fun x => 1) = 0
⊢ ↑(ContinuousMultilinearMap.mkPiField 𝕜 (Fin n) (↑(p n) fun x => 1)) x = ↑(OfNat.ofNat 0 n) x

case h.H.refine_1
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1132100
G : Type ?u.1132103
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 𝕜 E
x✝ : 𝕜
h : HasFPowerSeriesAt 0 p x✝
n : ℕ
x : Fin n → 𝕜
⊢ Prop
case h.H
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1132100
G : Type ?u.1132103
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 𝕜 E
x✝ : 𝕜
h : HasFPowerSeriesAt 0 p x✝
n : ℕ
x : Fin n → 𝕜
⊢ ↑(ContinuousMultilinearMap.mkPiField 𝕜 (Fin n) (↑(p n) fun x => 1)) x = ↑(OfNat.ofNat 0 n) x
have := Or.intro_right ?_ (h.apply_eq_zero n 1)
no goals
case h.H.refine_2
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1132100
G : Type ?u.1132103
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 𝕜 E
x✝ : 𝕜
h : HasFPowerSeriesAt 0 p x✝
n : ℕ
x : Fin n → 𝕜
this : ?h.H.refine_1 ∨ (↑(p n) fun x => 1) = 0
⊢ ↑(ContinuousMultilinearMap.mkPiField 𝕜 (Fin n) (↑(p n) fun x => 1)) x = ↑(OfNat.ofNat 0 n) x

case h.H.refine_1
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1132100
G : Type ?u.1132103
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 𝕜 E
x✝ : 𝕜
h : HasFPowerSeriesAt 0 p x✝
n : ℕ
x : Fin n → 𝕜
⊢ Prop
simpa using this