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
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)
rw₆ rw₇ : Eq.{u_2 + 1} (α := E) 0 0
⊢ (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope z₀)^[k] f z₀ = 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]

Premises used: FormalMultilinearSeries.coeff, zero_add, HasFPowerSeriesAt.has_fpower_series_iterate_dslope_fslope, FormalMultilinearSeries.apply_eq_zero_of_lt_order, FormalMultilinearSeries.coeff_iterate_fslope, HasFPowerSeriesAt.coeff_zero, ContinuousMultilinearMap.zero_apply, 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
rw : ∀ᶠ (x : 𝕜) in 𝓝 z₀, Membership.mem (γ := Set 𝕜) {z₀}ᶜ x → f x ≠ 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0

Tactic:
rw [eventually_nhdsWithin_iff]

Premises used: eventually_nhdsWithin_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₀ : 𝕜
hp : HasFPowerSeriesAt (𝕜 := 𝕜) f p z₀
h : p ≠ 0
⊢ 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
-- 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
h2 : ContinuousAt ((swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope z₀)^[p.order] f) z₀
⊢ ∀ᶠ (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)
-- 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
h2 : ContinuousAt ((swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope z₀)^[p.order] f) z₀
h3 : ∀ᶠ (z : 𝕜) in 𝓝 z₀, (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope z₀)^[p.order] f z ≠ 0
h₁ :
  ∀ (z : 𝕜) (e1 : (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope z₀)^[p.order] f z ≠ 0)
    (e2 : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z), f z ≠ 0
⊢ ∀ᶠ (x : 𝕜) in 𝓝 z₀, Membership.mem (γ := Set 𝕜) {z₀}ᶜ x → f x ≠ 0

Tactic:
filter_upwards [h3] with z e1 e2
-- 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
h2 : ContinuousAt ((swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope z₀)^[p.order] f) z₀
h3 : ∀ᶠ (z : 𝕜) in 𝓝 z₀, (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope z₀)^[p.order] f z ≠ 0
z : 𝕜
e1 : (swap (φ := fun (x : 𝕜 → E) (y : 𝕜) ↦ 𝕜 → E) dslope z₀)^[p.order] f z ≠ 0
e2 : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z
⊢ f z ≠ 0

Tactic:
simpa [eq_pow_order_mul_iterate_dslope hp, e1, e2] using pow_ne_zero p.order (sub_ne_zero.mpr e2)

Premises used: Iff.mpr, HasFPowerSeriesAt.eq_pow_order_mul_iterate_dslope, sub_ne_zero, FormalMultilinearSeries.order, 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
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hp : HasFPowerSeriesAt (𝕜 := 𝕜) f p z₀
h : p = 0
rwa rwa₁ rwa₂ rwa₃ : ∀ (hp : HasFPowerSeriesAt (𝕜 := 𝕜) f 0 z₀) (h : p = 0), HasFPowerSeriesAt (𝕜 := 𝕜) f 0 z₀
⊢ HasFPowerSeriesAt (𝕜 := 𝕜) f 0 z₀

