awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
n : ℕ
⊢ HPow.hPow (α := 𝕜 → 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) n =
    HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x_1 : 𝕜) ↦ x_1 - x) (↑n : ℤ)

Tactic:
simp only [zpow_natCast]

Premises used: zpow_natCast
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
rw : meromorphicOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) x = (↑1 : WithTop ℤ)
rw₁ :
  meromorphicOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) x =
    meromorphicOrderAt (HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x_1 : 𝕜) ↦ x_1 - x) 1) x
rw₂ : 𝕜
rw₃ : meromorphicOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) x = meromorphicOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) x
rw₄ : 𝕜
rw₅ : meromorphicOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) x = meromorphicOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) x
rw₆ : 𝕜
⊢ meromorphicOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) x = 1

Tactic:
rw [← WithTop.coe_one, ← meromorphicOrderAt_zpow_id_sub_const (𝕜 := 𝕜), zpow_one]

Premises used: zpow_one, WithTop.coe_one, meromorphicOrderAt_zpow_id_sub_const
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
pos : ∀ (h₁ : ¬MeromorphicAt f x), meromorphicOrderAt f x = meromorphicOrderAt (-f) x
neg : ∀ (h₁ : ¬¬MeromorphicAt f x), meromorphicOrderAt f x = meromorphicOrderAt (-f) x
⊢ meromorphicOrderAt f x = meromorphicOrderAt (-f) x

Tactic:
by_cases h₁ : ¬MeromorphicAt f x

Premises used: MeromorphicAt
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h₁ : ¬MeromorphicAt f x
⊢ meromorphicOrderAt f x = meromorphicOrderAt (-f) x

Tactic:
aesop
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h₁ : ¬¬MeromorphicAt f x
⊢ MeromorphicAt f x

Tactic:
rw [not_not] at h₁

Premises used: Classical.not_not
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h₁ : MeromorphicAt f x
pos : ∀ (h₂ : meromorphicOrderAt f x = ⊤), meromorphicOrderAt f x = meromorphicOrderAt (-f) x
neg : ∀ (h₂ : ¬meromorphicOrderAt f x = ⊤), meromorphicOrderAt f x = meromorphicOrderAt (-f) x
⊢ meromorphicOrderAt f x = meromorphicOrderAt (-f) x

Tactic:
by_cases h₂ : meromorphicOrderAt f x = ⊤

Premises used: meromorphicOrderAt
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h₁ : MeromorphicAt f x
h₂ : meromorphicOrderAt f x = ⊤
pos : meromorphicOrderAt (-f) x = ⊤
⊢ meromorphicOrderAt f x = meromorphicOrderAt (-f) x

