awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
h_eq : ¬EventuallyEq.{u_1, u_2} (β := 𝕜') (𝓝 x) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) 0
n : ℕ
g : 𝕜 → 𝕜'
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ m • f z = (z - x) ^ n • g z
this : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ (m + 1)) x
h :
  ∀ (z : 𝕜) (hfg : (z - x) ^ m • f z = (z - x) ^ n • g z) (hg_ne' : g z ≠ 0),
    (z - x) ^ (m + 1) • g⁻¹ z = (z - x) ^ (n + 1) • f⁻¹ z
⊢ EventuallyEq.{u_1, u_2} (β := 𝕜') (𝓝 x) (fun (i : 𝕜) ↦ (i - x) ^ (m + 1) • g⁻¹ i) fun (z : 𝕜) ↦
    (z - x) ^ (n + 1) • f⁻¹ z

Tactic:
filter_upwards [hg_eq, hg_an.continuousAt.eventually_ne hg_ne] with z hfg hg_ne'

Premises used: ContinuousAt.eventually_ne, AnalyticAt.continuousAt
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
h_eq : ¬EventuallyEq.{u_1, u_2} (β := 𝕜') (𝓝 x) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) 0
n : ℕ
g : 𝕜 → 𝕜'
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ m • f z = (z - x) ^ n • g z
this : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ (m + 1)) x
z : 𝕜
hfg : (z - x) ^ m • f z = (z - x) ^ n • g z
hg_ne' : g z ≠ 0
h :
  ∀ (hf : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z_1 : 𝕜) ↦ (z_1 - z) ^ m • f z_1) z)
    (h_eq : ¬EventuallyEq.{u_1, u_2} (β := 𝕜') (𝓝 z) (fun (z_1 : 𝕜) ↦ (z_1 - z) ^ m • f z_1) 0)
    (hg_an : AnalyticAt 𝕜 g z) (hg_ne : g z ≠ 0)
    (hg_eq : ∀ᶠ (z_1 : 𝕜) in 𝓝 z, (z_1 - z) ^ m • f z_1 = (z_1 - z) ^ n • g z_1)
    (this : AnalyticAt 𝕜 (F := 𝕜) (fun (z_1 : 𝕜) ↦ (z_1 - z) ^ (m + 1)) z)
    (hfg : (z - z) ^ m • f z = (z - z) ^ n • g z), (z - z) ^ (m + 1) • g⁻¹ z = (z - z) ^ (n + 1) • f⁻¹ z
h₁ : ∀ (hz_ne : z ≠ x), (z - x) ^ (m + 1) • g⁻¹ z = (z - x) ^ (n + 1) • f⁻¹ z
⊢ (z - x) ^ (m + 1) • g⁻¹ z = (z - x) ^ (n + 1) • f⁻¹ z

Tactic:
rcases eq_or_ne z x with rfl | hz_ne

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
f : 𝕜 → 𝕜'
m n : ℕ
g : 𝕜 → 𝕜'
z : 𝕜
hg_ne' : g z ≠ 0
hf : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z_1 : 𝕜) ↦ (z_1 - z) ^ m • f z_1) z
h_eq : ¬EventuallyEq.{u_1, u_2} (β := 𝕜') (𝓝 z) (fun (z_1 : 𝕜) ↦ (z_1 - z) ^ m • f z_1) 0
hg_an : AnalyticAt 𝕜 g z
hg_ne : g z ≠ 0
hg_eq : ∀ᶠ (z_1 : 𝕜) in 𝓝 z, (z_1 - z) ^ m • f z_1 = (z_1 - z) ^ n • g z_1
this : AnalyticAt 𝕜 (F := 𝕜) (fun (z_1 : 𝕜) ↦ (z_1 - z) ^ (m + 1)) z
hfg : (z - z) ^ m • f z = (z - z) ^ n • g z
⊢ (z - z) ^ (m + 1) • g⁻¹ z = (z - z) ^ (n + 1) • f⁻¹ z

Tactic:
simp
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
h_eq : ¬EventuallyEq.{u_1, u_2} (β := 𝕜') (𝓝 x) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) 0
n : ℕ
g : 𝕜 → 𝕜'
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ m • f z = (z - x) ^ n • g z
this : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ (m + 1)) x
z : 𝕜
hfg : (z - x) ^ m • f z = (z - x) ^ n • g z
hg_ne' : g z ≠ 0
hz_ne : z ≠ x
⊢ Eq.{u_2 + 1} (α := 𝕜') ((fun (x : 𝕜') ↦ x⁻¹) ((z - x) ^ m • f z)) ((fun (x : 𝕜') ↦ x⁻¹) ((z - x) ^ n • g z))

Tactic:
replace hfg := congr_arg (·⁻¹) hfg
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
h_eq : ¬EventuallyEq.{u_1, u_2} (β := 𝕜') (𝓝 x) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) 0
n : ℕ
g : 𝕜 → 𝕜'
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ m • f z = (z - x) ^ n • g z
this : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ (m + 1)) x
z : 𝕜
hg_ne' : g z ≠ 0
hz_ne : z ≠ x
hfg : Eq.{u_2 + 1} (α := 𝕜') ((fun (x : 𝕜') ↦ x⁻¹) ((z - x) ^ m • f z)) ((fun (x : 𝕜') ↦ x⁻¹) ((z - x) ^ n • g z))
⊢ ((z - x) ^ m)⁻¹ • (f z)⁻¹ = ((z - x) ^ n)⁻¹ • (g z)⁻¹

Tactic:
simp only [smul_inv₀] at hfg

Premises used: smul_inv₀
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
h_eq : ¬EventuallyEq.{u_1, u_2} (β := 𝕜') (𝓝 x) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) 0
n : ℕ
g : 𝕜 → 𝕜'
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ m • f z = (z - x) ^ n • g z
this : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ (m + 1)) x
z : 𝕜
hg_ne' : g z ≠ 0
hz_ne : z ≠ x
hfg : ((z - x) ^ m)⁻¹ • (f z)⁻¹ = ((z - x) ^ n)⁻¹ • (g z)⁻¹
⊢ (z - x) ^ n • (f z)⁻¹ = (z - x) ^ m • (g z)⁻¹

Tactic:
rw [inv_smul_eq_iff₀ (pow_ne_zero m (sub_ne_zero.mpr hz_ne)), smul_comm,
        eq_inv_smul_iff₀ (pow_ne_zero n (sub_ne_zero.mpr hz_ne))] at hfg

Premises used: Iff.mpr, sub_ne_zero, pow_ne_zero, inv_smul_eq_iff₀, SMulCommClass.smul_comm, eq_inv_smul_iff₀
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
h_eq : ¬EventuallyEq.{u_1, u_2} (β := 𝕜') (𝓝 x) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) 0
n : ℕ
g : 𝕜 → 𝕜'
hg_an : AnalyticAt 𝕜 g x
hg_ne : g x ≠ 0
hg_eq : ∀ᶠ (z : 𝕜) in 𝓝 x, (z - x) ^ m • f z = (z - x) ^ n • g z
this : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ (m + 1)) x
z : 𝕜
hg_ne' : g z ≠ 0
hz_ne : z ≠ x
hfg : (z - x) ^ n • (f z)⁻¹ = (z - x) ^ m • (g z)⁻¹
⊢ (z - x) ^ (m + 1) • g⁻¹ z = (z - x) ^ (n + 1) • f⁻¹ z

Tactic:
simp [pow_succ', mul_smul, hfg]

Premises used: SemigroupAction.mul_smul, pow_succ'
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
h : MeromorphicAt f⁻¹ x
⊢ MeromorphicAt f x

Tactic:
simpa only [inv_inv] using h.inv

Premises used: inv_inv, MeromorphicAt.inv
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f g : 𝕜 → 𝕜'
hf : MeromorphicAt f x
hg : MeromorphicAt g x
⊢ MeromorphicAt (f / g) x

Tactic:
(div_eq_mul_inv f g).symm ▸ (hf.mul hg.inv)

Premises used: MeromorphicAt.mul, Eq.rec, div_eq_mul_inv, MeromorphicAt.inv, Eq.symm
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : MeromorphicAt f x
⊢ MeromorphicAt (HPow.hPow (β := ℕ) f 0) x

Tactic:
simpa only [pow_zero] using MeromorphicAt.const 1 x

Premises used: MeromorphicAt.const, pow_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : MeromorphicAt f x
m : ℕ
hm : MeromorphicAt (f ^ m) x
⊢ MeromorphicAt (f ^ (m + 1)) x

Tactic:
simpa only [pow_succ] using hm.mul hf

Premises used: MeromorphicAt.mul, pow_succ
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : MeromorphicAt f x
n : ℕ
zero : MeromorphicAt (HPow.hPow (β := ℕ) f 0) x
succ : ∀ (m : ℕ) (hm : MeromorphicAt (f ^ m) x), MeromorphicAt (f ^ (m + 1)) x
⊢ MeromorphicAt (f ^ n) x

Tactic:
induction n with
  | zero => simpa only [pow_zero] using MeromorphicAt.const 1 x
  | succ m hm => simpa only [pow_succ] using hm.mul hf

Premises used: pow_succ, MeromorphicAt.const, pow_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : MeromorphicAt f x
m : ℕ
⊢ MeromorphicAt (f ^ Int.ofNat m) x

Tactic:
simpa only [Int.ofNat_eq_natCast, zpow_natCast] using hf.pow m

Premises used: zpow_natCast, Int.ofNat_eq_natCast, MeromorphicAt.pow
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : MeromorphicAt f x
m : ℕ
⊢ MeromorphicAt (f ^ Int.negSucc m) x

Tactic:
simpa only [zpow_negSucc, inv_iff] using hf.pow (m + 1)

Premises used: MeromorphicAt.inv_iff, zpow_negSucc, MeromorphicAt.pow, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
x : 𝕜
f : 𝕜 → 𝕜'
hf : MeromorphicAt f x
n : ℤ
ofNat : ∀ (m : ℕ), MeromorphicAt (f ^ Int.ofNat m) x
negSucc : ∀ (m : ℕ), MeromorphicAt (f ^ Int.negSucc m) x
⊢ MeromorphicAt (f ^ n) x

Tactic:
cases n with
  | ofNat m => simpa only [Int.ofNat_eq_natCast, zpow_natCast] using hf.pow m
  | negSucc m => simpa only [zpow_negSucc, inv_iff] using hf.pow (m + 1)

Premises used: zpow_natCast, MeromorphicAt.inv_iff, zpow_negSucc, Int.ofNat_eq_natCast
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h : MeromorphicAt f x
obtain :
  ∀ (n : ℕ) (h : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x),
    ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ContinuousAt f y
⊢ ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ContinuousAt f y

Tactic:
obtain ⟨n, h⟩ := h
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
n : ℕ
h : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x
⊢ ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ContinuousAt.{u_1, u_3} (Y := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y

Tactic:
have : ∀ᶠ y in 𝓝[≠] x, ContinuousAt (fun z ↦ (z - x) ^ n • f z) y :=
    nhdsWithin_le_nhds h.eventually_continuousAt
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
n : ℕ
h : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x
this : ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ContinuousAt.{u_1, u_3} (Y := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
h₁ :
  ∀ (y : 𝕜) (hy : ContinuousAt.{u_1, u_3} (Y := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y)
    (h'y : Membership.mem (γ := Set 𝕜) {x}ᶜ y), ContinuousAt f y
⊢ ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ContinuousAt f y

Tactic:
filter_upwards [this, self_mem_nhdsWithin] with y hy h'y

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
n : ℕ
h : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x
this : ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ContinuousAt.{u_1, u_3} (Y := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
y : 𝕜
hy : ContinuousAt.{u_1, u_3} (Y := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
h'y : Membership.mem (γ := Set 𝕜) {x}ᶜ y
⊢ ¬y = x

Tactic:
simp only [Set.mem_compl_iff, Set.mem_singleton_iff] at h'y

Premises used: Set.mem_singleton_iff, Set.mem_compl_iff
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
n : ℕ
h : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x
this : ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ContinuousAt.{u_1, u_3} (Y := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
y : 𝕜
hy : ContinuousAt.{u_1, u_3} (Y := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
h'y : ¬y = x
⊢ ContinuousAt (Y := 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ n) y

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
n : ℕ
h : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x
this : ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ContinuousAt.{u_1, u_3} (Y := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
y : 𝕜
hy : ContinuousAt.{u_1, u_3} (Y := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
h'y : ¬y = x
⊢ (y - x) ^ n ≠ 0

Tactic:
simp [sub_eq_zero, h'y]

Premises used: sub_eq_zero
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
n : ℕ
h : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x
this : ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ContinuousAt.{u_1, u_3} (Y := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
y : 𝕜
hy : ContinuousAt.{u_1, u_3} (Y := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
h'y : ¬y = x
⊢ ContinuousAt (Y := 𝕜) (fun (z : 𝕜) ↦ ((z - x) ^ n)⁻¹) y

Tactic:
have : ContinuousAt (fun z ↦ ((z - x) ^ n)⁻¹) y :=
    ContinuousAt.inv₀ (by fun_prop) (by simp [sub_eq_zero, h'y])
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
n : ℕ
h : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x
this_1 : ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ContinuousAt.{u_1, u_3} (Y := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
y : 𝕜
hy : ContinuousAt.{u_1, u_3} (Y := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
h'y : ¬y = x
this : ContinuousAt (Y := 𝕜) (fun (z : 𝕜) ↦ ((z - x) ^ n)⁻¹) y
h₁ : (fun (x_1 : 𝕜) ↦ ((x_1 - x) ^ n)⁻¹ • (x_1 - x) ^ n • f x_1) =ᶠ[𝓝 y] f
⊢ ContinuousAt f y

Tactic:
apply (this.smul hy).congr

Premises used: ContinuousAt.congr, ContinuousAt.smul
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
n : ℕ
h : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x
this_1 : ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ContinuousAt.{u_1, u_3} (Y := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
y : 𝕜
hy : ContinuousAt.{u_1, u_3} (Y := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
h'y : ¬y = x
this : ContinuousAt (Y := 𝕜) (fun (z : 𝕜) ↦ ((z - x) ^ n)⁻¹) y
h₁ : ∀ (z : 𝕜) (hz : z ≠ x), ((z - x) ^ n)⁻¹ • (z - x) ^ n • f z = f z
⊢ (fun (x_1 : 𝕜) ↦ ((x_1 - x) ^ n)⁻¹ • (x_1 - x) ^ n • f x_1) =ᶠ[𝓝 y] f

Tactic:
filter_upwards [eventually_ne_nhds h'y] with z hz

Premises used: eventually_ne_nhds
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
n : ℕ
h : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x
this_1 : ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ContinuousAt.{u_1, u_3} (Y := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
y : 𝕜
hy : ContinuousAt.{u_1, u_3} (Y := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
h'y : ¬y = x
this : ContinuousAt (Y := 𝕜) (fun (z : 𝕜) ↦ ((z - x) ^ n)⁻¹) y
z : 𝕜
hz : z ≠ x
⊢ ((z - x) ^ n)⁻¹ • (z - x) ^ n • f z = f z

Tactic:
simp [smul_smul, hz, sub_eq_zero]

Premises used: sub_eq_zero, smul_smul
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
inst_3 : CompleteSpace E
f : 𝕜 → E
h : MeromorphicAt f x
obtain :
  ∀ (n : ℕ) (h : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x),
    ∀ᶠ (y : 𝕜) in 𝓝[≠] x, AnalyticAt 𝕜 f y
⊢ ∀ᶠ (y : 𝕜) in 𝓝[≠] x, AnalyticAt 𝕜 f y

Tactic:
obtain ⟨n, h⟩ := h
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
inst_3 : CompleteSpace E
f : 𝕜 → E
n : ℕ
h : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x
⊢ ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y

Tactic:
apply AnalyticAt.eventually_analyticAt at h

Premises used: AnalyticAt.eventually_analyticAt
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
inst_3 : CompleteSpace E
f : 𝕜 → E
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
⊢ ∀ᶠ (y : 𝕜) in 𝓝[≠] x, AnalyticAt 𝕜 f y

Tactic:
(h.filter_mono ?_).mp ?_

Premises used: Filter.Eventually.filter_mono, Filter.Eventually.mp
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
inst_3 : CompleteSpace E
f : 𝕜 → E
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
refine_1 : 𝓝[≠] x ≤ 𝓝 x
refine_2 :
  ∀ᶠ (x_1 : 𝕜) in 𝓝[≠] x,
    AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x_1 → AnalyticAt 𝕜 f x_1
⊢ ∀ᶠ (y : 𝕜) in 𝓝[≠] x, AnalyticAt 𝕜 f y

Tactic:
refine (h.filter_mono ?_).mp ?_

Premises used: Filter.Eventually.filter_mono, Filter.Eventually.mp
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
inst_3 : CompleteSpace E
f : 𝕜 → E
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
⊢ 𝓝[≠] x ≤ 𝓝 x

Tactic:
simp [nhdsWithin]

Premises used: nhdsWithin
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
inst_3 : CompleteSpace E
f : 𝕜 → E
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
refine_2 :
  ∀ᶠ (x_1 : 𝕜) in 𝓝 x,
    Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 →
      AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x_1 → AnalyticAt 𝕜 f x_1
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝[≠] x,
    AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x_1 → AnalyticAt 𝕜 f x_1

Tactic:
rw [eventually_nhdsWithin_iff]

Premises used: eventually_nhdsWithin_iff
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
inst_3 : CompleteSpace E
f : 𝕜 → E
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
refine_2 :
  ∀ (x_1 : 𝕜),
    Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 →
      AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x_1 → AnalyticAt 𝕜 f x_1
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝 x,
    Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 →
      AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x_1 → AnalyticAt 𝕜 f x_1

Tactic:
apply Filter.Eventually.of_forall

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
inst_3 : CompleteSpace E
f : 𝕜 → E
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
y : 𝕜
hy : Membership.mem (γ := Set 𝕜) {x}ᶜ y
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
⊢ ¬y = x

Tactic:
rw [Set.mem_compl_iff, Set.mem_singleton_iff] at hy

Premises used: Set.mem_singleton_iff, Set.mem_compl_iff
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
inst_3 : CompleteSpace E
f : 𝕜 → E
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
y : 𝕜
hy : Membership.mem (γ := Set 𝕜) {x}ᶜ y
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
hy₁ : ¬y = x
⊢ AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y

Tactic:
rw [Set.mem_compl_iff, Set.mem_singleton_iff] at hy

Premises used: Set.mem_singleton_iff, Set.mem_compl_iff
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
inst_3 : CompleteSpace E
f : 𝕜 → E
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
y : 𝕜
hy : ¬y = x
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
⊢ AnalyticAt 𝕜 ((HSub.hSub (α := 𝕜 → 𝕜) _root_.id fun (x_1 : 𝕜) ↦ x) ^ n)⁻¹ y

Tactic:
have := ((analyticAt_id (𝕜 := 𝕜).sub analyticAt_const).pow n).inv
      (pow_ne_zero _ (sub_ne_zero_of_ne hy))
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
inst_3 : CompleteSpace E
f : 𝕜 → E
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
y : 𝕜
hy : ¬y = x
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
this : AnalyticAt 𝕜 ((HSub.hSub (α := 𝕜 → 𝕜) _root_.id fun (x_1 : 𝕜) ↦ x) ^ n)⁻¹ y
refine_2 :
  ∀ (x_1 : 𝕜),
    x_1 ≠ x →
      HSMul.hSMul (β := 𝕜 → E) ((HSub.hSub (α := 𝕜 → 𝕜) _root_.id fun (x_2 : 𝕜) ↦ x) ^ n)⁻¹
          (fun (z : 𝕜) ↦ (z - x) ^ n • f z) x_1 =
        f x_1
⊢ AnalyticAt 𝕜 f y

Tactic:
apply (this.smul hf).congr ∘ (eventually_ne_nhds hy).mono

Premises used: AnalyticAt.smul, eventually_ne_nhds, Filter.Eventually.mono, AnalyticAt.congr
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
inst_3 : CompleteSpace E
f : 𝕜 → E
n : ℕ
h : ∀ᶠ (y : 𝕜) in 𝓝 x, AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
y : 𝕜
hy : ¬y = x
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ n • f z) y
this : AnalyticAt 𝕜 ((HSub.hSub (α := 𝕜 → 𝕜) _root_.id fun (x_1 : 𝕜) ↦ x) ^ n)⁻¹ y
z : 𝕜
hz : z ≠ x
⊢ HSMul.hSMul (β := 𝕜 → E) ((HSub.hSub (α := 𝕜 → 𝕜) _root_.id fun (x_1 : 𝕜) ↦ x) ^ n)⁻¹
      (fun (z : 𝕜) ↦ (z - x) ^ n • f z) z =
    f z

Tactic:
simp [smul_smul, hz, sub_eq_zero]

Premises used: sub_eq_zero, smul_smul
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
⊢ MeromorphicAt f x ↔ ∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z

Tactic:
⟨fun ⟨n, hn⟩ ↦ ⟨-n, _, ⟨hn, eventually_nhdsWithin_iff.mpr ?_⟩⟩, ?_⟩

Premises used: Iff.mpr, Compl.compl, nhdsWithin, Filter.Eventually, HSub.hSub, Exists, Nat.cast, _private.0.MeromorphicAt.iff_eventuallyEq_zpow_smul_analyticAt.match_1, And, HPow.hPow, AnalyticAt, eventually_nhdsWithin_iff, And.intro, Iff.intro, Exists.intro, HSMul.hSMul, Singleton.singleton, Eq, Neg.neg