awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun (m : ℕ) ↦ z ^ m • a m) s
ha : ∀ k < n, a k = 0
inl : ∀ (ha : ∀ k < 0, a k = 0), ∃ (t : E), HPow.hPow (β := ℕ) z 0 • t = s ∧ HasSum (fun (m : ℕ) ↦ z ^ m • a (m + 0)) t
inr : ∀ (hn : n > 0), ∃ (t : E), z ^ n • t = s ∧ HasSum (fun (m : ℕ) ↦ z ^ m • a (m + n)) t
⊢ ∃ (t : E), z ^ n • t = s ∧ HasSum (fun (m : ℕ) ↦ z ^ m • a (m + n)) t

Tactic:
obtain rfl | hn := n.eq_zero_or_pos

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : E
z : 𝕜
a : ℕ → E
hs : HasSum (fun (m : ℕ) ↦ z ^ m • a m) s
ha : ∀ k < 0, a k = 0
⊢ ∃ (t : E), HPow.hPow (β := ℕ) z 0 • t = s ∧ HasSum (fun (m : ℕ) ↦ z ^ m • a (m + 0)) t

Tactic:
simpa
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun (m : ℕ) ↦ z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
pos : ∀ (h : z = 0), ∃ (t : E), z ^ n • t = s ∧ HasSum (fun (m : ℕ) ↦ z ^ m • a (m + n)) t
neg : ∀ (h : ¬z = 0), ∃ (t : E), z ^ n • t = s ∧ HasSum (fun (m : ℕ) ↦ z ^ m • a (m + n)) t
⊢ ∃ (t : E), z ^ n • t = s ∧ HasSum (fun (m : ℕ) ↦ z ^ m • a (m + n)) t

Tactic:
by_cases h : z = 0
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun (m : ℕ) ↦ z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : z = 0
⊢ HasSum.{u_2, 0} (α := E) (fun (m : ℕ) ↦ z ^ m • a m) 0

Tactic:
simpa [ha 0 hn, h] using hasSum_at_zero a

Premises used: HasSum.hasSum_at_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun (m : ℕ) ↦ z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : z = 0
⊢ s = 0

Tactic:
have : s = 0 := hs.unique (by simpa [ha 0 hn, h] using hasSum_at_zero a)
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun (m : ℕ) ↦ z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : z = 0
this : s = 0
⊢ z ^ n • a n = s