Tactic:
rw [h₂, eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h₁ : MeromorphicAt f x
h₂ : meromorphicOrderAt f x = ⊤
⊢ meromorphicOrderAt (-f) x = ⊤

Tactic:
simp_all [meromorphicOrderAt_eq_top_iff]

Premises used: meromorphicOrderAt_eq_top_iff
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h₁ : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
⊢ meromorphicOrderAt f x ≠ ⊤

Tactic:
h₂
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h₁ : MeromorphicAt f x
h₂ : ¬meromorphicOrderAt f x = ⊤
neg : ∀ (n : ℤ) (hn : (↑n : WithTop ℤ) = meromorphicOrderAt f x), (↑n : WithTop ℤ) = meromorphicOrderAt (-f) x
⊢ meromorphicOrderAt f x = meromorphicOrderAt (-f) x

Tactic:
lift meromorphicOrderAt f x to ℤ using h₂ with n hn

Premises used: meromorphicOrderAt
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h₁ : MeromorphicAt f x
n : ℤ
hn : meromorphicOrderAt f x = (↑n : WithTop ℤ)
⊢ MeromorphicAt (-f) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h₁ : MeromorphicAt f x
n : ℤ
hn : meromorphicOrderAt f x = (↑n : WithTop ℤ)
⊢ MeromorphicAt f x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h₁ : MeromorphicAt f x
n : ℤ
hn : (↑n : WithTop ℤ) = meromorphicOrderAt f x
neg :
  ∀ (hn : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z),
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (-f) z = (z - x) ^ n • g z
⊢ (↑n : WithTop ℤ) = meromorphicOrderAt (-f) x

Tactic:
rw [eq_comm, meromorphicOrderAt_eq_int_iff (by fun_prop)] at *

Premises used: meromorphicOrderAt_eq_int_iff, eq_comm
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h₁ : MeromorphicAt f x
n : ℤ
hn : ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
neg :
  ∀ (g : 𝕜 → E) (hg : AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z),
    ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (-f) z = (z - x) ^ n • g z
⊢ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (-f) z = (z - x) ^ n • g z

Tactic:
obtain ⟨g, hg⟩ := hn
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h₁ : MeromorphicAt f x
n : ℤ
g : 𝕜 → E
hg : AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
h : AnalyticAt 𝕜 (-g) x ∧ (-g) x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (-f) z = (z - x) ^ n • (-g) z
⊢ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (-f) z = (z - x) ^ n • g z

Tactic:
use -g
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
h₁ : MeromorphicAt f x
n : ℤ
g : 𝕜 → E
hg : AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ n • g z
⊢ AnalyticAt 𝕜 (-g) x ∧ (-g) x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (-f) z = (z - x) ^ n • (-g) z

Tactic:
simp_all
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → E
⊢ meromorphicOrderAt f x = meromorphicOrderAt.{u_1, u_2} (E := E) (fun (z : 𝕜) ↦ -f z) x

Tactic:
meromorphicOrderAt_neg

Premises used: meromorphicOrderAt_neg
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → 𝕜
g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
h₂f : meromorphicOrderAt f x = ⊤
top : ∀ (h₂f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0), ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f • g) z = 0
⊢ meromorphicOrderAt (f • g) x = ⊤ + meromorphicOrderAt g x

Tactic:
simp only [top_add, meromorphicOrderAt_eq_top_iff] at h₂f ⊢

Premises used: meromorphicOrderAt_eq_top_iff, top_add
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → 𝕜
g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
h₂f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
z : 𝕜
hz : f z = 0
⊢ (f • g) z = 0

Tactic:
simp [hz]
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → 𝕜
g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
h₂f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0
h :
  ∀ (a : 𝕜),
    Membership.mem (γ := Set 𝕜)
      {x : 𝕜 |
        Membership.mem (γ := Set 𝕜) {x : 𝕜 | (fun (z : 𝕜) ↦ f z = 0) x} x →
          Membership.mem (γ := Set 𝕜) {x : 𝕜 | (fun (z : 𝕜) ↦ (f • g) z = 0) x} x}
      a
h₁ h₂ : ∀ (z : 𝕜) (hz : f z = 0), (f • g) z = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f • g) z = 0

Tactic:
filter_upwards [h₂f] with z hz using by simp [hz]
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → 𝕜
g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
m : ℤ
h₂f : meromorphicOrderAt f x = (↑m : WithTop ℤ)
h₂g : meromorphicOrderAt g x = ⊤
coe : ∀ (h₂g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, g z = 0), ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f • g) z = 0
⊢ meromorphicOrderAt (f • g) x = (↑m : WithTop ℤ) + ⊤

Tactic:
simp only [add_top, meromorphicOrderAt_eq_top_iff] at h₂g ⊢

Premises used: add_top, meromorphicOrderAt_eq_top_iff
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → 𝕜
g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
m : ℤ
h₂f : meromorphicOrderAt f x = (↑m : WithTop ℤ)
h₂g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, g z = 0
z : 𝕜
hz : g z = 0
⊢ (f • g) z = 0

