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
f : 𝕜 → E
z₀ : 𝕜
m n : ℤ
hm : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z
hn : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • g z
h_le : n ≤ m
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
left : g z₀ ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z
j : 𝕜 → E
hj_an : AnalyticAt 𝕜 j z₀
hj_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • j z
hj_ne : m ≠ n
this : ∀ᶠ (z : 𝕜) in 𝓝 z₀, j z = (z - z₀) ^ (m - n) • g z
rw : (z₀ - z₀) ^ (m - n) • g z₀ = 0
rw₁ : HPow.hPow (α := 𝕜) 0 (m - n) • g z₀ = 0
rw₂ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 (g z₀) = 0
rw₃ rw₄ : Eq.{u_2 + 1} (α := E) 0 0
⊢ j z₀ = 0

Tactic:
rw [EventuallyEq.eq_of_nhds this, sub_self, zero_zpow _ (sub_ne_zero.mpr hj_ne), zero_smul]

Premises used: Iff.mpr, zero_zpow, sub_self, Filter.EventuallyEq.eq_of_nhds, sub_ne_zero, zero_smul
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
m n : ℤ
hm : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z
hn : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • g z
h_le : n ≤ m
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
left : g z₀ ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z
j : 𝕜 → E
hj_an : AnalyticAt 𝕜 j z₀
hj_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • j z
hj_ne : m ≠ n
this : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, j z = (z - z₀) ^ (m - n) • g z
h : ∀ (z : 𝕜), (z - z₀) ^ (m - n)
| AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - z₀) ^ (m - n) • g z) z₀

Tactic:
enter [2, z, 1]
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
m n : ℤ
hm : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z
hn : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • g z
h_le : n ≤ m
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
left : g z₀ ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z
j : 𝕜 → E
hj_an : AnalyticAt 𝕜 j z₀
hj_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • j z
hj_ne : m ≠ n
this : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, j z = (z - z₀) ^ (m - n) • g z
z : 𝕜
h : (z - z₀) ^ (m - n).toNat
| (z - z₀) ^ (m - n)

Tactic:
rw [← Int.toNat_sub_of_le h_le, zpow_natCast]

Premises used: zpow_natCast, Int.toNat_sub_of_le
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
m n : ℤ
hm : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z
hn : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • g z
h_le : n ≤ m
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
left : g z₀ ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z
j : 𝕜 → E
hj_an : AnalyticAt 𝕜 j z₀
hj_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • j z
hj_ne : m ≠ n
this : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, j z = (z - z₀) ^ (m - n) • g z
h : ∀ (z : 𝕜), (z - z₀) ^ (m - n).toNat
| AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - z₀) ^ (m - n) • g z) z₀

Tactic:
enter [2, z, 1]; rw [← Int.toNat_sub_of_le h_le, zpow_natCast]

Premises used: zpow_natCast, Int.toNat_sub_of_le
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
m n : ℤ
hm : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z
hn : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • g z
h_le : n ≤ m
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
left : g z₀ ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z
j : 𝕜 → E
hj_an : AnalyticAt 𝕜 j z₀
hj_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • j z
hj_ne : m ≠ n
this : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, j z = (z - z₀) ^ (m - n) • g z
conv : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - z₀) ^ (m - n).toNat • g z) z₀
⊢ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - z₀) ^ (m - n) • g z) z₀

Tactic:
conv => enter [2, z, 1]; rw [← Int.toNat_sub_of_le h_le, zpow_natCast]

Premises used: zpow_natCast, Int.toNat_sub_of_le
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
m n : ℤ
hm : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z
hn : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • g z
h_le : n ≤ m
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
left : g z₀ ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z
j : 𝕜 → E
hj_an : AnalyticAt 𝕜 j z₀
hj_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • j z
hj_ne : m ≠ n
this : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, j z = (z - z₀) ^ (m - n) • g z
⊢ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - z₀) ^ (m - n).toNat • g z) z₀

Tactic:
((analyticAt_id.sub analyticAt_const).pow _).smul hg_an

