awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x ∨ MeromorphicAt f x ∧ meromorphicOrderAt f x < 0 ∧ f x = 0
h₂f : 0 ≤ meromorphicOrderAt f x
mp : ∀ (h : AnalyticAt 𝕜 f x), AnalyticAt 𝕜 f x
mp₁ : MeromorphicAt f x → ∀ (h₃f : meromorphicOrderAt f x < 0), f x = 0 → AnalyticAt 𝕜 f x
⊢ AnalyticAt 𝕜 f x

Tactic:
rcases hf with h | ⟨_, h₃f, _⟩
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h₂f : 0 ≤ meromorphicOrderAt f x
h : AnalyticAt 𝕜 f x
⊢ AnalyticAt 𝕜 f x

Tactic:
h
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h₂f : 0 ≤ meromorphicOrderAt f x
h : AnalyticAt 𝕜 f x
⊢ AnalyticAt 𝕜 f x

Tactic:
exact h
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h₂f : 0 ≤ meromorphicOrderAt f x
left : MeromorphicAt f x
h₃f : meromorphicOrderAt f x < 0
right : f x = 0
mp : ∀ (h' : ¬AnalyticAt 𝕜 f x), False
⊢ AnalyticAt 𝕜 f x

Tactic:
by_contra h'
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h₂f : 0 ≤ meromorphicOrderAt f x
left : MeromorphicAt f x
h₃f : meromorphicOrderAt f x < 0
right : f x = 0
h' : ¬AnalyticAt 𝕜 f x
⊢ False

Tactic:
lt_irrefl 0 (lt_of_le_of_lt h₂f h₃f)

Premises used: lt_of_le_of_lt, lt_irrefl, OfNat.ofNat
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h₂f : 0 ≤ meromorphicOrderAt f x
left : MeromorphicAt f x
h₃f : meromorphicOrderAt f x < 0
right : f x = 0
h' : ¬AnalyticAt 𝕜 f x
⊢ False

Tactic:
exact lt_irrefl 0 (lt_of_le_of_lt h₂f h₃f)

Premises used: lt_of_le_of_lt, lt_irrefl, OfNat.ofNat
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicNFAt f x
h₂f : AnalyticAt 𝕜 f x
mpr : LE.le (α := WithTop ℤ) 0 (ENat.map Nat.cast (analyticOrderAt f x))
⊢ 0 ≤ meromorphicOrderAt f x

Tactic:
rw [h₂f.meromorphicOrderAt_eq]

Premises used: AnalyticAt.meromorphicOrderAt_eq
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicNFAt f x
h₂f : AnalyticAt 𝕜 f x
⊢ LE.le (α := WithTop ℤ) 0 (ENat.map Nat.cast (analyticOrderAt f x))

Tactic:
simp
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
⊢ MeromorphicNFAt f x

Tactic:
simp [meromorphicNFAt_iff_analyticAt_or, hf]

Premises used: meromorphicNFAt_iff_analyticAt_or
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
h : ∀ (a : 𝕜) (ha : AnalyticAt 𝕜 f a), MeromorphicNFAt f a
⊢ {x : 𝕜 | MeromorphicNFAt f x} ∈ Filter.codiscreteWithin U

Tactic:
filter_upwards [hf.analyticAt_mem_codiscreteWithin] with _ ha

Premises used: MeromorphicOn.analyticAt_mem_codiscreteWithin
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
a : 𝕜
ha : AnalyticAt 𝕜 f a
⊢ MeromorphicNFAt f a

Tactic:
ha.meromorphicNFAt

Premises used: AnalyticAt.meromorphicNFAt
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : MeromorphicOn f U
a : 𝕜
ha : AnalyticAt 𝕜 f a
⊢ MeromorphicNFAt f a

Tactic:
exact ha.meromorphicNFAt

Premises used: AnalyticAt.meromorphicNFAt
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicNFAt f x
mp : meromorphicOrderAt f x = 0 → f x ≠ 0
mpr : f x ≠ 0 → meromorphicOrderAt f x = 0
⊢ meromorphicOrderAt f x = 0 ↔ f x ≠ 0

Tactic:
constructor
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicNFAt f x
h₁f : meromorphicOrderAt f x = 0
⊢ AnalyticAt 𝕜 f x

Tactic:
have h₂f := hf.meromorphicOrderAt_nonneg_iff_analyticAt.1 (le_of_eq h₁f.symm)
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicNFAt f x
h₁f : meromorphicOrderAt f x = 0
h₂f : AnalyticAt 𝕜 f x
mp : Eq (α := WithTop ℤ) (ENat.map Nat.cast (analyticOrderAt f x)) 0
⊢ f x ≠ 0

Tactic:
rw [← h₂f.analyticOrderAt_eq_zero, ← ENat.map_natCast_eq_zero (α := ℤ)]

Premises used: ENat.map_natCast_eq_zero, AnalyticAt.analyticOrderAt_eq_zero
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicNFAt f x
h₁f : meromorphicOrderAt f x = 0
h₂f : AnalyticAt 𝕜 f x
mp mp₁ mp₂ mp₃ :
  ∀ (h₁f : Eq (α := WithTop ℤ) (ENat.map Nat.cast (analyticOrderAt f x)) 0) (h₂f : AnalyticAt 𝕜 f x),
    Eq (α := WithTop ℤ) (ENat.map Nat.cast (analyticOrderAt f x)) 0
⊢ Eq (α := WithTop ℤ) (ENat.map Nat.cast (analyticOrderAt f x)) 0

Tactic:
rwa [h₂f.meromorphicOrderAt_eq] at h₁f

Premises used: AnalyticAt.meromorphicOrderAt_eq
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicNFAt f x
h : f x ≠ 0
mpr : ∀ (h₁ : f =ᶠ[𝓝 x] 0), meromorphicOrderAt f x = 0
mpr₁ :
  ∀ (n : ℤ) (g : 𝕜 → E) (h₁g : AnalyticAt 𝕜 g x) (h₂g : g x ≠ 0)
    (h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g), meromorphicOrderAt f x = 0
⊢ meromorphicOrderAt f x = 0

Tactic:
rcases id hf with h₁ | ⟨n, g, h₁g, h₂g, h₃g⟩

Premises used: id
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicNFAt f x
h : f x ≠ 0
h₁ : f =ᶠ[𝓝 x] 0
⊢ f x = 0 x

Tactic:
have := h₁.eq_of_nhds
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicNFAt f x
h : f x ≠ 0
h₁ : f =ᶠ[𝓝 x] 0
this : f x = 0 x
⊢ meromorphicOrderAt f x = 0

Tactic:
tauto
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicNFAt f x
h : f x ≠ 0
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
by_contra : ∀ (hContra : ¬n = 0), False
⊢ n = 0

Tactic:
by_contra hContra
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicNFAt f x
h : f x ≠ 0
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
hContra : ¬n = 0
⊢ f x = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) x