Tactic:
simp [hz]
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → 𝕜
g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
m : ℤ
h₂f : meromorphicOrderAt f x = (↑m : WithTop ℤ)
h₂g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, g z = 0
h :
  ∀ (a : 𝕜),
    Membership.mem (γ := Set 𝕜)
      {x : 𝕜 |
        Membership.mem (γ := Set 𝕜) {x : 𝕜 | (fun (z : 𝕜) ↦ g z = 0) x} x →
          Membership.mem (γ := Set 𝕜) {x : 𝕜 | (fun (z : 𝕜) ↦ (f • g) z = 0) x} x}
      a
h₁ h₂ : ∀ (z : 𝕜) (hz : g z = 0), (f • g) z = 0
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f • g) z = 0

Tactic:
filter_upwards [h₂g] with z hz using by simp [hz]
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → 𝕜
g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
m : ℤ
h₂f : meromorphicOrderAt f x = (↑m : WithTop ℤ)
n : ℤ
h₂g : meromorphicOrderAt g x = (↑n : WithTop ℤ)
coe : ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 x ∧ g_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f • g) z = (z - x) ^ (m + n) • g_1 z
⊢ meromorphicOrderAt (f • g) x = (↑m : WithTop ℤ) + (↑n : WithTop ℤ)

Tactic:
rw [← WithTop.coe_add, meromorphicOrderAt_eq_int_iff (hf.smul hg)]

Premises used: meromorphicOrderAt_eq_int_iff, WithTop.coe_add, MeromorphicAt.smul
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → 𝕜
g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
m : ℤ
h₂f : meromorphicOrderAt f x = (↑m : WithTop ℤ)
n : ℤ
h₂g : meromorphicOrderAt g x = (↑n : WithTop ℤ)
coe :
  ∀ (F : 𝕜 → 𝕜) (h₁F : AnalyticAt 𝕜 F x) (h₂F : F x ≠ 0) (h₃F : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ m • F z),
    ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 x ∧ g_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f • g) z = (z - x) ^ (m + n) • g_1 z
⊢ ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 x ∧ g_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f • g) z = (z - x) ^ (m + n) • g_1 z

Tactic:
obtain ⟨F, h₁F, h₂F, h₃F⟩ := (meromorphicOrderAt_eq_int_iff hf).1 h₂f

Premises used: meromorphicOrderAt_eq_int_iff, Iff.mp
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → 𝕜
g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
m : ℤ
h₂f : meromorphicOrderAt f x = (↑m : WithTop ℤ)
n : ℤ
h₂g : meromorphicOrderAt g x = (↑n : WithTop ℤ)
F : 𝕜 → 𝕜
h₁F : AnalyticAt 𝕜 F x
h₂F : F x ≠ 0
h₃F : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ m • F z
coe :
  ∀ (G : 𝕜 → E) (h₁G : AnalyticAt 𝕜 G x) (h₂G : G x ≠ 0) (h₃G : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, g z = (z - x) ^ n • G z),
    ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 x ∧ g_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f • g) z = (z - x) ^ (m + n) • g_1 z
⊢ ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 x ∧ g_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f • g) z = (z - x) ^ (m + n) • g_1 z

Tactic:
obtain ⟨G, h₁G, h₂G, h₃G⟩ := (meromorphicOrderAt_eq_int_iff hg).1 h₂g

Premises used: meromorphicOrderAt_eq_int_iff, Iff.mp
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → 𝕜
g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
m : ℤ
h₂f : meromorphicOrderAt f x = (↑m : WithTop ℤ)
n : ℤ
h₂g : meromorphicOrderAt g x = (↑n : WithTop ℤ)
F : 𝕜 → 𝕜
h₁F : AnalyticAt 𝕜 F x
h₂F : F x ≠ 0
h₃F : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ m • F z
G : 𝕜 → E
h₁G : AnalyticAt 𝕜 G x
h₂G : G x ≠ 0
h₃G : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, g z = (z - x) ^ n • G z
⊢ (F • G) x ≠ 0

