awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a : ℕ → E
h : a 0 = HPow.hPow (α := 𝕜) (β := ℕ) 0 0 • a 0
⊢ HasSum (fun (n : ℕ) ↦ HPow.hPow (α := 𝕜) 0 n • a n) (a 0)
have convert_2 : ∀ (b : ℕ) (h : b ≠ 0), HPow.hPow (α := 𝕜) 0 b • a b = 0
Tactic: convert! hasSum_single (α := E) 0 fun b h ↦ _
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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
⊢ ∃ (t : E), z ^ n • t = s ∧ HasSum (fun (m : ℕ) ↦ z ^ m • a (m + n)) t
have inl : ∀ (ha : ∀ k < 0, a k = 0), ∃ (t : E), HPow.hPow (β := ℕ) z 0 • t = s ∧ HasSum (fun (m : ℕ) ↦ z ^ m • a (m + 0)) t
Tactic: obtain rfl | hn := n.eq_zero_or_pos
Cleared hypotheses: n, ha
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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
⊢ ∃ (t : E), z ^ n • t = s ∧ HasSum (fun (m : ℕ) ↦ z ^ m • a (m + n)) t
have inr : ∀ (hn : n > 0), ∃ (t : E), z ^ n • t = s ∧ HasSum (fun (m : ℕ) ↦ z ^ m • a (m + n)) t
Tactic: obtain rfl | hn := n.eq_zero_or_pos
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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
⊢ ∃ (t : E), z ^ n • t = s ∧ HasSum (fun (m : ℕ) ↦ z ^ m • a (m + n)) t
have pos : ∀ (h : z = 0), ∃ (t : E), z ^ n • t = s ∧ HasSum (fun (m : ℕ) ↦ z ^ m • a (m + n)) t
Tactic: by_cases h : z = 0
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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
⊢ ∃ (t : E), z ^ n • t = s ∧ HasSum (fun (m : ℕ) ↦ z ^ m • a (m + n)) t
have neg : ∀ (h : ¬z = 0), ∃ (t : E), z ^ n • t = s ∧ HasSum (fun (m : ℕ) ↦ z ^ m • a (m + n)) t
Tactic: by_cases h : z = 0
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (hypothesis)
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
⊢ ∃ (t : E), z ^ n • t = s ∧ HasSum (fun (m : ℕ) ↦ z ^ m • a (m + n)) t
have this : s = 0
Tactic: have : s = 0 := hs.unique (by simpa [ha 0 hn, h] using hasSum_at_zero a)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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)⁻¹ • s = s
have match_scalars : z ^ n * ((z ^ n)⁻¹ * 1) = 1
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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
⊢ ∃ (t : E), z ^ n • t = s ∧ HasSum (fun (m : ℕ) ↦ z ^ m • a (m + n)) t
have neg : HasSum (fun (m : ℕ) ↦ z ^ m • a (m + n)) ((z ^ n)⁻¹ • s)
Tactic: refine ⟨(z ^ n)⁻¹ • s, by match_scalars; field, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (hypothesis)
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 (fun (m : ℕ) ↦ z ^ m • a (m + n)) ((z ^ n)⁻¹ • s)
have h1 : 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)]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (hypothesis)
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 • a (m + n)) ((z ^ n)⁻¹ • s)
have h2 : 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
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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 (m : ℕ) ↦ z ^ m • a (m + n)) ((z ^ n)⁻¹ • s)
have h₁ : ∀ (x : ℕ), z ^ x • a (x + n) = z⁻¹ ^ n • z ^ (x + n) • a (x + n)
Tactic: convert! h2.const_smul (z⁻¹ ^ n) using 2 with x
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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)
⊢ HasSum (fun (m : ℕ) ↦ z ^ m • a (m + n)) ((z ^ n)⁻¹ • s)
have h₂ : (z ^ n)⁻¹ = z⁻¹ ^ n
Tactic: convert! h2.const_smul (z⁻¹ ^ n) using 2 with x
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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 • a (x + n) = z⁻¹ ^ n • z ^ (x + n) • a (x + n)
have match_scalars : z ^ x * 1 = z⁻¹ ^ n * (z ^ (x + n) * 1)
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (hypothesis)
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₀
⊢ HasFPowerSeriesAt (dslope f z₀) p.fslope z₀
have hpd : deriv f z₀ = p.coeff 1
Tactic: have hpd : deriv f z₀ = p.coeff 1 := hp.deriv
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (hypothesis)
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
⊢ HasFPowerSeriesAt (dslope f z₀) p.fslope z₀
have hp0 : p.coeff 0 = f z₀
Tactic: have hp0 : p.coeff 0 = f z₀ := hp.coeff_zero 1
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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₀
⊢ HasFPowerSeriesAt (dslope f z₀) p.fslope z₀
have 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))
Tactic: simp only [hasFPowerSeriesAt_iff, coeff_fslope] at hp ⊢
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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))
have 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))
Tactic: refine hp.mono fun x hx => ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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))
⊢ HasSum (fun (n : ℕ) ↦ x ^ n • p.coeff (n + 1)) (dslope f z₀ (z₀ + x))
have pos : ∀ (h : x = 0), HasSum (fun (n : ℕ) ↦ x ^ n • p.coeff (n + 1)) (dslope f z₀ (z₀ + x))
Tactic: by_cases h : x = 0
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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))
⊢ HasSum (fun (n : ℕ) ↦ x ^ n • p.coeff (n + 1)) (dslope f z₀ (z₀ + x))
have neg : ∀ (h : ¬x = 0), HasSum (fun (n : ℕ) ↦ x ^ n • p.coeff (n + 1)) (dslope f z₀ (z₀ + x))
Tactic: by_cases h : x = 0
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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)) (dslope f z₀ (z₀ + x))
have h₁ : dslope f z₀ (z₀ + x) = HPow.hPow (β := ℕ) x 0 • p.coeff (HAdd.hAdd (α := ℕ) 0 1)
Tactic: convert! hasSum_single (α := E) 0 _
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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)
⊢ HasSum (fun (n : ℕ) ↦ x ^ n • p.coeff (n + 1)) (dslope f z₀ (z₀ + x))
have pos : ∀ (b' : ℕ), b' ≠ 0 → x ^ b' • p.coeff (b' + 1) = 0
Tactic: convert! hasSum_single (α := E) 0 _
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (hypothesis)
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)) (dslope f z₀ (z₀ + x))
have hxx : ∀ (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]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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 ^ n • p.coeff (n + 1)) (dslope f z₀ (z₀ + x))
have neg : HasSum (fun (n : ℕ) ↦ x⁻¹ • x ^ (n + 1) • p.coeff (n + 1)) (x⁻¹ • (f (z₀ + x) - f z₀))
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
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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₀
⊢ HasFPowerSeriesAt (𝕜 := 𝕜) ((swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope z₀)^[n] f) (fslope^[n] p) z₀
have 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₀
Tactic: induction n generalizing f p with
  | zero => exact hp
  | succ n ih => simpa using ih (has_fpower_series_dslope_fslope hp)