Premises used: AnalyticAt.smul, analyticAt_const, AnalyticAt.sub, analyticAt_id, AnalyticAt.pow
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
m n : ℤ
hm : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z
hn : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • g z
h_le : n ≤ m
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
left : g z₀ ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z
j : 𝕜 → E
hj_an : AnalyticAt 𝕜 j z₀
hj_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • j z
hj_ne : m ≠ n
this : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, j z = (z - z₀) ^ (m - n) • g z
⊢ AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - z₀) ^ (m - n).toNat • g z) z₀

Tactic:
exact ((analyticAt_id.sub analyticAt_const).pow _).smul hg_an

Premises used: AnalyticAt.smul, analyticAt_const, AnalyticAt.sub, analyticAt_id, AnalyticAt.pow
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
m n : ℕ
hm : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ m • g z
hn : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
⊢ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = HPow.hPow (β := ℤ) (z - z₀) (↑m : ℤ) • g z

Tactic:
simp_rw [← zpow_natCast] at hm hn

Premises used: zpow_natCast
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
m n : ℕ
hm : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ m • g z
hn : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
hm₁ : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = HPow.hPow (β := ℤ) (z - z₀) (↑m : ℤ) • g z
⊢ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = HPow.hPow (β := ℤ) (z - z₀) (↑n : ℤ) • g z

Tactic:
simp_rw [← zpow_natCast] at hm hn

Premises used: zpow_natCast
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
m n : ℕ
hm : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = HPow.hPow (β := ℤ) (z - z₀) (↑m : ℤ) • g z
hn : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = HPow.hPow (β := ℤ) (z - z₀) (↑n : ℤ) • g z
⊢ m = n

Tactic:
Int.ofNat_inj.mp <| unique_eventuallyEq_zpow_smul_nonzero
    (let ⟨g, h₁, h₂, h₃⟩ := hm; ⟨g, h₁, h₂, h₃.filter_mono nhdsWithin_le_nhds⟩)
    (let ⟨g, h₁, h₂, h₃⟩ := hn; ⟨g, h₁, h₂, h₃.filter_mono nhdsWithin_le_nhds⟩)

Premises used: Filter.Eventually.filter_mono, Compl.compl, nhdsWithin, Filter.Eventually, HSub.hSub, Exists, Int.ofNat_inj, _private.0.AnalyticAt.unique_eventuallyEq_pow_smul_nonzero.match_1, Ne, Nat.cast, And, nhdsWithin_le_nhds, HPow.hPow, AnalyticAt, And.intro, Exists.intro, Iff.mp, HSMul.hSMul, AnalyticAt.unique_eventuallyEq_zpow_smul_nonzero, Singleton.singleton, OfNat.ofNat, Eq
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
m n : ℕ
hm : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = HPow.hPow (β := ℤ) (z - z₀) (↑m : ℤ) • g z
hn : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = HPow.hPow (β := ℤ) (z - z₀) (↑n : ℤ) • g z
⊢ m = n

Tactic:
exact Int.ofNat_inj.mp <| unique_eventuallyEq_zpow_smul_nonzero
    (let ⟨g, h₁, h₂, h₃⟩ := hm; ⟨g, h₁, h₂, h₃.filter_mono nhdsWithin_le_nhds⟩)
    (let ⟨g, h₁, h₂, h₃⟩ := hn; ⟨g, h₁, h₂, h₃.filter_mono nhdsWithin_le_nhds⟩)