Tactic:
simp [h₂F, h₂G]
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → 𝕜
g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
m : ℤ
h₂f : meromorphicOrderAt f x = (↑m : WithTop ℤ)
n : ℤ
h₂g : meromorphicOrderAt g x = (↑n : WithTop ℤ)
F : 𝕜 → 𝕜
h₁F : AnalyticAt 𝕜 F x
h₂F : F x ≠ 0
h₃F : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ m • F z
G : 𝕜 → E
h₁G : AnalyticAt 𝕜 G x
h₂G : G x ≠ 0
h₃G : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, g z = (z - x) ^ n • G z
right : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f • g) z = (z - x) ^ (m + n) • (F • G) z
⊢ ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 x ∧ g_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f • g) z = (z - x) ^ (m + n) • g_1 z

Tactic:
use F • G, h₁F.smul h₁G, by simp [h₂F, h₂G]

Premises used: AnalyticAt.smul
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → 𝕜
g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
m : ℤ
h₂f : meromorphicOrderAt f x = (↑m : WithTop ℤ)
n : ℤ
h₂g : meromorphicOrderAt g x = (↑n : WithTop ℤ)
F : 𝕜 → 𝕜
h₁F : AnalyticAt 𝕜 F x
h₂F : F x ≠ 0
h₃F : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ m • F z
G : 𝕜 → E
h₁G : AnalyticAt 𝕜 G x
h₂G : G x ≠ 0
h₃G : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, g z = (z - x) ^ n • G z
h :
  ∀ (a : 𝕜) (ha : Membership.mem (γ := Set 𝕜) {x}ᶜ a) (hfa : f a = (a - x) ^ m • F a) (hga : g a = (a - x) ^ n • G a),
    (f • g) a = (a - x) ^ (m + n) • (F • G) a
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f • g) z = (z - x) ^ (m + n) • (F • G) z

Tactic:
filter_upwards [self_mem_nhdsWithin, h₃F, h₃G] with a ha hfa hga

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → 𝕜
g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
m : ℤ
h₂f : meromorphicOrderAt f x = (↑m : WithTop ℤ)
n : ℤ
h₂g : meromorphicOrderAt g x = (↑n : WithTop ℤ)
F : 𝕜 → 𝕜
h₁F : AnalyticAt 𝕜 F x
h₂F : F x ≠ 0
h₃F : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ m • F z
G : 𝕜 → E
h₁G : AnalyticAt 𝕜 G x
h₂G : G x ≠ 0
h₃G : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, g z = (z - x) ^ n • G z
a : 𝕜
ha : Membership.mem (γ := Set 𝕜) {x}ᶜ a
hfa : f a = (a - x) ^ m • F a
hga : g a = (a - x) ^ n • G a
⊢ (f • g) a = (a - x) ^ (m + n) • (F • G) a

Tactic:
simp [hfa, hga, smul_comm (F a), zpow_add₀ (sub_ne_zero.mpr ha), mul_smul]

Premises used: Iff.mpr, sub_ne_zero, zpow_add₀, SMulCommClass.smul_comm, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → 𝕜
g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
m : ℤ
h₂f : meromorphicOrderAt f x = (↑m : WithTop ℤ)
coe : ∀ (x_1 : WithTop ℤ) (h₂g : meromorphicOrderAt g x = x_1), meromorphicOrderAt (f • g) x = (↑m : WithTop ℤ) + x_1
⊢ meromorphicOrderAt (f • g) x = (↑m : WithTop ℤ) + meromorphicOrderAt g x