Tactic:
simp [h, hn.ne', this]

Premises used: LT.lt.ne'
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun (m : ℕ) ↦ z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : z = 0
this : s = 0
⊢ HasSum (fun (m : ℕ) ↦ z ^ m • a (m + n)) (a n)

Tactic:
simpa [h] using hasSum_at_zero fun m => a (m + n)

Premises used: HasSum.hasSum_at_zero, HAdd.hAdd
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun (m : ℕ) ↦ z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : z = 0
this : s = 0
⊢ ∃ (t : E), z ^ n • t = s ∧ HasSum (fun (m : ℕ) ↦ z ^ m • a (m + n)) t

Tactic:
exact ⟨a n, by simp [h, hn.ne', this], by simpa [h] using hasSum_at_zero fun m => a (m + n)⟩
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun (m : ℕ) ↦ z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : ¬z = 0
match_scalars : z ^ n * ((z ^ n)⁻¹ * 1) = 1
⊢ z ^ n • (z ^ n)⁻¹ • s = s

Tactic:
match_scalars
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun (m : ℕ) ↦ z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : ¬z = 0
⊢ z ^ n * ((z ^ n)⁻¹ * 1) = 1

Tactic:
field
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun (m : ℕ) ↦ z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : ¬z = 0
neg : HasSum (fun (m : ℕ) ↦ z ^ m • a (m + n)) ((z ^ n)⁻¹ • s)
⊢ ∃ (t : E), z ^ n • t = s ∧ HasSum (fun (m : ℕ) ↦ z ^ m • a (m + n)) t

Tactic:
refine ⟨(z ^ n)⁻¹ • s, by match_scalars; field, ?_⟩
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun (m : ℕ) ↦ z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : ¬z = 0
k : ℕ
hk : k ∈ Finset.range n
⊢ z ^ k • a k = 0

Tactic:
simp [ha k (Finset.mem_range.mp hk)]

Premises used: Finset.mem_range, Iff.mp
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun (m : ℕ) ↦ z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : ¬z = 0
⊢ Eq.{u_2 + 1} (α := E) (∑ i ∈ Finset.range n, z ^ i • a i) 0

Tactic:
have h1 : ∑ i ∈ Finset.range n, z ^ i • a i = 0 :=
      Finset.sum_eq_zero fun k hk => by simp [ha k (Finset.mem_range.mp hk)]
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun (m : ℕ) ↦ z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : ¬z = 0
h1 : Eq.{u_2 + 1} (α := E) (∑ i ∈ Finset.range n, z ^ i • a i) 0
⊢ HasSum (fun (m : ℕ) ↦ z ^ (m + n) • a (m + n)) s

Tactic:
simpa [h1] using (hasSum_nat_add_iff' n).mpr hs

Premises used: Iff.mpr, hasSum_nat_add_iff'
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun (m : ℕ) ↦ z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : ¬z = 0
h1 : Eq.{u_2 + 1} (α := E) (∑ i ∈ Finset.range n, z ^ i • a i) 0
⊢ HasSum (fun (m : ℕ) ↦ z ^ (m + n) • a (m + n)) s

Tactic:
have h2 : HasSum (fun m => z ^ (m + n) • a (m + n)) s := by
      simpa [h1] using (hasSum_nat_add_iff' n).mpr hs
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun (m : ℕ) ↦ z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : ¬z = 0
h1 : Eq.{u_2 + 1} (α := E) (∑ i ∈ Finset.range n, z ^ i • a i) 0
h2 : HasSum (fun (m : ℕ) ↦ z ^ (m + n) • a (m + n)) s
⊢ HasSum (fun (i : ℕ) ↦ z⁻¹ ^ n • z ^ (i + n) • a (i + n)) (z⁻¹ ^ n • s)

Tactic:
h2.const_smul (z⁻¹ ^ n)

Premises used: Inv.inv, HPow.hPow, HasSum.const_smul
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun (m : ℕ) ↦ z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : ¬z = 0
h1 : Eq.{u_2 + 1} (α := E) (∑ i ∈ Finset.range n, z ^ i • a i) 0
h2 : HasSum (fun (m : ℕ) ↦ z ^ (m + n) • a (m + n)) s
h₁ : ∀ (x : ℕ), z ^ x • a (x + n) = z⁻¹ ^ n • z ^ (x + n) • a (x + n)
h₂ : (z ^ n)⁻¹ = z⁻¹ ^ n
⊢ HasSum (fun (m : ℕ) ↦ z ^ m • a (m + n)) ((z ^ n)⁻¹ • s)

Tactic:
convert! h2.const_smul (z⁻¹ ^ n) using 2 with x

Premises used: Inv.inv, HPow.hPow, HasSum.const_smul
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun (m : ℕ) ↦ z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : ¬z = 0
h1 : Eq.{u_2 + 1} (α := E) (∑ i ∈ Finset.range n, z ^ i • a i) 0
h2 : HasSum (fun (m : ℕ) ↦ z ^ (m + n) • a (m + n)) s
x : ℕ
match_scalars : z ^ x * 1 = z⁻¹ ^ n * (z ^ (x + n) * 1)
⊢ z ^ x • a (x + n) = z⁻¹ ^ n • z ^ (x + n) • a (x + n)

Tactic:
match_scalars
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun (m : ℕ) ↦ z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : ¬z = 0
h1 : Eq.{u_2 + 1} (α := E) (∑ i ∈ Finset.range n, z ^ i • a i) 0
h2 : HasSum (fun (m : ℕ) ↦ z ^ (m + n) • a (m + n)) s
x : ℕ
⊢ z ^ x * 1 = z⁻¹ ^ n * (z ^ (x + n) * 1)

Tactic:
simp [field, pow_add]

Premises used: pow_add
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun (m : ℕ) ↦ z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : ¬z = 0
h1 : Eq.{u_2 + 1} (α := E) (∑ i ∈ Finset.range n, z ^ i • a i) 0
h2 : HasSum (fun (m : ℕ) ↦ z ^ (m + n) • a (m + n)) s
⊢ (z ^ n)⁻¹ = z⁻¹ ^ n

Tactic:
simp only [inv_pow]

Premises used: inv_pow
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hp : HasFPowerSeriesAt (𝕜 := 𝕜) f p z₀
⊢ deriv f z₀ = p.coeff 1

Tactic:
have hpd : deriv f z₀ = p.coeff 1 := hp.deriv
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hp : HasFPowerSeriesAt (𝕜 := 𝕜) f p z₀
hpd : deriv f z₀ = p.coeff 1
⊢ p.coeff 0 = f z₀

Tactic:
have hp0 : p.coeff 0 = f z₀ := hp.coeff_zero 1
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hp : HasFPowerSeriesAt (𝕜 := 𝕜) f p z₀
hpd : deriv f z₀ = p.coeff 1
hp0 : p.coeff 0 = f z₀
simp :
  ∀ (hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun (n : ℕ) ↦ z ^ n • p.coeff n) (f (z₀ + z))),
    ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun (n : ℕ) ↦ z ^ n • p.coeff (n + 1)) (dslope f z₀ (z₀ + z))
⊢ HasFPowerSeriesAt (dslope f z₀) p.fslope z₀

Tactic:
simp only [hasFPowerSeriesAt_iff, coeff_fslope] at hp ⊢

Premises used: FormalMultilinearSeries.coeff_fslope, hasFPowerSeriesAt_iff
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hpd : deriv f z₀ = p.coeff 1
hp0 : p.coeff 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun (n : ℕ) ↦ z ^ n • p.coeff n) (f (z₀ + z))
⊢ ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun (n : ℕ) ↦ z ^ n • p.coeff (n + 1)) (dslope f z₀ (z₀ + z))

