awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hf : MeromorphicAt f x
⊢ MeromorphicAt (HSMul.hSMul (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ -1) f) x

Tactic:
(MeromorphicAt.const (-1 : 𝕜) x).smul hf

Premises used: MeromorphicAt.const, OfNat.ofNat, MeromorphicAt.smul, Neg.neg
-- 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
hf : MeromorphicAt f x
h : -f = HSMul.hSMul (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ -1) f
⊢ MeromorphicAt (-f) x

Tactic:
convert! (MeromorphicAt.const (-1 : 𝕜) x).smul hf using 1

Premises used: MeromorphicAt.const, OfNat.ofNat, MeromorphicAt.smul, Neg.neg
-- 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
hf : MeromorphicAt f x
h : ∀ (z : 𝕜), (-f) z = HSMul.hSMul (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ -1) f z
⊢ -f = HSMul.hSMul (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ -1) f

Tactic:
ext1 z
-- 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
hf : MeromorphicAt f x
z : 𝕜
⊢ (-f) z = HSMul.hSMul (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ -1) f z

Tactic:
simp only [Pi.neg_apply, Pi.smul_apply', neg_smul, one_smul]

Premises used: neg_smul, Pi.smul_apply', one_smul, Pi.neg_apply
-- 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
⊢ MeromorphicAt f x

Tactic:
simpa only [neg_neg] using h.neg

Premises used: neg_neg, MeromorphicAt.neg
-- 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 g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
⊢ MeromorphicAt (f + -g) x

Tactic:
hf.add hg.neg

Premises used: MeromorphicAt.add, MeromorphicAt.neg
-- 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 g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
h : f - g = f + -g
⊢ MeromorphicAt (f - g) x

Tactic:
convert! hf.add hg.neg using 1

Premises used: MeromorphicAt.add, MeromorphicAt.neg
-- 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 g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
h : ∀ (z : 𝕜), (f - g) z = (f + -g) z
⊢ f - g = f + -g

Tactic:
ext1 z
-- 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 g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
z : 𝕜
h : f z - g z = (f + -g) z
h₁ : f z - g z = f z + (-g) z
h₂ : f z - g z = f z + -g z
⊢ (f - g) z = (f + -g) z

Tactic:
simp_rw [Pi.sub_apply, Pi.add_apply, Pi.neg_apply, sub_eq_add_neg]

Premises used: sub_eq_add_neg, Pi.add_apply, Pi.neg_apply, Pi.sub_apply
-- 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 g : 𝕜 → E
hf : MeromorphicAt f x
h : MeromorphicAt (f + g) x
⊢ MeromorphicAt g x

Tactic:
simpa using h.sub hf

Premises used: MeromorphicAt.sub
-- 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 g : 𝕜 → E
hf : MeromorphicAt f x
h : MeromorphicAt g x
⊢ MeromorphicAt (f + g) x

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 g : 𝕜 → E
hf : MeromorphicAt f x
⊢ MeromorphicAt (f + g) x ↔ MeromorphicAt g x

Tactic:
exact ⟨fun h ↦ by simpa using h.sub hf, fun _ ↦ by 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 g : 𝕜 → E
hf : MeromorphicAt f x
⊢ MeromorphicAt.{u_1, u_3} (E := E) (fun (z : 𝕜) ↦ f z + g z) x ↔ MeromorphicAt g x

Tactic:
meromorphicAt_add_iff_meromorphicAt₁ hf

Premises used: MeromorphicAt.meromorphicAt_add_iff_meromorphicAt₁
-- 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 g : 𝕜 → E
hg : MeromorphicAt g x
rw : MeromorphicAt (g + f) x ↔ MeromorphicAt f x
⊢ MeromorphicAt (f + g) x ↔ MeromorphicAt f x

Tactic:
rw [add_comm]

Premises used: add_comm
-- 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 g : 𝕜 → E
hg : MeromorphicAt g x
⊢ MeromorphicAt (g + f) x ↔ MeromorphicAt f x

Tactic:
meromorphicAt_add_iff_meromorphicAt₁ hg

Premises used: MeromorphicAt.meromorphicAt_add_iff_meromorphicAt₁
-- 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 g : 𝕜 → E
hg : MeromorphicAt g x
⊢ MeromorphicAt (g + f) x ↔ MeromorphicAt f x

Tactic:
exact meromorphicAt_add_iff_meromorphicAt₁ hg

Premises used: MeromorphicAt.meromorphicAt_add_iff_meromorphicAt₁
-- 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 g : 𝕜 → E
hg : MeromorphicAt g x
⊢ MeromorphicAt.{u_1, u_3} (E := E) (fun (z : 𝕜) ↦ f z + g z) x ↔ MeromorphicAt f x

Tactic:
meromorphicAt_add_iff_meromorphicAt₂ hg

Premises used: MeromorphicAt.meromorphicAt_add_iff_meromorphicAt₂
-- 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 g : 𝕜 → E
hf : MeromorphicAt f x
h : MeromorphicAt (f - g) x
⊢ MeromorphicAt g x

Tactic:
simpa using h.sub hf

Premises used: MeromorphicAt.sub
-- 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 g : 𝕜 → E
hf : MeromorphicAt f x
h : MeromorphicAt g x
⊢ MeromorphicAt (f - g) x

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 g : 𝕜 → E
hf : MeromorphicAt f x
⊢ MeromorphicAt (f - g) x ↔ MeromorphicAt g x

Tactic:
exact ⟨fun h ↦ by simpa using h.sub hf, fun _ ↦ by 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 g : 𝕜 → E
hf : MeromorphicAt f x
⊢ MeromorphicAt.{u_1, u_3} (E := E) (fun (z : 𝕜) ↦ f z - g z) x ↔ MeromorphicAt g x

Tactic:
meromorphicAt_sub_iff_meromorphicAt₁ hf

Premises used: MeromorphicAt.meromorphicAt_sub_iff_meromorphicAt₁
-- 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 g : 𝕜 → E
hg : MeromorphicAt g x
h : MeromorphicAt (f - g) x
⊢ MeromorphicAt f x

Tactic:
simpa using h.add hg

Premises used: MeromorphicAt.add
-- 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 g : 𝕜 → E
hg : MeromorphicAt g x
h : MeromorphicAt f x
⊢ MeromorphicAt (f - g) x

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 g : 𝕜 → E
hg : MeromorphicAt g x
⊢ MeromorphicAt (f - g) x ↔ MeromorphicAt f x

Tactic:
exact ⟨fun h ↦ by simpa using h.add hg, fun _ ↦ by 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 g : 𝕜 → E
hg : MeromorphicAt g x
⊢ MeromorphicAt.{u_1, u_3} (E := E) (fun (z : 𝕜) ↦ f z - g z) x ↔ MeromorphicAt f x

Tactic:
meromorphicAt_sub_iff_meromorphicAt₂ hg

Premises used: MeromorphicAt.meromorphicAt_sub_iff_meromorphicAt₂
-- 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 g : 𝕜 → E
hf : MeromorphicAt f x
hfg : f =ᶠ[𝓝[≠] x] g
rcases : ∀ (m : ℕ) (hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x), MeromorphicAt g x
⊢ MeromorphicAt g x

Tactic:
rcases hf with ⟨m, hf⟩
-- 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 g : 𝕜 → E
hfg : f =ᶠ[𝓝[≠] x] g
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
⊢ MeromorphicAt g x

Tactic:
⟨m + 1, ?_⟩

Premises used: HAdd.hAdd, Exists.intro, OfNat.ofNat, MeromorphicAt
-- 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 g : 𝕜 → E
hfg : f =ᶠ[𝓝[≠] x] g
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
refine : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ (m + 1) • g z) x
⊢ MeromorphicAt g x