Tactic:
cases h₂g : meromorphicOrderAt g x with
    | top =>
      simp only [add_top, meromorphicOrderAt_eq_top_iff] at h₂g ⊢
      filter_upwards [h₂g] with z hz using by simp [hz]
    | coe n => -- Non-trivial case: both functions do not vanish around z₀
      rw [← WithTop.coe_add, meromorphicOrderAt_eq_int_iff (hf.smul hg)]
      obtain ⟨F, h₁F, h₂F, h₃F⟩ := (meromorphicOrderAt_eq_int_iff hf).1 h₂f
      obtain ⟨G, h₁G, h₂G, h₃G⟩ := (meromorphicOrderAt_eq_int_iff hg).1 h₂g
      use F • G, h₁F.smul h₁G, by simp [h₂F, h₂G]
      filter_upwards [self_mem_nhdsWithin, h₃F, h₃G] with a ha hfa hga
      simp [hfa, hga, smul_comm (F a), zpow_add₀ (sub_ne_zero.mpr ha), mul_smul]

Premises used: add_top, meromorphicOrderAt_eq_top_iff, meromorphicOrderAt, meromorphicOrderAt_eq_int_iff, self_mem_nhdsWithin, Iff.mp, WithTop.coe_add, MeromorphicAt.smul, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : 𝕜
f : 𝕜 → 𝕜
g : 𝕜 → E
hf : MeromorphicAt f x
hg : MeromorphicAt g x
cases :
  ∀ (x_1 : WithTop ℤ) (h₂f : meromorphicOrderAt f x = x_1), meromorphicOrderAt (f • g) x = x_1 + meromorphicOrderAt g x
⊢ meromorphicOrderAt (f • g) x = meromorphicOrderAt f x + meromorphicOrderAt g x

Tactic:
cases h₂f : meromorphicOrderAt f x with
  | top =>
    simp only [top_add, meromorphicOrderAt_eq_top_iff] at h₂f ⊢
    filter_upwards [h₂f] with z hz using by simp [hz]
  | coe m =>
    cases h₂g : meromorphicOrderAt g x with
    | top =>
      simp only [add_top, meromorphicOrderAt_eq_top_iff] at h₂g ⊢
      filter_upwards [h₂g] with z hz using by simp [hz]
    | coe n => -- Non-trivial case: both functions do not vanish around z₀
      rw [← WithTop.coe_add, meromorphicOrderAt_eq_int_iff (hf.smul hg)]
      obtain ⟨F, h₁F, h₂F, h₃F⟩ := (meromorphicOrderAt_eq_int_iff hf).1 h₂f
      obtain ⟨G, h₁G, h₂G, h₃G⟩ := (meromorphicOrderAt_eq_int_iff hg).1 h₂g
      use F • G, h₁F.smul h₁G, by simp [h₂F, h₂G]
      filter_upwards [self_mem_nhdsWithin, h₃F, h₃G] with a ha hfa hga
      simp [hfa, hga, smul_comm (F a), zpow_add₀ (sub_ne_zero.mpr ha), mul_smul]

Premises used: add_top, meromorphicOrderAt_eq_top_iff, meromorphicOrderAt, meromorphicOrderAt_eq_int_iff, self_mem_nhdsWithin, top_add, WithTop.coe_add, MeromorphicAt.smul, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
f g : 𝕜 → 𝕜
hf : MeromorphicAt f x
hg : MeromorphicAt g x
⊢ meromorphicOrderAt (f * g) x = meromorphicOrderAt f x + meromorphicOrderAt g x

Tactic:
meromorphicOrderAt_smul hf hg

Premises used: meromorphicOrderAt_smul
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → MeromorphicAt (f i) x
empty : ∃ (g : 𝕜 → 𝕜), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, 1 z = HPow.hPow (β := ℤ) (z - x) 0 • g z
empty₁ : MeromorphicAt (E := 𝕜) 1 x
⊢ meromorphicOrderAt (E := 𝕜) (∏ i ∈ ∅, f i) x = ∑ i ∈ ∅, meromorphicOrderAt (f i) x

Tactic:
rw [Finset.prod_empty, Finset.sum_empty, ← WithTop.coe_zero, meromorphicOrderAt_eq_int_iff]