Tactic:
have := h₃g.eq_of_nhds
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicNFAt f x
h : f x ≠ 0
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
hContra : ¬n = 0
this : f x = (HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g) x
⊢ f x = 0

Tactic:
simp only [Pi.smul_apply', Pi.pow_apply, sub_self, zero_zpow n hContra, zero_smul] at this

Premises used: zero_zpow, sub_self, Pi.smul_apply', zero_smul, Pi.pow_apply
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicNFAt f x
h : f x ≠ 0
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
hContra : ¬n = 0
this : f x = 0
⊢ False

Tactic:
tauto
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicNFAt f x
h : f x ≠ 0
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
⊢ n = 0

Tactic:
have : n = 0 := by
        by_contra hContra
        have := h₃g.eq_of_nhds
        simp only [Pi.smul_apply', Pi.pow_apply, sub_self, zero_zpow n hContra, zero_smul] at this
        tauto
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicNFAt f x
h : f x ≠ 0
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
h₃g : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • g
this : n = 0
⊢ f =ᶠ[𝓝 x] HSMul.hSMul (α := 𝕜 → 𝕜) 1 g

Tactic:
simp only [this, zpow_zero] at h₃g

Premises used: zpow_zero
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicNFAt f x
h : f x ≠ 0
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
this : n = 0
h₃g : f =ᶠ[𝓝 x] HSMul.hSMul (α := 𝕜 → 𝕜) 1 g
mpr : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • g z
⊢ meromorphicOrderAt f x = 0

Tactic:
apply (meromorphicOrderAt_eq_int_iff hf.meromorphicAt).2

Premises used: Iff.mpr, meromorphicOrderAt_eq_int_iff, MeromorphicNFAt.meromorphicAt
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicNFAt f x
h : f x ≠ 0
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
this : n = 0
h₃g : f =ᶠ[𝓝 x] HSMul.hSMul (α := 𝕜 → 𝕜) 1 g
right : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • g z
⊢ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • g z

Tactic:
use g, h₁g, h₂g
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicNFAt f x
h : f x ≠ 0
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
this : n = 0
h₃g : f =ᶠ[𝓝 x] HSMul.hSMul (α := 𝕜 → 𝕜) 1 g
right : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 (g z)
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HPow.hPow (β := ℤ) (z - x) 0 • g z

Tactic:
simp only [zpow_zero]

Premises used: zpow_zero
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicNFAt f x
h : f x ≠ 0
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
this : n = 0
h₃g : f =ᶠ[𝓝 x] HSMul.hSMul (α := 𝕜 → 𝕜) 1 g
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 (g z)

Tactic:
h₃g.filter_mono nhdsWithin_le_nhds

Premises used: Filter.EventuallyEq.filter_mono, Filter.EventuallyEq, nhdsWithin_le_nhds
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : MeromorphicNFAt f x
h : f x ≠ 0
n : ℤ
g : 𝕜 → E
h₁g : AnalyticAt 𝕜 g x
h₂g : g x ≠ 0
this : n = 0
h₃g : f =ᶠ[𝓝 x] HSMul.hSMul (α := 𝕜 → 𝕜) 1 g
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 (g z)

Tactic:
exact h₃g.filter_mono nhdsWithin_le_nhds

Premises used: Filter.EventuallyEq.filter_mono, nhdsWithin_le_nhds
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
mp : f =ᶠ[𝓝[≠] x] g → f =ᶠ[𝓝 x] g
mpr : f =ᶠ[𝓝 x] g → f =ᶠ[𝓝[≠] x] g
⊢ f =ᶠ[𝓝[≠] x] g ↔ f =ᶠ[𝓝 x] g

Tactic:
constructor
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
h : f =ᶠ[𝓝[≠] x] g
⊢ meromorphicOrderAt f x = meromorphicOrderAt g x

Tactic:
have t₀ := meromorphicOrderAt_congr h
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
h : f =ᶠ[𝓝[≠] x] g
t₀ : meromorphicOrderAt f x = meromorphicOrderAt g x
pos : ∀ (cs : meromorphicOrderAt f x = 0), f =ᶠ[𝓝 x] g
neg : ∀ (cs : ¬meromorphicOrderAt f x = 0), f =ᶠ[𝓝 x] g
⊢ f =ᶠ[𝓝 x] g

Tactic:
by_cases cs : meromorphicOrderAt f x = 0

Premises used: meromorphicOrderAt
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
h : f =ᶠ[𝓝[≠] x] g
t₀ : meromorphicOrderAt f x = meromorphicOrderAt g x
cs : meromorphicOrderAt f x = 0
⊢ 0 = meromorphicOrderAt g x

Tactic:
rw [cs] at t₀
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
h : f =ᶠ[𝓝[≠] x] g
t₀ : meromorphicOrderAt f x = meromorphicOrderAt g x
cs : meromorphicOrderAt f x = 0
t₁ : 0 = meromorphicOrderAt g x
⊢ meromorphicOrderAt f x = 0

Tactic:
rw [cs] at t₀
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
h : f =ᶠ[𝓝[≠] x] g
t₀ : 0 = meromorphicOrderAt g x
cs : meromorphicOrderAt f x = 0
⊢ ContinuousAt f x

Tactic:
have Z := (hf.meromorphicOrderAt_nonneg_iff_analyticAt.1 (le_of_eq cs.symm)).continuousAt
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
h : f =ᶠ[𝓝[≠] x] g
t₀ : 0 = meromorphicOrderAt g x
cs : meromorphicOrderAt f x = 0
Z : ContinuousAt f x
⊢ ContinuousAt g x

Tactic:
have W := (hg.meromorphicOrderAt_nonneg_iff_analyticAt.1 (le_of_eq t₀)).continuousAt
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
h : f =ᶠ[𝓝[≠] x] g
t₀ : 0 = meromorphicOrderAt g x
cs : meromorphicOrderAt f x = 0
Z : ContinuousAt f x
W : ContinuousAt g x
⊢ f =ᶠ[𝓝 x] g

Tactic:
(Z.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE W).1 h

Premises used: Iff.mp, ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
h : f =ᶠ[𝓝[≠] x] g
t₀ : 0 = meromorphicOrderAt g x
cs : meromorphicOrderAt f x = 0
Z : ContinuousAt f x
W : ContinuousAt g x
⊢ f =ᶠ[𝓝 x] g

Tactic:
exact (Z.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE W).1 h

Premises used: Iff.mp, ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
h : f =ᶠ[𝓝[≠] x] g
t₀ : meromorphicOrderAt f x = meromorphicOrderAt g x
cs : ¬meromorphicOrderAt f x = 0
neg : f x = g x
⊢ f =ᶠ[𝓝 x] g

Tactic:
apply eventuallyEq_nhds_of_eventuallyEq_nhdsNE h

Premises used: eventuallyEq_nhds_of_eventuallyEq_nhdsNE
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
h : f =ᶠ[𝓝[≠] x] g
t₀ : meromorphicOrderAt f x = meromorphicOrderAt g x
cs : ¬meromorphicOrderAt f x = 0
h₁f : ¬meromorphicOrderAt f x = 0 := cs
⊢ ¬f x ≠ 0

Tactic:
rw [hf.meromorphicOrderAt_eq_zero_iff] at h₁f

Premises used: MeromorphicNFAt.meromorphicOrderAt_eq_zero_iff
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
h : f =ᶠ[𝓝[≠] x] g
t₀ : meromorphicOrderAt f x = meromorphicOrderAt g x
cs : ¬meromorphicOrderAt f x = 0
h₁f : ¬f x ≠ 0
h₁g : ¬meromorphicOrderAt f x = 0 := cs
⊢ ¬g x ≠ 0

Tactic:
rw [t₀, hg.meromorphicOrderAt_eq_zero_iff] at h₁g

Premises used: MeromorphicNFAt.meromorphicOrderAt_eq_zero_iff
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
h : f =ᶠ[𝓝[≠] x] g
t₀ : meromorphicOrderAt f x = meromorphicOrderAt g x
cs : ¬meromorphicOrderAt f x = 0
h₁f : ¬f x ≠ 0
h₁g : ¬g x ≠ 0
⊢ f x = 0

Tactic:
simp only [not_not] at *

Premises used: Classical.not_not
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
h : f =ᶠ[𝓝[≠] x] g
t₀ : meromorphicOrderAt f x = meromorphicOrderAt g x
cs : ¬meromorphicOrderAt f x = 0
h₁f : ¬f x ≠ 0
h₁g : ¬g x ≠ 0
h₁f₁ : f x = 0
⊢ g x = 0

Tactic:
simp only [not_not] at *

Premises used: Classical.not_not
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
h : f =ᶠ[𝓝[≠] x] g
t₀ : meromorphicOrderAt f x = meromorphicOrderAt g x
cs : ¬meromorphicOrderAt f x = 0
h₁f : f x = 0
h₁g : g x = 0
neg : 0 = g x
neg₁ neg₂ : Eq.{u_2 + 1} (α := E) 0 0
⊢ f x = g x

Tactic:
rw [h₁f, h₁g]
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
⊢ f =ᶠ[𝓝 x] g → f =ᶠ[𝓝[≠] x] g

Tactic:
(Filter.EventuallyEq.filter_mono · nhdsWithin_le_nhds)

Premises used: Filter.EventuallyEq.filter_mono, nhdsWithin_le_nhds
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hf : MeromorphicNFAt f x
hg : MeromorphicNFAt g x
⊢ f =ᶠ[𝓝 x] g → f =ᶠ[𝓝[≠] x] g

Tactic:
exact (Filter.EventuallyEq.filter_mono · nhdsWithin_le_nhds)

Premises used: Filter.EventuallyEq.filter_mono, nhdsWithin_le_nhds
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hfg : f =ᶠ[𝓝 x] g
mp : MeromorphicNFAt f x → MeromorphicNFAt g x
mpr : MeromorphicNFAt g x → MeromorphicNFAt f x
⊢ MeromorphicNFAt f x ↔ MeromorphicNFAt g x

Tactic:
constructor
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hfg : f =ᶠ[𝓝 x] g
h : f =ᶠ[𝓝 x] 0
⊢ MeromorphicNFAt g x

Tactic:
.inl (hfg.symm.trans h)

Premises used: Filter.EventuallyEq.trans, Or.inl, MeromorphicNFAt, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hfg : f =ᶠ[𝓝 x] g
h : f =ᶠ[𝓝 x] 0
⊢ MeromorphicNFAt g x

Tactic:
exact .inl (hfg.symm.trans h)
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hfg : f =ᶠ[𝓝 x] g
n : ℤ
h : 𝕜 → E
h₁h : AnalyticAt 𝕜 h x
h₂h : h x ≠ 0
h₃h : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • h
⊢ MeromorphicNFAt g x

Tactic:
.inr ⟨n, h, h₁h, h₂h, hfg.symm.trans h₃h⟩

Premises used: Filter.EventuallyEq.trans, And.intro, Exists.intro, MeromorphicNFAt, Filter.EventuallyEq.symm, Or.inr
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hfg : f =ᶠ[𝓝 x] g
n : ℤ
h : 𝕜 → E
h₁h : AnalyticAt 𝕜 h x
h₂h : h x ≠ 0
h₃h : f =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • h
⊢ MeromorphicNFAt g x

Tactic:
exact .inr ⟨n, h, h₁h, h₂h, hfg.symm.trans h₃h⟩
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hfg : f =ᶠ[𝓝 x] g
h : g =ᶠ[𝓝 x] 0
⊢ MeromorphicNFAt f x

Tactic:
.inl (hfg.trans h)

Premises used: Filter.EventuallyEq.trans, Or.inl, MeromorphicNFAt
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hfg : f =ᶠ[𝓝 x] g
h : g =ᶠ[𝓝 x] 0
⊢ MeromorphicNFAt f x

Tactic:
exact .inl (hfg.trans h)
-- Module: Mathlib.Analysis.Meromorphic.NormalForm
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
g : 𝕜 → E
hfg : f =ᶠ[𝓝 x] g
n : ℤ
h : 𝕜 → E
h₁h : AnalyticAt 𝕜 h x
h₂h : h x ≠ 0
h₃h : g =ᶠ[𝓝 x] HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n • h
⊢ MeromorphicNFAt f x

Tactic:
.inr ⟨n, h, h₁h, h₂h, hfg.trans h₃h⟩

Premises used: Filter.EventuallyEq.trans, And.intro, Exists.intro, MeromorphicNFAt, Or.inr