Tactic:
hp.mono fun x hx => ?_

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hpd : deriv f z₀ = p.coeff 1
hp0 : p.coeff 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun (n : ℕ) ↦ z ^ n • p.coeff n) (f (z₀ + z))
refine :
  ∀ (x : 𝕜) (hx : HasSum (fun (n : ℕ) ↦ x ^ n • p.coeff n) (f (z₀ + x))),
    HasSum (fun (n : ℕ) ↦ x ^ n • p.coeff (n + 1)) (dslope f z₀ (z₀ + x))
⊢ ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun (n : ℕ) ↦ z ^ n • p.coeff (n + 1)) (dslope f z₀ (z₀ + z))

Tactic:
refine hp.mono fun x hx => ?_

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hpd : deriv f z₀ = p.coeff 1
hp0 : p.coeff 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun (n : ℕ) ↦ z ^ n • p.coeff n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun (n : ℕ) ↦ x ^ n • p.coeff n) (f (z₀ + x))
pos : ∀ (h : x = 0), HasSum (fun (n : ℕ) ↦ x ^ n • p.coeff (n + 1)) (dslope f z₀ (z₀ + x))
neg : ∀ (h : ¬x = 0), HasSum (fun (n : ℕ) ↦ x ^ n • p.coeff (n + 1)) (dslope f z₀ (z₀ + x))
⊢ HasSum (fun (n : ℕ) ↦ x ^ n • p.coeff (n + 1)) (dslope f z₀ (z₀ + x))

Tactic:
by_cases h : x = 0
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hpd : deriv f z₀ = p.coeff 1
hp0 : p.coeff 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun (n : ℕ) ↦ z ^ n • p.coeff n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun (n : ℕ) ↦ x ^ n • p.coeff n) (f (z₀ + x))
h : x = 0
⊢ HasSum (fun (n : ℕ) ↦ x ^ n • p.coeff (n + 1)) (HPow.hPow (β := ℕ) x 0 • p.coeff (HAdd.hAdd (α := ℕ) 0 1))

Tactic:
hasSum_single (α := E) 0 _

Premises used: hasSum_single, OfNat.ofNat, SummationFilter.unconditional
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hpd : deriv f z₀ = p.coeff 1
hp0 : p.coeff 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun (n : ℕ) ↦ z ^ n • p.coeff n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun (n : ℕ) ↦ x ^ n • p.coeff n) (f (z₀ + x))
h : x = 0
h₁ : dslope f z₀ (z₀ + x) = HPow.hPow (β := ℕ) x 0 • p.coeff (HAdd.hAdd (α := ℕ) 0 1)
pos : ∀ (b' : ℕ), b' ≠ 0 → x ^ b' • p.coeff (b' + 1) = 0
⊢ HasSum (fun (n : ℕ) ↦ x ^ n • p.coeff (n + 1)) (dslope f z₀ (z₀ + x))

Tactic:
convert! hasSum_single (α := E) 0 _

Premises used: hasSum_single, OfNat.ofNat, SummationFilter.unconditional
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hpd : deriv f z₀ = p.coeff 1
hp0 : p.coeff 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun (n : ℕ) ↦ z ^ n • p.coeff n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun (n : ℕ) ↦ x ^ n • p.coeff n) (f (z₀ + x))
h : x = 0
⊢ dslope f z₀ (z₀ + x) = HPow.hPow (β := ℕ) x 0 • p.coeff (HAdd.hAdd (α := ℕ) 0 1)