Tactic:
rwa [h] at 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 : AnalyticAt 𝕜 f z₀
rcases :
  ∀ (p : FormalMultilinearSeries 𝕜 𝕜 E) (hp : HasFPowerSeriesAt f p z₀),
    (∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0
⊢ (∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0

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₀ : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
hp : HasFPowerSeriesAt f p z₀
pos : ∀ (h : p = 0), (∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0
neg : ∀ (h : ¬p = 0), (∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0
⊢ (∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0

Tactic:
by_cases h : p = 0
-- 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₀ : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
hp : HasFPowerSeriesAt f p z₀
h : p = 0
rwa rwa₁ rwa₂ rwa₃ : ∀ (hp : HasFPowerSeriesAt (𝕜 := 𝕜) f 0 z₀) (h : p = 0), HasFPowerSeriesAt (𝕜 := 𝕜) f 0 z₀
⊢ HasFPowerSeriesAt (𝕜 := 𝕜) f 0 z₀

Tactic:
rwa [h] at 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₀ : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
hp : HasFPowerSeriesAt f p z₀
h : p = 0
⊢ (∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0

Tactic:
exact Or.inl (HasFPowerSeriesAt.eventually_eq_zero (by rwa [h] at hp))

Premises used: HasFPowerSeriesAt.eventually_eq_zero, Or.inl
-- 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₀ : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
hp : HasFPowerSeriesAt f p z₀
h : ¬p = 0
⊢ (∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0

Tactic:
Or.inr (hp.locally_ne_zero h)

Premises used: HasFPowerSeriesAt.locally_ne_zero, Or.inr
-- 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₀ : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 E
hp : HasFPowerSeriesAt f p z₀
h : ¬p = 0
⊢ (∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ 0

Tactic:
exact Or.inr (hp.locally_ne_zero h)

Premises used: HasFPowerSeriesAt.locally_ne_zero, Or.inr
-- 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₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
⊢ (∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = g z) ∨ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z ≠ g z

Tactic:
simpa [sub_eq_zero] using (hf.sub hg).eventually_eq_zero_or_eventually_ne_zero

Premises used: sub_eq_zero, AnalyticAt.sub, AnalyticAt.eventually_eq_zero_or_eventually_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
w : 𝕜
hf : AnalyticAt 𝕜 f w
⊢ (∃ᶠ (z : 𝕜) in 𝓝[≠] w, f z = 0) ↔ ∀ᶠ (z : 𝕜) in 𝓝 w, f z = 0

Tactic:
⟨hf.eventually_eq_zero_or_eventually_ne_zero.resolve_right, fun h =>
    (h.filter_mono nhdsWithin_le_nhds).frequently⟩

Premises used: Filter.Eventually.filter_mono, nhdsWithin_le_nhds, Iff.intro, AnalyticAt.eventually_eq_zero_or_eventually_ne_zero, Filter.Eventually.frequently, Or.resolve_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 g : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : AnalyticAt 𝕜 g z₀
⊢ (∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = g z) ↔ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = g z

Tactic:
simpa [sub_eq_zero] using frequently_zero_iff_eventually_zero (hf.sub hg)

Premises used: sub_eq_zero, AnalyticAt.frequently_zero_iff_eventually_zero, AnalyticAt.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 : 𝕜 → 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
inr :
  ∀
    (this :
      ∀ {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), m = n)
    (h_le : m < n), m = n
wlog! :
  ∀ {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),
    m = n
⊢ m = n

Tactic:
wlog! h_le : n ≤ m generalizing 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
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
this :
  ∀ {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),
    m = n
h_le : m < n
⊢ m = n

Tactic:
((this hn hm) h_le.le).symm

Premises used: LT.lt.le, 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
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
this :
  ∀ {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),
    m = n
h_le : m < n
⊢ m = n

Tactic:
exact ((this hn hm) h_le.le).symm

Premises used: LT.lt.le, 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
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
let :
  ∀ (g : 𝕜 → E) (hg_an : AnalyticAt 𝕜 g z₀),
    g z₀ ≠ 0 → ∀ (hg_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z), m = n
⊢ m = n

Tactic:
let ⟨g, hg_an, _, hg_eq⟩ := hm
-- 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
let :
  ∀ (j : 𝕜 → E) (hj_an : AnalyticAt 𝕜 j z₀) (hj_ne : j z₀ ≠ 0)
    (hj_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • j z), m = n
⊢ m = n

Tactic:
let ⟨j, hj_an, hj_ne, hj_eq⟩ := hn
-- 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_ne : j z₀ ≠ 0
hj_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • j z
contrapose! : ∀ (hj_ne : m ≠ n), j z₀ = 0
⊢ m = n

Tactic:
contrapose! hj_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₀ : 𝕜
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
h : ∀ᶠ (x : 𝕜) in 𝓝[≠] z₀, j x = (x - z₀) ^ (m - n) • g x
⊢ ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, j z = (z - z₀) ^ (m - n) • g z

Tactic:
apply Filter.Eventually.frequently

Premises used: 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₀ : 𝕜
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
h :
  ∀ (hg_eq : ∀ᶠ (x : 𝕜) in 𝓝 z₀, Membership.mem (γ := Set 𝕜) {z₀}ᶜ x → f x = (x - z₀) ^ m • g x) (j : 𝕜 → E)
    (hj_an : AnalyticAt 𝕜 j z₀)
    (hj_eq : ∀ᶠ (x : 𝕜) in 𝓝 z₀, Membership.mem (γ := Set 𝕜) {z₀}ᶜ x → f x = (x - z₀) ^ n • j x) (hj_ne : m ≠ n),
    ∀ᶠ (x : 𝕜) in 𝓝 z₀, Membership.mem (γ := Set 𝕜) {z₀}ᶜ x → j x = (x - z₀) ^ (m - n) • g x
⊢ ∀ᶠ (x : 𝕜) in 𝓝[≠] z₀, j x = (x - z₀) ^ (m - n) • g x

Tactic:
rw [eventually_nhdsWithin_iff] at hg_eq hj_eq ⊢

Premises used: eventually_nhdsWithin_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₀ : 𝕜
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 : ∀ᶠ (x : 𝕜) in 𝓝 z₀, Membership.mem (γ := Set 𝕜) {z₀}ᶜ x → f x = (x - z₀) ^ m • g x
j : 𝕜 → E
hj_an : AnalyticAt 𝕜 j z₀
hj_eq : ∀ᶠ (x : 𝕜) in 𝓝 z₀, Membership.mem (γ := Set 𝕜) {z₀}ᶜ x → f x = (x - z₀) ^ n • j x
hj_ne : m ≠ n
h :
  ∀ (z : 𝕜) (hfz : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z → f z = (z - z₀) ^ m • g z)
    (hfz' : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z → f z = (z - z₀) ^ n • j z) (hz : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z),
    j z = (z - z₀) ^ (m - n) • g z
⊢ ∀ᶠ (x : 𝕜) in 𝓝 z₀, Membership.mem (γ := Set 𝕜) {z₀}ᶜ x → j x = (x - z₀) ^ (m - n) • g x

Tactic:
filter_upwards [hg_eq, hj_eq] with z hfz hfz' 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₀ : 𝕜
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 : ∀ᶠ (x : 𝕜) in 𝓝 z₀, Membership.mem (γ := Set 𝕜) {z₀}ᶜ x → f x = (x - z₀) ^ m • g x
j : 𝕜 → E
hj_an : AnalyticAt 𝕜 j z₀
hj_eq : ∀ᶠ (x : 𝕜) in 𝓝 z₀, Membership.mem (γ := Set 𝕜) {z₀}ᶜ x → f x = (x - z₀) ^ n • j x
hj_ne : m ≠ n
z : 𝕜
hfz : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z → f z = (z - z₀) ^ m • g z
hfz' : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z → f z = (z - z₀) ^ n • j z
hz : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z
⊢ Membership.mem (γ := Set 𝕜) {z₀}ᶜ z → j z = (z - z₀) ^ (m - n) • g z

Tactic:
rw [← add_sub_cancel_left n m, add_sub_assoc, zpow_add₀ <| sub_ne_zero.mpr hz, mul_smul,
      hfz' hz, smul_right_inj <| zpow_ne_zero _ <| sub_ne_zero.mpr hz] at hfz

Premises used: Iff.mpr, add_sub_assoc, add_sub_cancel_left, sub_ne_zero, zpow_add₀, zpow_ne_zero, SemigroupAction.mul_smul, smul_right_inj
-- 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 : ∀ᶠ (x : 𝕜) in 𝓝 z₀, Membership.mem (γ := Set 𝕜) {z₀}ᶜ x → f x = (x - z₀) ^ m • g x
j : 𝕜 → E
hj_an : AnalyticAt 𝕜 j z₀
hj_eq : ∀ᶠ (x : 𝕜) in 𝓝 z₀, Membership.mem (γ := Set 𝕜) {z₀}ᶜ x → f x = (x - z₀) ^ n • j x
hj_ne : m ≠ n
z : 𝕜
hfz : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z → f z = (z - z₀) ^ m • g z
hfz' : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z → f z = (z - z₀) ^ n • j z
hz : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z
hfz₁ : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z → j z = (z - z₀) ^ (m - n) • g z
⊢ Membership.mem (γ := Set 𝕜) {z₀}ᶜ z → f z = (z - z₀) ^ n • j z

Tactic:
rw [← add_sub_cancel_left n m, add_sub_assoc, zpow_add₀ <| sub_ne_zero.mpr hz, mul_smul,
      hfz' hz, smul_right_inj <| zpow_ne_zero _ <| sub_ne_zero.mpr hz] at hfz

Premises used: Iff.mpr, add_sub_assoc, add_sub_cancel_left, sub_ne_zero, zpow_add₀, zpow_ne_zero, SemigroupAction.mul_smul, smul_right_inj
-- 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 : ∀ᶠ (x : 𝕜) in 𝓝 z₀, Membership.mem (γ := Set 𝕜) {z₀}ᶜ x → f x = (x - z₀) ^ m • g x
j : 𝕜 → E
hj_an : AnalyticAt 𝕜 j z₀
hj_eq : ∀ᶠ (x : 𝕜) in 𝓝 z₀, Membership.mem (γ := Set 𝕜) {z₀}ᶜ x → f x = (x - z₀) ^ n • j x
hj_ne : m ≠ n
z : 𝕜
hfz : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z → f z = (z - z₀) ^ m • g z
hfz' : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z → f z = (z - z₀) ^ n • j z
hz : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z
hfz₁ : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z → j z = (z - z₀) ^ (m - n) • g z
hfz'₁ : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z → f z = (z - z₀) ^ n • j z
⊢ Membership.mem (γ := Set 𝕜) {z₀}ᶜ z

Tactic:
rw [← add_sub_cancel_left n m, add_sub_assoc, zpow_add₀ <| sub_ne_zero.mpr hz, mul_smul,
      hfz' hz, smul_right_inj <| zpow_ne_zero _ <| sub_ne_zero.mpr hz] at hfz

Premises used: Iff.mpr, add_sub_assoc, add_sub_cancel_left, sub_ne_zero, zpow_add₀, zpow_ne_zero, SemigroupAction.mul_smul, smul_right_inj
-- 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 : ∀ᶠ (x : 𝕜) in 𝓝 z₀, Membership.mem (γ := Set 𝕜) {z₀}ᶜ x → f x = (x - z₀) ^ m • g x
j : 𝕜 → E
hj_an : AnalyticAt 𝕜 j z₀
hj_eq : ∀ᶠ (x : 𝕜) in 𝓝 z₀, Membership.mem (γ := Set 𝕜) {z₀}ᶜ x → f x = (x - z₀) ^ n • j x
hj_ne : m ≠ n
z : 𝕜
hfz : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z → j z = (z - z₀) ^ (m - n) • g z
hfz' : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z → f z = (z - z₀) ^ n • j z
hz : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z
⊢ j z = (z - z₀) ^ (m - n) • g z

Tactic:
hfz 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₀ : 𝕜
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 : ∀ᶠ (x : 𝕜) in 𝓝 z₀, Membership.mem (γ := Set 𝕜) {z₀}ᶜ x → f x = (x - z₀) ^ m • g x
j : 𝕜 → E
hj_an : AnalyticAt 𝕜 j z₀
hj_eq : ∀ᶠ (x : 𝕜) in 𝓝 z₀, Membership.mem (γ := Set 𝕜) {z₀}ᶜ x → f x = (x - z₀) ^ n • j x
hj_ne : m ≠ n
z : 𝕜
hfz : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z → j z = (z - z₀) ^ (m - n) • g z
hfz' : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z → f z = (z - z₀) ^ n • j z
hz : Membership.mem (γ := Set 𝕜) {z₀}ᶜ z
⊢ j z = (z - z₀) ^ (m - n) • g z

Tactic:
exact hfz 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₀ : 𝕜
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
⊢ ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, j z = (z - z₀) ^ (m - n) • g z

Tactic:
have : ∃ᶠ z in 𝓝[≠] z₀, j z = (z - z₀) ^ (m - n) • g z := by
    apply Filter.Eventually.frequently
    rw [eventually_nhdsWithin_iff] at hg_eq hj_eq ⊢
    filter_upwards [hg_eq, hj_eq] with z hfz hfz' hz
    rw [← add_sub_cancel_left n m, add_sub_assoc, zpow_add₀ <| sub_ne_zero.mpr hz, mul_smul,
      hfz' hz, smul_right_inj <| zpow_ne_zero _ <| sub_ne_zero.mpr hz] at hfz
    exact hfz 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₀ : 𝕜
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 : ∀ (this : ∀ᶠ (z : 𝕜) in 𝓝 z₀, j z = (z - z₀) ^ (m - n) • g z), j z₀ = 0
rw₁ : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - z₀) ^ (m - n) • g z) z₀
⊢ j z₀ = 0

Tactic:
rw [frequently_eq_iff_eventually_eq hj_an] at this

Premises used: AnalyticAt.frequently_eq_iff_eventually_eq