Tactic:
refine ⟨m + 1, ?_⟩
-- 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 g : 𝕜 → E
hfg : f =ᶠ[𝓝[≠] x] g
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
⊢ AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ z - x) x

Tactic:
have : AnalyticAt 𝕜 (fun z ↦ z - x) x := analyticAt_id.sub analyticAt_const
-- 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 g : 𝕜 → E
hfg : f =ᶠ[𝓝[≠] x] g
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
this : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ z - x) x
⊢ AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ (m + 1) • g z) x

Tactic:
(this.fun_smul hf).congr ?_

Premises used: AnalyticAt.fun_smul, 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 : 𝕜
f g : 𝕜 → E
hfg : f =ᶠ[𝓝[≠] x] g
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
this : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ z - x) x
refine :
  EventuallyEq.{u_1, u_3} (β := E) (𝓝 x) (fun (i : 𝕜) ↦ (i - x) • (i - x) ^ m • f i) fun (z : 𝕜) ↦
    (z - x) ^ (m + 1) • g z
⊢ AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ (m + 1) • g z) x

Tactic:
refine (this.fun_smul hf).congr ?_

Premises used: AnalyticAt.fun_smul, 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 : 𝕜
f g : 𝕜 → E
hfg : f =ᶠ[𝓝[≠] x] g
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
this : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ z - x) x
rw :
  ∀ (hfg : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 → f x_1 = g x_1) (m : ℕ)
    (hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x)
    (this : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ z - x) x),
    EventuallyEq.{u_1, u_3} (β := E) (𝓝 x) (fun (i : 𝕜) ↦ (i - x) • (i - x) ^ m • f i) fun (z : 𝕜) ↦
      (z - x) ^ (m + 1) • g z