Tactic:
simp [*]
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hpd : deriv f z₀ = p.coeff 1
hp0 : p.coeff 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun (n : ℕ) ↦ z ^ n • p.coeff n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun (n : ℕ) ↦ x ^ n • p.coeff n) (f (z₀ + x))
h : x = 0
b' : ℕ
h_1 : b' ≠ 0
⊢ x ^ b' • p.coeff (b' + 1) = 0

Tactic:
simp [*]
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hpd : deriv f z₀ = p.coeff 1
hp0 : p.coeff 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun (n : ℕ) ↦ z ^ n • p.coeff n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun (n : ℕ) ↦ x ^ n • p.coeff n) (f (z₀ + x))
h : ¬x = 0
n : ℕ
⊢ x⁻¹ * x ^ (n + 1) = x ^ n

Tactic:
simp [field, _root_.pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hpd : deriv f z₀ = p.coeff 1
hp0 : p.coeff 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun (n : ℕ) ↦ z ^ n • p.coeff n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun (n : ℕ) ↦ x ^ n • p.coeff n) (f (z₀ + x))
h : ¬x = 0
⊢ ∀ (n : ℕ), x⁻¹ * x ^ (n + 1) = x ^ n

Tactic:
have hxx : ∀ n : ℕ, x⁻¹ * x ^ (n + 1) = x ^ n := fun n => by simp [field, _root_.pow_succ]
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hpd : deriv f z₀ = p.coeff 1
hp0 : p.coeff 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun (n : ℕ) ↦ z ^ n • p.coeff n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun (n : ℕ) ↦ x ^ n • p.coeff n) (f (z₀ + x))
h : ¬x = 0
hxx : ∀ (n : ℕ), x⁻¹ * x ^ (n + 1) = x ^ n
this : HasSum (fun (n : ℕ) ↦ x⁻¹ • x ^ (n + 1) • p.coeff (n + 1)) (x⁻¹ • (f (z₀ + x) - f z₀))
⊢ HasSum (fun (n : ℕ) ↦ x ^ n • p.coeff (n + 1)) (dslope f z₀ (z₀ + x))

Tactic:
simpa [dslope, slope, h, smul_smul, hxx] using this

Premises used: smul_smul, slope, dslope
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hpd : deriv f z₀ = p.coeff 1
hp0 : p.coeff 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun (n : ℕ) ↦ z ^ n • p.coeff n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun (n : ℕ) ↦ x ^ n • p.coeff n) (f (z₀ + x))
h : ¬x = 0
hxx : ∀ (n : ℕ), x⁻¹ * x ^ (n + 1) = x ^ n
neg : HasSum (fun (n : ℕ) ↦ x⁻¹ • x ^ (n + 1) • p.coeff (n + 1)) (x⁻¹ • (f (z₀ + x) - f z₀))
⊢ HasSum (fun (n : ℕ) ↦ x ^ n • p.coeff (n + 1)) (dslope f z₀ (z₀ + x))

Tactic:
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
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hpd : deriv f z₀ = p.coeff 1
hp0 : p.coeff 0 = f z₀
hp : ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun (n : ℕ) ↦ z ^ n • p.coeff n) (f (z₀ + z))
x : 𝕜
hx : HasSum (fun (n : ℕ) ↦ x ^ n • p.coeff n) (f (z₀ + x))
h : ¬x = 0
hxx : ∀ (n : ℕ), x⁻¹ * x ^ (n + 1) = x ^ n
⊢ HasSum (fun (n : ℕ) ↦ x⁻¹ • x ^ (n + 1) • p.coeff (n + 1)) (x⁻¹ • (f (z₀ + x) - f z₀))