Premises used: Filter.Eventually.filter_mono, Compl.compl, nhdsWithin, Filter.Eventually, HSub.hSub, Exists, Int.ofNat_inj, _private.0.AnalyticAt.unique_eventuallyEq_pow_smul_nonzero.match_1, Ne, Nat.cast, And, nhdsWithin_le_nhds, HPow.hPow, AnalyticAt, And.intro, Exists.intro, Iff.mp, HSMul.hSMul, AnalyticAt.unique_eventuallyEq_zpow_smul_nonzero, Singleton.singleton, OfNat.ofNat, Eq
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
mp :
  (∃ (n : ℕ) (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) →
    ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
mpr :
  (¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0) →
    ∃ (n : ℕ) (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
⊢ (∃ (n : ℕ) (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z) ↔
    ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0

Tactic:
constructor
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
hg_ne : g z₀ ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
mp : ∀ (hg_ne : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0), g z₀ = 0
⊢ ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0

Tactic:
contrapose hg_ne
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
hg_ne : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
mp : g =ᶠ[𝓝 z₀] fun {z₀ : 𝕜} ↦ 0
⊢ g z₀ = 0

Tactic:
apply EventuallyEq.eq_of_nhds

Premises used: Filter.EventuallyEq.eq_of_nhds
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
hg_ne : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
mp : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, g z = 0
⊢ g =ᶠ[𝓝 z₀] fun {z₀ : 𝕜} ↦ 0

Tactic:
rw [EventuallyEq, ← AnalyticAt.frequently_eq_iff_eventually_eq hg_an analyticAt_const]

Premises used: Filter.EventuallyEq, analyticAt_const, AnalyticAt.frequently_eq_iff_eventually_eq
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
hg_ne : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
⊢ ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, g z = 0

Tactic:
(eventually_nhdsWithin_iff.mpr ?_).frequently

Premises used: Iff.mpr, eventually_nhdsWithin_iff, Filter.Eventually.frequently
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
hg_ne : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
mp : ∀ᶠ (x : 𝕜) in 𝓝 z₀, Membership.mem (γ := Set 𝕜) {z₀}ᶜ x → g x = 0
⊢ ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, g z = 0

Tactic:
refine (eventually_nhdsWithin_iff.mpr ?_).frequently

Premises used: Iff.mpr, eventually_nhdsWithin_iff, Filter.Eventually.frequently
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
hg_ne : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
h : ∀ (z : 𝕜) (hf_eq : f z = (z - z₀) ^ n • g z) (hf0 : f z = 0) (hz : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z), g z = 0
⊢ ∀ᶠ (x : 𝕜) in 𝓝 z₀, Membership.mem (γ := Set 𝕜) {z₀}ᶜ x → g x = 0

Tactic:
filter_upwards [hg_eq, hg_ne] with z hf_eq hf0 hz
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
hg_ne : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
z : 𝕜
hf_eq : f z = (z - z₀) ^ n • g z
hf0 : f z = 0
hz : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z
h : ∀ (hf_eq : (z - z₀) ^ n • g z = 0) (hf0 : f z = 0) (hz : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z), (z - z₀) ^ n ≠ 0
⊢ g z = 0

Tactic:
rwa [hf0, eq_comm, smul_eq_zero_iff_right] at hf_eq

Premises used: eq_comm, smul_eq_zero_iff_right
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
hg_ne : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
z : 𝕜
hf_eq : (z - z₀) ^ n • g z = 0
hf0 : f z = 0
hz : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z
⊢ (z - z₀) ^ n ≠ 0

Tactic:
pow_ne_zero _ (sub_ne_zero.mpr hz)

Premises used: Iff.mpr, sub_ne_zero, pow_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
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
g : 𝕜 → E
hg_an : AnalyticAt 𝕜 g z₀
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
hg_ne : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
z : 𝕜
hf_eq : (z - z₀) ^ n • g z = 0
hf0 : f z = 0
hz : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z
⊢ (z - z₀) ^ n ≠ 0

Tactic:
exact pow_ne_zero _ (sub_ne_zero.mpr hz)

Premises used: Iff.mpr, sub_ne_zero, pow_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
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
hf_ne : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
mpr :
  ∀ (p : FormalMultilinearSeries 𝕜 𝕜 E) (hp : HasFPowerSeriesAt f p z₀),
    ∃ (n : ℕ) (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z
⊢ ∃ (n : ℕ) (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z

Tactic:
rcases hf with ⟨p, hp⟩
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf_ne : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
p : FormalMultilinearSeries 𝕜 𝕜 E
hp : HasFPowerSeriesAt f p z₀
⊢ ∃ (n : ℕ) (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z

Tactic:
⟨p.order, _, ⟨_, hp.has_fpower_series_iterate_dslope_fslope p.order⟩,
      hp.iterate_dslope_fslope_ne_zero (hf_ne.imp hp.locally_zero_iff.mpr),
      .of_forall hp.eq_pow_order_mul_iterate_dslope⟩

Premises used: Iff.mpr, HasFPowerSeriesAt.iterate_dslope_fslope_ne_zero, HasFPowerSeriesAt.eq_pow_order_mul_iterate_dslope, FormalMultilinearSeries.order, Filter.Eventually.of_forall, Not.imp, HasFPowerSeriesAt.has_fpower_series_iterate_dslope_fslope, And.intro, Exists.intro, HasFPowerSeriesAt.locally_zero_iff
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf_ne : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
p : FormalMultilinearSeries 𝕜 𝕜 E
hp : HasFPowerSeriesAt f p z₀
⊢ ∃ (n : ℕ) (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ n • g z

Tactic:
exact ⟨p.order, _, ⟨_, hp.has_fpower_series_iterate_dslope_fslope p.order⟩,
      hp.iterate_dslope_fslope_ne_zero (hf_ne.imp hp.locally_zero_iff.mpr),
      .of_forall hp.eq_pow_order_mul_iterate_dslope⟩
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
h₀ : z₀ ∈ U
hfw : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = 0
⊢ EqOn f 0 U

Tactic:
hf.eqOn_zero_of_preconnected_of_eventuallyEq_zero hU h₀
    ((hf z₀ h₀).frequently_zero_iff_eventually_zero.1 hfw)

Premises used: AnalyticAt.frequently_zero_iff_eventually_zero, Iff.mp, AnalyticOnNhd.eqOn_zero_of_preconnected_of_eventuallyEq_zero
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
simp : (∃ (x : 𝕜) (_ : x ∈ U), (U \ {x : 𝕜 | ¬f x = 0})ᶜ ∉ 𝓝[≠] x) → EqOn f 0 U
⊢ EqOn f 0 U ∨ ∀ᶠ (x : 𝕜) in codiscreteWithin U, f x ≠ 0

Tactic:
simp only [or_iff_not_imp_right, ne_eq, eventually_iff, mem_codiscreteWithin,
    disjoint_principal_right, not_forall]

Premises used: Classical.or_iff_not_imp_right, Filter.eventually_iff, ne_eq, mem_codiscreteWithin, Classical.not_forall, Filter.disjoint_principal_right
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
x : 𝕜
hx : x ∈ U
hx2 : (U \ {x : 𝕜 | ¬f x = 0})ᶜ ∉ 𝓝[≠] x
⊢ EqOn f 0 U

Tactic:
hf.eqOn_zero_of_preconnected_of_frequently_eq_zero hU hx fun nh ↦ hx2 ?_

Premises used: AnalyticOnNhd.eqOn_zero_of_preconnected_of_frequently_eq_zero
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
x : 𝕜
hx : x ∈ U
hx2 : (U \ {x : 𝕜 | ¬f x = 0})ᶜ ∉ 𝓝[≠] x
refine : ∀ (nh : ∀ᶠ (x : 𝕜) in 𝓝[≠] x, ¬(fun (z : 𝕜) ↦ f z = 0) x), (U \ {x : 𝕜 | ¬f x = 0})ᶜ ∈ 𝓝[≠] x
⊢ EqOn f 0 U

Tactic:
refine hf.eqOn_zero_of_preconnected_of_frequently_eq_zero hU hx fun nh ↦ hx2 ?_

Premises used: AnalyticOnNhd.eqOn_zero_of_preconnected_of_frequently_eq_zero
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
x : 𝕜
hx : x ∈ U
hx2 : (U \ {x : 𝕜 | ¬f x = 0})ᶜ ∉ 𝓝[≠] x
nh : ∀ᶠ (x : 𝕜) in 𝓝[≠] x, ¬(fun (z : 𝕜) ↦ f z = 0) x
h : ∀ (a : 𝕜) (ha : ¬f a = 0), a ∈ (U \ {x : 𝕜 | ¬f x = 0})ᶜ
⊢ (U \ {x : 𝕜 | ¬f x = 0})ᶜ ∈ 𝓝[≠] x

Tactic:
filter_upwards [nh] with a ha
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
x : 𝕜
hx : x ∈ U
hx2 : (U \ {x : 𝕜 | ¬f x = 0})ᶜ ∉ 𝓝[≠] x
nh : ∀ᶠ (x : 𝕜) in 𝓝[≠] x, ¬(fun (z : 𝕜) ↦ f z = 0) x
a : 𝕜
ha : ¬f a = 0
⊢ a ∈ (U \ {x : 𝕜 | ¬f x = 0})ᶜ

Tactic:
simp_all
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
h₀ : z₀ ∈ U
hfz₀ :
  Membership.mem (γ := Set 𝕜) (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ({z : 𝕜 | f z = 0} \ {z₀}))
    z₀
⊢ EqOn f 0 U

Tactic:
hf.eqOn_zero_of_preconnected_of_frequently_eq_zero hU h₀
    (mem_closure_ne_iff_frequently_within.mp hfz₀)

Premises used: mem_closure_ne_iff_frequently_within, AnalyticOnNhd.eqOn_zero_of_preconnected_of_frequently_eq_zero, 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
f g : 𝕜 → E
z₀ : 𝕜
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hU : IsPreconnected U
h₀ : z₀ ∈ U
hfg : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = g z
z : 𝕜
h : f z = g z
rw : f z - g z = 0
rw₁ : g z - g z = 0
rw₂ rw₃ : Eq.{u_2 + 1} (α := E) 0 0
⊢ (f - g) z = 0

Tactic:
rw [Pi.sub_apply, h, sub_self]

Premises used: sub_self, Pi.sub_apply
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hU : IsPreconnected U
h₀ : z₀ ∈ U
hfg : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = g z
⊢ ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, (f - g) z = 0

Tactic:
have hfg' : ∃ᶠ z in 𝓝[≠] z₀, (f - g) z = 0 :=
    hfg.mono fun z h => by rw [Pi.sub_apply, h, sub_self]
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hU : IsPreconnected U
h₀ : z₀ ∈ U
hfg : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = g z
hfg' : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, (f - g) z = 0
⊢ EqOn f g U

Tactic:
simpa [sub_eq_zero] using fun z hz =>
    (hf.sub hg).eqOn_zero_of_preconnected_of_frequently_eq_zero hU h₀ hfg' hz

Premises used: sub_eq_zero, AnalyticOnNhd.eqOn_zero_of_preconnected_of_frequently_eq_zero, AnalyticOnNhd.sub
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hU : IsPreconnected U
⊢ (∀ᶠ (x : 𝕜) in codiscreteWithin U, (f - g) x ≠ 0) → ∀ᶠ (x : 𝕜) in codiscreteWithin U, f x ≠ g x

Tactic:
simp only [Pi.sub_apply, ne_eq, sub_eq_zero, imp_self]

Premises used: sub_eq_zero, ne_eq, imp_self, Pi.sub_apply
-- Module: Mathlib.Analysis.Analytic.IsolatedZeros
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hU : IsPreconnected U
h₀ : z₀ ∈ U
hfg :
  Membership.mem (γ := Set 𝕜)
    (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ({z : 𝕜 | f z = g z} \ {z₀})) z₀
⊢ EqOn f g U

Tactic:
hf.eqOn_of_preconnected_of_frequently_eq hg hU h₀ (mem_closure_ne_iff_frequently_within.mp hfg)

Premises used: mem_closure_ne_iff_frequently_within, AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq, Iff.mp