⊢ EventuallyEq.{u_1, u_3} (β := E) (𝓝 x) (fun (i : 𝕜) ↦ (i - x) • (i - x) ^ m • f i) fun (z : 𝕜) ↦
    (z - x) ^ (m + 1) • g z

Tactic:
rw [eventuallyEq_nhdsWithin_iff] at hfg

Premises used: eventuallyEq_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 : 𝕜
f g : 𝕜 → E
hfg : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 → f x_1 = g x_1
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
this : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ z - x) x
h :
  ∀ (z : 𝕜) (hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z → f z = g z), (z - x) • (z - x) ^ m • f z = (z - x) ^ (m + 1) • g z
⊢ EventuallyEq.{u_1, u_3} (β := E) (𝓝 x) (fun (i : 𝕜) ↦ (i - x) • (i - x) ^ m • f i) fun (z : 𝕜) ↦
    (z - x) ^ (m + 1) • g z

Tactic:
filter_upwards [hfg] with z hz
-- 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 g : 𝕜 → E
hfg : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 → f x_1 = g x_1
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
this : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ z - x) x
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z → f z = g z
h :
  ∀ (hfg : ∀ᶠ (x : 𝕜) in 𝓝 z, Membership.mem (γ := Set 𝕜) {z}ᶜ x → f x = g x)
    (hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z_1 : 𝕜) ↦ (z_1 - z) ^ m • f z_1) z)
    (this : AnalyticAt 𝕜 (F := 𝕜) (fun (z_1 : 𝕜) ↦ z_1 - z) z) (hz : Membership.mem (γ := Set 𝕜) {z}ᶜ z → f z = g z),
    (z - z) • (z - z) ^ m • f z = (z - z) ^ (m + 1) • g z
h₁ : ∀ (hn : z ≠ x), (z - x) • (z - x) ^ m • f z = (z - x) ^ (m + 1) • g z
⊢ (z - x) • (z - x) ^ m • f z = (z - x) ^ (m + 1) • g z

Tactic:
rcases eq_or_ne z x with rfl | hn

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : 𝕜 → E
m : ℕ
z : 𝕜
hfg : ∀ᶠ (x : 𝕜) in 𝓝 z, Membership.mem (γ := Set 𝕜) {z}ᶜ x → f x = g x
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z_1 : 𝕜) ↦ (z_1 - z) ^ m • f z_1) z
this : AnalyticAt 𝕜 (F := 𝕜) (fun (z_1 : 𝕜) ↦ z_1 - z) z
hz : Membership.mem (γ := Set 𝕜) {z}ᶜ z → f z = g z
⊢ (z - z) • (z - z) ^ m • f z = (z - z) ^ (m + 1) • g z

Tactic:
simp
-- 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 g : 𝕜 → E
hfg : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 → f x_1 = g x_1
m : ℕ
hf : AnalyticAt.{u_1, u_1, u_3} 𝕜 (F := E) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x
this : AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ z - x) x
z : 𝕜
hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z → f z = g z
hn : z ≠ x
h : (z - x) • (z - x) ^ m • g z = (z - x) ^ (m + 1) • g z
h₁ : (z - x) • (z - x) ^ m • g z = ((z - x) * (z - x) ^ m) • g z
h₂ h₃ : (z - x) • (z - x) ^ m • g z = (z - x) • (z - x) ^ m • g z
⊢ (z - x) • (z - x) ^ m • f z = (z - x) ^ (m + 1) • g z