Tactic:
simpa [hp0] using ((hasSum_nat_add_iff' 1).mpr hx).const_smul x⁻¹

Premises used: Iff.mpr, hasSum_nat_add_iff', Inv.inv, OfNat.ofNat, HasSum.const_smul
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
z₀ : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
hp : HasFPowerSeriesAt (𝕜 := 𝕜) f p z₀
⊢ HasFPowerSeriesAt (𝕜 := 𝕜) ((swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope z₀)^[0] f) (fslope^[0] p) z₀

Tactic:
hp

Premises used: Nat.iterate
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
z₀ : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
hp : HasFPowerSeriesAt (𝕜 := 𝕜) f p z₀
⊢ HasFPowerSeriesAt (𝕜 := 𝕜) ((swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope z₀)^[0] f) (fslope^[0] p) z₀

Tactic:
exact hp
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
z₀ : 𝕜
n : ℕ
ih :
  ∀ {p : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜 → E} (hp : HasFPowerSeriesAt (𝕜 := 𝕜) f p z₀),
    HasFPowerSeriesAt (𝕜 := 𝕜) ((swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope z₀)^[n] f) (fslope^[n] p) z₀
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
hp : HasFPowerSeriesAt (𝕜 := 𝕜) f p z₀
⊢ HasFPowerSeriesAt (𝕜 := 𝕜) ((swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope z₀)^[n + 1] f) (fslope^[n + 1] p) z₀

Tactic:
simpa using ih (has_fpower_series_dslope_fslope hp)

Premises used: HasFPowerSeriesAt.has_fpower_series_dslope_fslope
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
n : ℕ
hp : HasFPowerSeriesAt (𝕜 := 𝕜) f p z₀
zero :
  ∀ {p : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜 → E} (hp : HasFPowerSeriesAt (𝕜 := 𝕜) f p z₀),
    HasFPowerSeriesAt (𝕜 := 𝕜) ((swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope z₀)^[0] f) (fslope^[0] p) z₀
succ :
  ∀ (n : ℕ)
    (ih :
      ∀ {p : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜 → E} (hp : HasFPowerSeriesAt (𝕜 := 𝕜) f p z₀),
        HasFPowerSeriesAt (𝕜 := 𝕜) ((swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope z₀)^[n] f) (fslope^[n] p) z₀)
    {p : FormalMultilinearSeries 𝕜 𝕜 E} {f : 𝕜 → E} (hp : HasFPowerSeriesAt (𝕜 := 𝕜) f p z₀),
    HasFPowerSeriesAt (𝕜 := 𝕜) ((swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope z₀)^[n + 1] f) (fslope^[n + 1] p) z₀
⊢ HasFPowerSeriesAt (𝕜 := 𝕜) ((swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope z₀)^[n] f) (fslope^[n] p) z₀

Tactic:
induction n generalizing f p with
  | zero => exact hp
  | succ n ih => simpa using ih (has_fpower_series_dslope_fslope hp)

Premises used: Nat.zero, Nat.succ
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hp : HasFPowerSeriesAt (𝕜 := 𝕜) f p z₀
h : p ≠ 0
rw : Ne.{u_2 + 1} (α := E) ((fslope^[p.order] p 0 : (a : (i : Fin 0) → 𝕜) → E) 1 : E) (0 : E)
⊢ (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope z₀)^[p.order] f z₀ ≠ 0

Tactic:
rw [← coeff_zero (has_fpower_series_iterate_dslope_fslope p.order hp) 1]

Premises used: FormalMultilinearSeries.order, HasFPowerSeriesAt.has_fpower_series_iterate_dslope_fslope, HasFPowerSeriesAt.coeff_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hp : HasFPowerSeriesAt (𝕜 := 𝕜) f p z₀
h : p ≠ 0
⊢ Ne.{u_2 + 1} (α := E) ((fslope^[p.order] p 0 : (a : (i : Fin 0) → 𝕜) → E) 1 : E) (0 : E)

Tactic:
simpa [coeff_eq_zero] using apply_order_ne_zero h

Premises used: FormalMultilinearSeries.coeff_eq_zero, FormalMultilinearSeries.apply_order_ne_zero
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hp : HasFPowerSeriesAt (𝕜 := 𝕜) f p z₀
z : 𝕜
⊢ f z = (z - z₀) ^ p.order • (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope z₀)^[p.order] f z

Tactic:
(pow_sub_smul_iterate_dslope_of_zero _ (fun k hk ↦ ?_) z).symm

Premises used: pow_sub_smul_iterate_dslope_of_zero, Eq.symm
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hp : HasFPowerSeriesAt (𝕜 := 𝕜) f p z₀
z : 𝕜
refine : ∀ (k : ℕ) (hk : k < p.order), (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope z₀)^[k] f z₀ = 0
⊢ f z = (z - z₀) ^ p.order • (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope z₀)^[p.order] f z

Tactic:
refine (pow_sub_smul_iterate_dslope_of_zero _ (fun k hk ↦ ?_) z).symm

Premises used: pow_sub_smul_iterate_dslope_of_zero, Eq.symm