[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a✝ a : ℕ → E
⊢ HasSum (fun n => 0 ^ n • a n) (a 0)
[PROOFSTEP]
convert hasSum_single (α := E) 0 fun b h => _
[GOAL]
case h.e'_6
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a✝ a : ℕ → E
⊢ a 0 = 0 ^ 0 • a 0
[PROOFSTEP]
first
| simp [Nat.pos_of_ne_zero h]
| simp
[GOAL]
case h.e'_6
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a✝ a : ℕ → E
⊢ a 0 = 0 ^ 0 • a 0
[PROOFSTEP]
simp [Nat.pos_of_ne_zero h]
[GOAL]
case h.e'_6
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a✝ a : ℕ → E
⊢ a 0 = 0 ^ 0 • a 0
[PROOFSTEP]
simp
[GOAL]
case convert_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a✝ a : ℕ → E
b : ℕ
h : b ≠ 0
⊢ 0 ^ b • a b = 0
[PROOFSTEP]
first
| simp [Nat.pos_of_ne_zero h]
| simp
[GOAL]
case convert_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a✝ a : ℕ → E
b : ℕ
h : b ≠ 0
⊢ 0 ^ b • a b = 0
[PROOFSTEP]
simp [Nat.pos_of_ne_zero h]
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ (k : ℕ), k < n → a k = 0
⊢ ∃ t, z ^ n • t = s ∧ HasSum (fun m => z ^ m • a (m + n)) t
[PROOFSTEP]
obtain rfl | hn := n.eq_zero_or_pos
[GOAL]
case inl
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
z z₀ : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ (k : ℕ), k < 0 → a k = 0
⊢ ∃ t, z ^ 0 • t = s ∧ HasSum (fun m => z ^ m • a (m + 0)) t
[PROOFSTEP]
simpa
[GOAL]
case inr
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ (k : ℕ), k < n → a k = 0
hn : n > 0
⊢ ∃ t, z ^ n • t = s ∧ HasSum (fun m => z ^ m • a (m + n)) t
[PROOFSTEP]
by_cases h : z = 0
[GOAL]
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ (k : ℕ), k < n → a k = 0
hn : n > 0
h : z = 0
⊢ ∃ t, z ^ n • t = s ∧ HasSum (fun m => z ^ m • a (m + n)) t
[PROOFSTEP]
have : s = 0 := hs.unique (by simpa [ha 0 hn, h] using hasSum_at_zero a)
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ (k : ℕ), k < n → a k = 0
hn : n > 0
h : z = 0
⊢ HasSum (fun m => z ^ m • a m) 0
[PROOFSTEP]
simpa [ha 0 hn, h] using hasSum_at_zero a
[GOAL]
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ (k : ℕ), k < n → a k = 0
hn : n > 0
h : z = 0
this : s = 0
⊢ ∃ t, z ^ n • t = s ∧ HasSum (fun m => z ^ m • a (m + n)) t
[PROOFSTEP]
exact ⟨a n, by simp [h, hn, this], by simpa [h] using hasSum_at_zero fun m => a (m + n)⟩
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ (k : ℕ), k < n → a k = 0
hn : n > 0
h : z = 0
this : s = 0
⊢ z ^ n • a n = s
[PROOFSTEP]
simp [h, hn, this]
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ (k : ℕ), k < n → a k = 0
hn : n > 0
h : z = 0
this : s = 0
⊢ HasSum (fun m => z ^ m • a (m + n)) (a n)
[PROOFSTEP]
simpa [h] using hasSum_at_zero fun m => a (m + n)
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ (k : ℕ), k < n → a k = 0
hn : n > 0
h : ¬z = 0
⊢ ∃ t, z ^ n • t = s ∧ HasSum (fun m => z ^ m • a (m + n)) t
[PROOFSTEP]
refine ⟨(z ^ n)⁻¹ • s, by field_simp [smul_smul], ?_⟩
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ (k : ℕ), k < n → a k = 0
hn : n > 0
h : ¬z = 0
⊢ z ^ n • (z ^ n)⁻¹ • s = s
[PROOFSTEP]
field_simp [smul_smul]
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ (k : ℕ), k < n → a k = 0
hn : n > 0
h : ¬z = 0
⊢ HasSum (fun m => z ^ m • a (m + n)) ((z ^ n)⁻¹ • s)
[PROOFSTEP]
have h1 : ∑ i in Finset.range n, z ^ i • a i = 0 :=
  Finset.sum_eq_zero fun k hk => by simp [ha k (Finset.mem_range.mp hk)]
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ (k : ℕ), k < n → a k = 0
hn : n > 0
h : ¬z = 0
k : ℕ
hk : k ∈ Finset.range n
⊢ z ^ k • a k = 0
[PROOFSTEP]
simp [ha k (Finset.mem_range.mp hk)]
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ (k : ℕ), k < n → a k = 0
hn : n > 0
h : ¬z = 0
h1 : ∑ i in Finset.range n, z ^ i • a i = 0
⊢ HasSum (fun m => z ^ m • a (m + n)) ((z ^ n)⁻¹ • s)
[PROOFSTEP]
have h2 : HasSum (fun m => z ^ (m + n) • a (m + n)) s := by simpa [h1] using (hasSum_nat_add_iff' n).mpr hs
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ (k : ℕ), k < n → a k = 0
hn : n > 0
h : ¬z = 0
h1 : ∑ i in Finset.range n, z ^ i • a i = 0
⊢ HasSum (fun m => z ^ (m + n) • a (m + n)) s
[PROOFSTEP]
simpa [h1] using (hasSum_nat_add_iff' n).mpr hs
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ (k : ℕ), k < n → a k = 0
hn : n > 0
h : ¬z = 0
h1 : ∑ i in Finset.range n, z ^ i • a i = 0
h2 : HasSum (fun m => z ^ (m + n) • a (m + n)) s
⊢ HasSum (fun m => z ^ m • a (m + n)) ((z ^ n)⁻¹ • s)
[PROOFSTEP]
convert h2.const_smul (z⁻¹ ^ n) using 1
[GOAL]
case h.e'_5
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ (k : ℕ), k < n → a k = 0
hn : n > 0
h : ¬z = 0
h1 : ∑ i in Finset.range n, z ^ i • a i = 0
h2 : HasSum (fun m => z ^ (m + n) • a (m + n)) s
⊢ (fun m => z ^ m • a (m + n)) = fun i => z⁻¹ ^ n • z ^ (i + n) • a (i + n)
[PROOFSTEP]
field_simp [pow_add, smul_smul]
[GOAL]
case h.e'_6
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
a : ℕ → E
hs : HasSum (fun m => z ^ m • a m) s
ha : ∀ (k : ℕ), k < n → a k = 0
hn : n > 0
h : ¬z = 0
h1 : ∑ i in Finset.range n, z ^ i • a i = 0
h2 : HasSum (fun m => z ^ (m + n) • a (m + n)) s
⊢ (z ^ n)⁻¹ • s = z⁻¹ ^ n • s
[PROOFSTEP]
simp only [inv_pow]
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
⊢ HasFPowerSeriesAt (dslope f z₀) (fslope p) z₀
[PROOFSTEP]
have hpd : deriv f z₀ = p.coeff 1 := hp.deriv
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
hpd : deriv f z₀ = coeff p 1
⊢ HasFPowerSeriesAt (dslope f z₀) (fslope p) z₀
[PROOFSTEP]
have hp0 : p.coeff 0 = f z₀ := hp.coeff_zero 1
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
hpd : deriv f z₀ = coeff p 1
hp0 : coeff p 0 = f z₀
⊢ HasFPowerSeriesAt (dslope f z₀) (fslope p) z₀
[PROOFSTEP]
simp only [hasFPowerSeriesAt_iff, apply_eq_pow_smul_coeff, coeff_fslope] at hp ⊢
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hpd : deriv f z₀ = coeff p 1
hp0 : coeff p 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • coeff p n) (f (z₀ + z))
⊢ ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • coeff p (n + 1)) (dslope f z₀ (z₀ + z))
[PROOFSTEP]
refine hp.mono fun x hx => ?_
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hpd : deriv f z₀ = coeff p 1
hp0 : coeff p 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • coeff p n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun n => x ^ n • coeff p n) (f (z₀ + x))
⊢ HasSum (fun n => x ^ n • coeff p (n + 1)) (dslope f z₀ (z₀ + x))
[PROOFSTEP]
by_cases h : x = 0
[GOAL]
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hpd : deriv f z₀ = coeff p 1
hp0 : coeff p 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • coeff p n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun n => x ^ n • coeff p n) (f (z₀ + x))
h : x = 0
⊢ HasSum (fun n => x ^ n • coeff p (n + 1)) (dslope f z₀ (z₀ + x))
[PROOFSTEP]
convert hasSum_single (α := E) 0 _
[GOAL]
case h.e'_6
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hpd : deriv f z₀ = coeff p 1
hp0 : coeff p 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • coeff p n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun n => x ^ n • coeff p n) (f (z₀ + x))
h : x = 0
⊢ dslope f z₀ (z₀ + x) = x ^ 0 • coeff p (0 + 1)
[PROOFSTEP]
intros
[GOAL]
case pos.convert_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hpd : deriv f z₀ = coeff p 1
hp0 : coeff p 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • coeff p n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun n => x ^ n • coeff p n) (f (z₀ + x))
h : x = 0
⊢ ∀ (b' : ℕ), b' ≠ 0 → x ^ b' • coeff p (b' + 1) = 0
[PROOFSTEP]
intros
[GOAL]
case h.e'_6
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hpd : deriv f z₀ = coeff p 1
hp0 : coeff p 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • coeff p n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun n => x ^ n • coeff p n) (f (z₀ + x))
h : x = 0
⊢ dslope f z₀ (z₀ + x) = x ^ 0 • coeff p (0 + 1)
[PROOFSTEP]
simp [*]
[GOAL]
case pos.convert_2
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hpd : deriv f z₀ = coeff p 1
hp0 : coeff p 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • coeff p n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun n => x ^ n • coeff p n) (f (z₀ + x))
h : x = 0
b'✝ : ℕ
x✝ : b'✝ ≠ 0
⊢ x ^ b'✝ • coeff p (b'✝ + 1) = 0
[PROOFSTEP]
simp [*]
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hpd : deriv f z₀ = coeff p 1
hp0 : coeff p 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • coeff p n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun n => x ^ n • coeff p n) (f (z₀ + x))
h : ¬x = 0
⊢ HasSum (fun n => x ^ n • coeff p (n + 1)) (dslope f z₀ (z₀ + x))
[PROOFSTEP]
have hxx : ∀ n : ℕ, x⁻¹ * x ^ (n + 1) = x ^ n := fun n => by field_simp [h, _root_.pow_succ']
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n✝ : ℕ
z z₀ : 𝕜
hpd : deriv f z₀ = coeff p 1
hp0 : coeff p 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • coeff p n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun n => x ^ n • coeff p n) (f (z₀ + x))
h : ¬x = 0
n : ℕ
⊢ x⁻¹ * x ^ (n + 1) = x ^ n
[PROOFSTEP]
field_simp [h, _root_.pow_succ']
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hpd : deriv f z₀ = coeff p 1
hp0 : coeff p 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • coeff p n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun n => x ^ n • coeff p n) (f (z₀ + x))
h : ¬x = 0
hxx : ∀ (n : ℕ), x⁻¹ * x ^ (n + 1) = x ^ n
⊢ HasSum (fun n => x ^ n • coeff p (n + 1)) (dslope f z₀ (z₀ + x))
[PROOFSTEP]
suffices HasSum (fun n => x⁻¹ • x ^ (n + 1) • p.coeff (n + 1)) (x⁻¹ • (f (z₀ + x) - f z₀)) by
  simpa [dslope, slope, h, smul_smul, hxx] using this
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hpd : deriv f z₀ = coeff p 1
hp0 : coeff p 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • coeff p n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun n => x ^ n • coeff p n) (f (z₀ + x))
h : ¬x = 0
hxx : ∀ (n : ℕ), x⁻¹ * x ^ (n + 1) = x ^ n
this : HasSum (fun n => x⁻¹ • x ^ (n + 1) • coeff p (n + 1)) (x⁻¹ • (f (z₀ + x) - f z₀))
⊢ HasSum (fun n => x ^ n • coeff p (n + 1)) (dslope f z₀ (z₀ + x))
[PROOFSTEP]
simpa [dslope, slope, h, smul_smul, hxx] using this
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hpd : deriv f z₀ = coeff p 1
hp0 : coeff p 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • coeff p n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun n => x ^ n • coeff p n) (f (z₀ + x))
h : ¬x = 0
hxx : ∀ (n : ℕ), x⁻¹ * x ^ (n + 1) = x ^ n
⊢ HasSum (fun n => x⁻¹ • x ^ (n + 1) • coeff p (n + 1)) (x⁻¹ • (f (z₀ + x) - f z₀))
[PROOFSTEP]
simpa [hp0] using ((hasSum_nat_add_iff' 1).mpr hx).const_smul x⁻¹
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n✝ : ℕ
z z₀ : 𝕜
n : ℕ
hp : HasFPowerSeriesAt f p z₀
⊢ HasFPowerSeriesAt ((swap dslope z₀)^[n] f) (fslope^[n] p) z₀
[PROOFSTEP]
induction' n with n ih generalizing f p
[GOAL]
case zero
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p✝ q : FormalMultilinearSeries 𝕜 𝕜 E
f✝ g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hp✝ : HasFPowerSeriesAt f✝ p✝ z₀
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
hp : HasFPowerSeriesAt f p z₀
⊢ HasFPowerSeriesAt ((swap dslope z₀)^[zero] f) (fslope^[zero] p) z₀
[PROOFSTEP]
exact hp
[GOAL]
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p✝ q : FormalMultilinearSeries 𝕜 𝕜 E
f✝ g : 𝕜 → E
n✝ : ℕ
z z₀ : 𝕜
hp✝ : HasFPowerSeriesAt f✝ p✝ z₀
n : ℕ
ih :
  ∀ {p : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜 → E},
    HasFPowerSeriesAt f p z₀ → HasFPowerSeriesAt ((swap dslope z₀)^[n] f) (fslope^[n] p) z₀
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
hp : HasFPowerSeriesAt f p z₀
⊢ HasFPowerSeriesAt ((swap dslope z₀)^[succ n] f) (fslope^[succ n] p) z₀
[PROOFSTEP]
simpa using ih (has_fpower_series_dslope_fslope hp)
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
⊢ (swap dslope z₀)^[order p] f z₀ ≠ 0
[PROOFSTEP]
rw [← coeff_zero (has_fpower_series_iterate_dslope_fslope p.order hp) 1]
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
⊢ ↑(fslope^[order p] p 0) 1 ≠ 0
[PROOFSTEP]
simpa [coeff_eq_zero] using apply_order_ne_zero h
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ order p • (swap dslope z₀)^[order p] f z
[PROOFSTEP]
have hq := hasFPowerSeriesAt_iff'.mp (has_fpower_series_iterate_dslope_fslope p.order hp)
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
hq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, HasSum (fun n => (z - z₀) ^ n • coeff (fslope^[order p] p) n) ((swap dslope z₀)^[order p] f z)
⊢ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ order p • (swap dslope z₀)^[order p] f z
[PROOFSTEP]
filter_upwards [hq, hasFPowerSeriesAt_iff'.mp hp] with x hx1 hx2
[GOAL]
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
hq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, HasSum (fun n => (z - z₀) ^ n • coeff (fslope^[order p] p) n) ((swap dslope z₀)^[order p] f z)
x : 𝕜
hx1 : HasSum (fun n => (x - z₀) ^ n • coeff (fslope^[order p] p) n) ((swap dslope z₀)^[order p] f x)
hx2 : HasSum (fun n => (x - z₀) ^ n • coeff p n) (f x)
⊢ f x = (x - z₀) ^ order p • (swap dslope z₀)^[order p] f x
[PROOFSTEP]
have : ∀ k < p.order, p.coeff k = 0 := fun k hk => by simpa [coeff_eq_zero] using apply_eq_zero_of_lt_order hk
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
hq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, HasSum (fun n => (z - z₀) ^ n • coeff (fslope^[order p] p) n) ((swap dslope z₀)^[order p] f z)
x : 𝕜
hx1 : HasSum (fun n => (x - z₀) ^ n • coeff (fslope^[order p] p) n) ((swap dslope z₀)^[order p] f x)
hx2 : HasSum (fun n => (x - z₀) ^ n • coeff p n) (f x)
k : ℕ
hk : k < order p
⊢ coeff p k = 0
[PROOFSTEP]
simpa [coeff_eq_zero] using apply_eq_zero_of_lt_order hk
[GOAL]
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
hq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, HasSum (fun n => (z - z₀) ^ n • coeff (fslope^[order p] p) n) ((swap dslope z₀)^[order p] f z)
x : 𝕜
hx1 : HasSum (fun n => (x - z₀) ^ n • coeff (fslope^[order p] p) n) ((swap dslope z₀)^[order p] f x)
hx2 : HasSum (fun n => (x - z₀) ^ n • coeff p n) (f x)
this : ∀ (k : ℕ), k < order p → coeff p k = 0
⊢ f x = (x - z₀) ^ order p • (swap dslope z₀)^[order p] f x
[PROOFSTEP]
obtain ⟨s, hs1, hs2⟩ := HasSum.exists_hasSum_smul_of_apply_eq_zero hx2 this
[GOAL]
case h.intro.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
hq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, HasSum (fun n => (z - z₀) ^ n • coeff (fslope^[order p] p) n) ((swap dslope z₀)^[order p] f z)
x : 𝕜
hx1 : HasSum (fun n => (x - z₀) ^ n • coeff (fslope^[order p] p) n) ((swap dslope z₀)^[order p] f x)
hx2 : HasSum (fun n => (x - z₀) ^ n • coeff p n) (f x)
this : ∀ (k : ℕ), k < order p → coeff p k = 0
s : E
hs1 : (x - z₀) ^ order p • s = f x
hs2 : HasSum (fun m => (x - z₀) ^ m • coeff p (m + order p)) s
⊢ f x = (x - z₀) ^ order p • (swap dslope z₀)^[order p] f x
[PROOFSTEP]
convert hs1.symm
[GOAL]
case h.e'_3.h.e'_6
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
hq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, HasSum (fun n => (z - z₀) ^ n • coeff (fslope^[order p] p) n) ((swap dslope z₀)^[order p] f z)
x : 𝕜
hx1 : HasSum (fun n => (x - z₀) ^ n • coeff (fslope^[order p] p) n) ((swap dslope z₀)^[order p] f x)
hx2 : HasSum (fun n => (x - z₀) ^ n • coeff p n) (f x)
this : ∀ (k : ℕ), k < order p → coeff p k = 0
s : E
hs1 : (x - z₀) ^ order p • s = f x
hs2 : HasSum (fun m => (x - z₀) ^ m • coeff p (m + order p)) s
⊢ (swap dslope z₀)^[order p] f x = s
[PROOFSTEP]
simp only [coeff_iterate_fslope] at hx1 
[GOAL]
case h.e'_3.h.e'_6
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s✝ : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
hq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, HasSum (fun n => (z - z₀) ^ n • coeff (fslope^[order p] p) n) ((swap dslope z₀)^[order p] f z)
x : 𝕜
hx2 : HasSum (fun n => (x - z₀) ^ n • coeff p n) (f x)
this : ∀ (k : ℕ), k < order p → coeff p k = 0
s : E
hs1 : (x - z₀) ^ order p • s = f x
hs2 : HasSum (fun m => (x - z₀) ^ m • coeff p (m + order p)) s
hx1 : HasSum (fun n => (x - z₀) ^ n • coeff p (n + order p)) ((swap dslope z₀)^[order p] f x)
⊢ (swap dslope z₀)^[order p] f x = s
[PROOFSTEP]
exact hx1.unique hs2
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[{z₀}ᶜ] z₀, f z ≠ 0
[PROOFSTEP]
rw [eventually_nhdsWithin_iff]
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
⊢ ∀ᶠ (x : 𝕜) in 𝓝 z₀, x ∈ {z₀}ᶜ → f x ≠ 0
[PROOFSTEP]
have h2 := (has_fpower_series_iterate_dslope_fslope p.order hp).continuousAt
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
h2 : ContinuousAt ((swap dslope z₀)^[order p] f) z₀
⊢ ∀ᶠ (x : 𝕜) in 𝓝 z₀, x ∈ {z₀}ᶜ → f x ≠ 0
[PROOFSTEP]
have h3 := h2.eventually_ne (iterate_dslope_fslope_ne_zero hp h)
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
h2 : ContinuousAt ((swap dslope z₀)^[order p] f) z₀
h3 : ∀ᶠ (z : 𝕜) in 𝓝 z₀, (swap dslope z₀)^[order p] f z ≠ 0
⊢ ∀ᶠ (x : 𝕜) in 𝓝 z₀, x ∈ {z₀}ᶜ → f x ≠ 0
[PROOFSTEP]
filter_upwards [eq_pow_order_mul_iterate_dslope hp, h3] with z e1 e2 e3
[GOAL]
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z✝ z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
h2 : ContinuousAt ((swap dslope z₀)^[order p] f) z₀
h3 : ∀ᶠ (z : 𝕜) in 𝓝 z₀, (swap dslope z₀)^[order p] f z ≠ 0
z : 𝕜
e1 : f z = (z - z₀) ^ order p • (swap dslope z₀)^[order p] f z
e2 : (swap dslope z₀)^[order p] f z ≠ 0
e3 : z ∈ {z₀}ᶜ
⊢ f z ≠ 0
[PROOFSTEP]
simpa [e1, e2, e3] using pow_ne_zero p.order (sub_ne_zero.mpr e3)
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
h : p = 0
⊢ HasFPowerSeriesAt (fun z => f z) 0 z₀
[PROOFSTEP]
rwa [h] at hp 
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
⊢ (∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[{z₀}ᶜ] z₀, f z ≠ 0
[PROOFSTEP]
rcases hf with ⟨p, hp⟩
[GOAL]
case intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p✝ q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
hp : HasFPowerSeriesAt f p z₀
⊢ (∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[{z₀}ᶜ] z₀, f z ≠ 0
[PROOFSTEP]
by_cases h : p = 0
[GOAL]
case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p✝ q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
hp : HasFPowerSeriesAt f p z₀
h : p = 0
⊢ (∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[{z₀}ᶜ] z₀, f z ≠ 0
[PROOFSTEP]
exact Or.inl (HasFPowerSeriesAt.eventually_eq_zero (by rwa [h] at hp ))
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p✝ q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
hp : HasFPowerSeriesAt f p z₀
h : p = 0
⊢ HasFPowerSeriesAt (fun z => f z) 0 z₀
[PROOFSTEP]
rwa [h] at hp 
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p✝ q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
hp : HasFPowerSeriesAt f p z₀
h : ¬p = 0
⊢ (∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[{z₀}ᶜ] z₀, f z ≠ 0
[PROOFSTEP]
exact Or.inr (hp.locally_ne_zero h)
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
⊢ (∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = g z) ∨ ∀ᶠ (z : 𝕜) in 𝓝[{z₀}ᶜ] z₀, f z ≠ g z
[PROOFSTEP]
simpa [sub_eq_zero] using (hf.sub hg).eventually_eq_zero_or_eventually_ne_zero
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
⊢ (∃ᶠ (z : 𝕜) in 𝓝[{z₀}ᶜ] z₀, f z = g z) ↔ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = g z
[PROOFSTEP]
simpa [sub_eq_zero] using frequently_zero_iff_eventually_zero (hf.sub hg)
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
U : Set 𝕜
hf : AnalyticOn 𝕜 f U
hg : AnalyticOn 𝕜 g U
hU : IsPreconnected U
h₀ : z₀ ∈ U
hfg : ∃ᶠ (z : 𝕜) in 𝓝[{z₀}ᶜ] z₀, f z = g z
⊢ EqOn f g U
[PROOFSTEP]
have hfg' : ∃ᶠ z in 𝓝[≠] z₀, (f - g) z = 0 := hfg.mono fun z h => by rw [Pi.sub_apply, h, sub_self]
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z✝ z₀ : 𝕜
U : Set 𝕜
hf : AnalyticOn 𝕜 f U
hg : AnalyticOn 𝕜 g U
hU : IsPreconnected U
h₀ : z₀ ∈ U
hfg : ∃ᶠ (z : 𝕜) in 𝓝[{z₀}ᶜ] z₀, f z = g z
z : 𝕜
h : f z = g z
⊢ (f - g) z = 0
[PROOFSTEP]
rw [Pi.sub_apply, h, sub_self]
[GOAL]
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
p q : FormalMultilinearSeries 𝕜 𝕜 E
f g : 𝕜 → E
n : ℕ
z z₀ : 𝕜
U : Set 𝕜
hf : AnalyticOn 𝕜 f U
hg : AnalyticOn 𝕜 g U
hU : IsPreconnected U
h₀ : z₀ ∈ U
hfg : ∃ᶠ (z : 𝕜) in 𝓝[{z₀}ᶜ] z₀, f z = g z
hfg' : ∃ᶠ (z : 𝕜) in 𝓝[{z₀}ᶜ] z₀, (f - g) z = 0
⊢ EqOn f g U
[PROOFSTEP]
simpa [sub_eq_zero] using fun z hz => (hf.sub hg).eqOn_zero_of_preconnected_of_frequently_eq_zero hU h₀ hfg' hz