Tactic:
rw [hz (Set.mem_compl_singleton_iff.mp hn), pow_succ', mul_smul]

Premises used: Set.mem_compl_singleton_iff, Iff.mp, SemigroupAction.mul_smul, pow_succ'
-- 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 g : 𝕜 → E
h : f =ᶠ[𝓝[≠] x] g
⊢ MeromorphicAt f x ↔ MeromorphicAt g x

Tactic:
⟨fun hf ↦ hf.congr h, fun hg ↦ hg.congr h.symm⟩

Premises used: Iff.intro, MeromorphicAt.congr, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : DecidableEq 𝕜
f : 𝕜 → E
z w : 𝕜
e : E
⊢ MeromorphicAt (Function.update (β := fun (a : 𝕜) ↦ E) f w e) z ↔ MeromorphicAt f z

Tactic:
meromorphicAt_congr (Function.update_eventuallyEq_nhdsNE f w z e)

Premises used: Function.update_eventuallyEq_nhdsNE, MeromorphicAt.meromorphicAt_congr
-- Module: Mathlib.Analysis.Meromorphic.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : DecidableEq 𝕜
f : 𝕜 → E
z : 𝕜
hf : MeromorphicAt f z
w : 𝕜
e : E
⊢ MeromorphicAt (Function.update (β := fun (a : 𝕜) ↦ E) f w e) z

Tactic:
update_iff.mpr hf

Premises used: Iff.mpr, MeromorphicAt.update_iff
-- 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
rcases :
  ∀ (m : ℕ) (hf : AnalyticAt.{u_1, u_1, u_2} 𝕜 (F := 𝕜') (fun (z : 𝕜) ↦ (z - x) ^ m • f z) x), MeromorphicAt f⁻¹ x
⊢ MeromorphicAt f⁻¹ x

Tactic:
rcases hf with ⟨m, hf⟩
-- 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
pos : ∀ (h_eq : EventuallyEq.{u_1, u_2} (β := 𝕜') (𝓝 x) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) 0), MeromorphicAt f⁻¹ x
neg : ∀ (h_eq : ¬EventuallyEq.{u_1, u_2} (β := 𝕜') (𝓝 x) (fun (z : 𝕜) ↦ (z - x) ^ m • f z) 0), MeromorphicAt f⁻¹ x
⊢ MeromorphicAt f⁻¹ x

Tactic:
by_cases h_eq : (fun z ↦ (z - x) ^ m • f z) =ᶠ[𝓝 x] 0

Premises used: HSub.hSub, nhds, HPow.hPow, HSMul.hSMul
-- 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
⊢ MeromorphicAt f⁻¹ x

Tactic:
(MeromorphicAt.const 0 x).congr ?_

Premises used: MeromorphicAt.const, OfNat.ofNat, MeromorphicAt.congr
-- 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
pos : (fun (x : 𝕜) ↦ 0) =ᶠ[𝓝[≠] x] f⁻¹
⊢ MeromorphicAt f⁻¹ x

Tactic:
refine (MeromorphicAt.const 0 x).congr ?_

Premises used: MeromorphicAt.const, OfNat.ofNat, MeromorphicAt.congr
-- 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
pos : ∀ᶠ (x_1 : 𝕜) in 𝓝 x, Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 → 0 = f⁻¹ x_1
⊢ (fun (x : 𝕜) ↦ 0) =ᶠ[𝓝[≠] x] f⁻¹

Tactic:
rw [eventuallyEq_nhdsWithin_iff]

Premises used: eventuallyEq_nhdsWithin_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
h : ∀ (z : 𝕜) (hfz : (z - x) ^ m • f z = 0 z) (hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z), 0 = f⁻¹ z
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝 x, Membership.mem (γ := Set 𝕜) {x}ᶜ x_1 → 0 = f⁻¹ x_1

Tactic:
filter_upwards [h_eq] with z hfz hz
-- 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
z : 𝕜
hfz : (z - x) ^ m • f z = 0 z
hz : Membership.mem (γ := Set 𝕜) {x}ᶜ z
h : 0 = (f z)⁻¹
h₁ : Eq.{u_2 + 1} (α := 𝕜') 0 0⁻¹
h₂ h₃ : Eq.{u_2 + 1} (α := 𝕜') 0 0
⊢ 0 = f⁻¹ z

Tactic:
rw [Pi.inv_apply, (smul_eq_zero_iff_right <| pow_ne_zero _ (sub_ne_zero.mpr hz)).mp hfz,
      inv_zero]

Premises used: Iff.mpr, inv_zero, sub_ne_zero, pow_ne_zero, smul_eq_zero_iff_right, Iff.mp, Pi.inv_apply
-- 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
neg :
  ∀ (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), MeromorphicAt f⁻¹ x
⊢ MeromorphicAt f⁻¹ x

Tactic:
obtain ⟨n, g, hg_an, hg_ne, hg_eq⟩ := hf.exists_eventuallyEq_pow_smul_nonzero_iff.mpr h_eq

Premises used: Iff.mpr, AnalyticAt.exists_eventuallyEq_pow_smul_nonzero_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
⊢ AnalyticAt 𝕜 (F := 𝕜) (fun (z : 𝕜) ↦ (z - x) ^ (m + 1)) x

Tactic:
have : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ (m + 1)) x :=
      (analyticAt_id.sub analyticAt_const).pow _
-- 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
⊢ MeromorphicAt f⁻¹ x

Tactic:
⟨n + 1, (this.fun_smul <| hg_an.inv hg_ne).congr ?_⟩

Premises used: AnalyticAt.fun_smul, HAdd.hAdd, Exists.intro, AnalyticAt.congr, OfNat.ofNat, AnalyticAt.inv, MeromorphicAt
-- 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
neg :
  EventuallyEq.{u_1, u_2} (β := 𝕜') (𝓝 x) (fun (i : 𝕜) ↦ (i - x) ^ (m + 1) • g⁻¹ i) fun (z : 𝕜) ↦
    (z - x) ^ (n + 1) • f⁻¹ z
⊢ MeromorphicAt f⁻¹ x

Tactic:
refine ⟨n + 1, (this.fun_smul <| hg_an.inv hg_ne).congr ?_⟩