Cleared hypotheses: p, f, n, hp
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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₀
⊢ HasFPowerSeriesAt (𝕜 := 𝕜) ((swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope z₀)^[n] f) (fslope^[n] p) z₀
have 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₀
Tactic: induction n generalizing f p with
  | zero => exact hp
  | succ n ih => simpa using ih (has_fpower_series_dslope_fslope hp)
Cleared hypotheses: p, f, n, hp
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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
⊢ (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope z₀)^[p.order] f z₀ ≠ 0
have rw : Ne.{u_2 + 1} (α := E) ((fslope^[p.order] p 0 : (a : (i : Fin 0) → 𝕜) → E) 1 : E) (0 : E)
Tactic: rw [← coeff_zero (has_fpower_series_iterate_dslope_fslope p.order hp) 1]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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
have refine : ∀ (k : ℕ) (hk : k < p.order), (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope z₀)^[k] f z₀ = 0
Tactic: refine (pow_sub_smul_iterate_dslope_of_zero _ (fun k hk ↦ ?_) z).symm
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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 : 𝕜
k : ℕ
hk : k < p.order
⊢ (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope z₀)^[k] f z₀ = 0
have rw : Eq.{u_2 + 1} (α := E) ((fslope^[k] p 0 : (a : (i : Fin 0) → 𝕜) → E) 1 : E) (0 : E)
Tactic: rw [← (has_fpower_series_iterate_dslope_fslope k hp).coeff_zero 1, ← coeff, coeff_iterate_fslope,
    zero_add, coeff, p.apply_eq_zero_of_lt_order hk, ContinuousMultilinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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 : 𝕜
k : ℕ
hk : k < p.order
rw : Eq.{u_2 + 1} (α := E) ((fslope^[k] p 0 : (a : (i : Fin 0) → 𝕜) → E) 1 : E) (0 : E)
⊢ (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope z₀)^[k] f z₀ = 0
have rw₁ : (fslope^[k] p).coeff 0 = 0
Tactic: rw [← (has_fpower_series_iterate_dslope_fslope k hp).coeff_zero 1, ← coeff, coeff_iterate_fslope,
    zero_add, coeff, p.apply_eq_zero_of_lt_order hk, ContinuousMultilinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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 : 𝕜
k : ℕ
hk : k < p.order
rw : Eq.{u_2 + 1} (α := E) ((fslope^[k] p 0 : (a : (i : Fin 0) → 𝕜) → E) 1 : E) (0 : E)
rw₁ : (fslope^[k] p).coeff 0 = 0
⊢ (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope z₀)^[k] f z₀ = 0
have rw₂ : p.coeff (0 + k) = 0
Tactic: rw [← (has_fpower_series_iterate_dslope_fslope k hp).coeff_zero 1, ← coeff, coeff_iterate_fslope,
    zero_add, coeff, p.apply_eq_zero_of_lt_order hk, ContinuousMultilinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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 : 𝕜
k : ℕ
hk : k < p.order
rw : Eq.{u_2 + 1} (α := E) ((fslope^[k] p 0 : (a : (i : Fin 0) → 𝕜) → E) 1 : E) (0 : E)
rw₁ : (fslope^[k] p).coeff 0 = 0
rw₂ : p.coeff (0 + k) = 0
⊢ (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope z₀)^[k] f z₀ = 0
have rw₃ : p.coeff k = 0
Tactic: rw [← (has_fpower_series_iterate_dslope_fslope k hp).coeff_zero 1, ← coeff, coeff_iterate_fslope,
    zero_add, coeff, p.apply_eq_zero_of_lt_order hk, ContinuousMultilinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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 : 𝕜
k : ℕ
hk : k < p.order
rw : Eq.{u_2 + 1} (α := E) ((fslope^[k] p 0 : (a : (i : Fin 0) → 𝕜) → E) 1 : E) (0 : E)
rw₁ : (fslope^[k] p).coeff 0 = 0
rw₂ : p.coeff (0 + k) = 0
rw₃ : p.coeff k = 0
⊢ (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope z₀)^[k] f z₀ = 0
have rw₄ : Eq.{u_2 + 1} (α := E) ((p k : (a : (i : Fin k) → 𝕜) → E) 1 : E) (0 : E)
Tactic: rw [← (has_fpower_series_iterate_dslope_fslope k hp).coeff_zero 1, ← coeff, coeff_iterate_fslope,
    zero_add, coeff, p.apply_eq_zero_of_lt_order hk, ContinuousMultilinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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 : 𝕜
k : ℕ
hk : k < p.order
rw : Eq.{u_2 + 1} (α := E) ((fslope^[k] p 0 : (a : (i : Fin 0) → 𝕜) → E) 1 : E) (0 : E)
rw₁ : (fslope^[k] p).coeff 0 = 0
rw₂ : p.coeff (0 + k) = 0
rw₃ : p.coeff k = 0
rw₄ : Eq.{u_2 + 1} (α := E) ((p k : (a : (i : Fin k) → 𝕜) → E) 1 : E) (0 : E)
⊢ (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope z₀)^[k] f z₀ = 0
have rw₅ : Eq.{u_2 + 1} (α := E) ((0 : (a : (i : Fin k) → 𝕜) → E) 1 : E) (0 : E)
Tactic: rw [← (has_fpower_series_iterate_dslope_fslope k hp).coeff_zero 1, ← coeff, coeff_iterate_fslope,
    zero_add, coeff, p.apply_eq_zero_of_lt_order hk, ContinuousMultilinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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 : 𝕜
k : ℕ
hk : k < p.order
rw : Eq.{u_2 + 1} (α := E) ((fslope^[k] p 0 : (a : (i : Fin 0) → 𝕜) → E) 1 : E) (0 : E)
rw₁ : (fslope^[k] p).coeff 0 = 0
rw₂ : p.coeff (0 + k) = 0
rw₃ : p.coeff k = 0
rw₄ : Eq.{u_2 + 1} (α := E) ((p k : (a : (i : Fin k) → 𝕜) → E) 1 : E) (0 : E)
rw₅ : Eq.{u_2 + 1} (α := E) ((0 : (a : (i : Fin k) → 𝕜) → E) 1 : E) (0 : E)
⊢ (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope z₀)^[k] f z₀ = 0
have rw₆ : Eq.{u_2 + 1} (α := E) 0 0
Tactic: rw [← (has_fpower_series_iterate_dslope_fslope k hp).coeff_zero 1, ← coeff, coeff_iterate_fslope,
    zero_add, coeff, p.apply_eq_zero_of_lt_order hk, ContinuousMultilinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (goal)
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
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0
have rw : ∀ᶠ (x : 𝕜) in 𝓝 z₀, Membership.mem (γ := Set 𝕜) {z₀}ᶜ x → f x ≠ 0
Tactic: rw [eventually_nhdsWithin_iff]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (hypothesis)
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
⊢ ∀ᶠ (x : 𝕜) in 𝓝 z₀, Membership.mem (γ := Set 𝕜) {z₀}ᶜ x → f x ≠ 0
have h2 : ContinuousAt ((swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope z₀)^[p.order] f) z₀
Tactic: have h2 := (has_fpower_series_iterate_dslope_fslope p.order hp).continuousAt
-- Lean 4 proof step from Mathlib.Analysis.Analytic.IsolatedZeros (hypothesis)
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
h2 : ContinuousAt ((swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope z₀)^[p.order] f) z₀
⊢ ∀ᶠ (x : 𝕜) in 𝓝 z₀, Membership.mem (γ := Set 𝕜) {z₀}ᶜ x → f x ≠ 0
have h3 : ∀ᶠ (z : 𝕜) in 𝓝 z₀, (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope z₀)^[p.order] f z ≠ 0
Tactic: have h3 := h2.eventually_ne (iterate_dslope_fslope_ne_zero hp h)