Premises used: Finset.prod_empty, meromorphicOrderAt_eq_int_iff, WithTop.coe_zero, Finset.sum_empty
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → MeromorphicAt (f i) x
⊢ Ne.{u_1 + 1} (α := 𝕜) (1 x) 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, 1 z = HSMul.hSMul (β := 𝕜) (HPow.hPow (β := ℤ) (z - x) 0) (1 z)

Tactic:
simp
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → MeromorphicAt (f i) x
⊢ ∃ (g : 𝕜 → 𝕜), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, 1 z = HPow.hPow (β := ℤ) (z - x) 0 • g z

Tactic:
exact ⟨1, analyticAt_const, by simp⟩
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → MeromorphicAt (f i) x
⊢ MeromorphicAt (E := 𝕜) 1 x

Tactic:
apply MeromorphicAt.const

Premises used: MeromorphicAt.const
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
a : ι
s : Finset ι
ha : a ∉ s
hs :
  ∀ (hf : ∀ i ∈ s, MeromorphicAt (f i) x),
    meromorphicOrderAt (E := 𝕜) (∏ i ∈ s, f i) x = ∑ i ∈ s, meromorphicOrderAt (f i) x
hf : ∀ i ∈ Insert.insert a s, MeromorphicAt (f i) x
insert :
  meromorphicOrderAt (f a) x + meromorphicOrderAt (E := 𝕜) (∏ i ∈ s, f i) x =
    meromorphicOrderAt (f a) x + ∑ x_1 ∈ s, meromorphicOrderAt (f x_1) x
⊢ meromorphicOrderAt (E := 𝕜) (∏ i ∈ Insert.insert a s, f i) x = ∑ i ∈ Insert.insert a s, meromorphicOrderAt (f i) x

Tactic:
rw [Finset.sum_insert ha, Finset.prod_insert ha, meromorphicOrderAt_mul
      (hf a (Finset.mem_insert_self a s))
      (MeromorphicAt.prod (fun i hi ↦ hf i (Finset.mem_insert_of_mem hi)))]

Premises used: Finset.prod_insert, meromorphicOrderAt_mul, Finset.mem_insert_self, MeromorphicAt.prod, Finset.mem_insert_of_mem, Finset.sum_insert
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
a : ι
s : Finset ι
ha : a ∉ s
hs :
  ∀ (hf : ∀ i ∈ s, MeromorphicAt (f i) x),
    meromorphicOrderAt (E := 𝕜) (∏ i ∈ s, f i) x = ∑ i ∈ s, meromorphicOrderAt (f i) x
hf : ∀ i ∈ Insert.insert a s, MeromorphicAt (f i) x
insert : meromorphicOrderAt (E := 𝕜) (∏ i ∈ s, f i) x = ∑ x_1 ∈ s, meromorphicOrderAt (f x_1) x
⊢ meromorphicOrderAt (f a) x + meromorphicOrderAt (E := 𝕜) (∏ i ∈ s, f i) x =
    meromorphicOrderAt (f a) x + ∑ x_1 ∈ s, meromorphicOrderAt (f x_1) x

Tactic:
congr
-- Module: Mathlib.Analysis.Meromorphic.Order
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
a : ι
s : Finset ι
ha : a ∉ s
hs :
  ∀ (hf : ∀ i ∈ s, MeromorphicAt (f i) x),
    meromorphicOrderAt (E := 𝕜) (∏ i ∈ s, f i) x = ∑ i ∈ s, meromorphicOrderAt (f i) x
hf : ∀ i ∈ Insert.insert a s, MeromorphicAt (f i) x
insert insert₁ : Eq (α := WithTop ℤ) (∑ i ∈ s, meromorphicOrderAt (f i) x) (∑ x_1 ∈ s, meromorphicOrderAt (f x_1) x)
⊢ meromorphicOrderAt (E := 𝕜) (∏ i ∈ s, f i) x = ∑ x_1 ∈ s, meromorphicOrderAt (f x_1) x

Tactic:
rw [hs (fun i hi ↦ hf i (Finset.mem_insert_of_mem hi))]

Premises used: Finset.mem_insert_of_mem