awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
⊢ meromorphicOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) x = 1
have rw : meromorphicOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) x = (↑1 : WithTop ℤ)
Tactic: rw [← WithTop.coe_one, ← meromorphicOrderAt_zpow_id_sub_const (𝕜 := 𝕜), zpow_one]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
rw : meromorphicOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) x = (↑1 : WithTop ℤ)
⊢ meromorphicOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) x = 1
have rw₁ : meromorphicOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) x =
  meromorphicOrderAt (HPow.hPow (α := 𝕜 → 𝕜) (β := ℤ) (fun (x_1 : 𝕜) ↦ x_1 - x) 1) x
Tactic: rw [← WithTop.coe_one, ← meromorphicOrderAt_zpow_id_sub_const (𝕜 := 𝕜), zpow_one]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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₂ : 𝕜
⊢ meromorphicOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) x = 1
have rw₃ : meromorphicOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) x = meromorphicOrderAt (E := 𝕜) (fun (x_1 : 𝕜) ↦ x_1 - x) x
Tactic: rw [← WithTop.coe_one, ← meromorphicOrderAt_zpow_id_sub_const (𝕜 := 𝕜), zpow_one]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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 (-f) x
have pos : ∀ (h₁ : ¬MeromorphicAt f x), meromorphicOrderAt f x = meromorphicOrderAt (-f) x
Tactic: by_cases h₁ : ¬MeromorphicAt f x
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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
⊢ meromorphicOrderAt f x = meromorphicOrderAt (-f) x
have neg : ∀ (h₁ : ¬¬MeromorphicAt f x), meromorphicOrderAt f x = meromorphicOrderAt (-f) x
Tactic: by_cases h₁ : ¬MeromorphicAt f x
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (hypothesis)
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
have h₂ : MeromorphicAt f x
Tactic: rw [not_not] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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
have pos : ∀ (h₂ : meromorphicOrderAt f x = ⊤), meromorphicOrderAt f x = meromorphicOrderAt (-f) x
Tactic: by_cases h₂ : meromorphicOrderAt f x = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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
⊢ meromorphicOrderAt f x = meromorphicOrderAt (-f) x
have neg : ∀ (h₂ : ¬meromorphicOrderAt f x = ⊤), meromorphicOrderAt f x = meromorphicOrderAt (-f) x
Tactic: by_cases h₂ : meromorphicOrderAt f x = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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 = meromorphicOrderAt (-f) x
have pos : meromorphicOrderAt (-f) x = ⊤
Tactic: rw [h₂, eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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 = meromorphicOrderAt (-f) x
have neg : ∀ (n : ℤ) (hn : (↑n : WithTop ℤ) = meromorphicOrderAt f x), (↑n : WithTop ℤ) = meromorphicOrderAt (-f) x
Tactic: lift meromorphicOrderAt f x to ℤ using h₂ with n hn
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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
⊢ (↑n : WithTop ℤ) = meromorphicOrderAt (-f) x
have 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
Tactic: rw [eq_comm, meromorphicOrderAt_eq_int_iff (by fun_prop)] at *
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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
⊢ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (-f) z = (z - x) ^ n • g z
have 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
Tactic: obtain ⟨g, hg⟩ := hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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
⊢ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (-f) z = (z - x) ^ n • g z
have h : AnalyticAt 𝕜 (-g) x ∧ (-g) x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (-f) z = (z - x) ^ n • (-g) z
Tactic: use -g
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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 = ⊤
⊢ meromorphicOrderAt (f • g) x = ⊤ + meromorphicOrderAt g x
have top : ∀ (h₂f : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = 0), ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f • g) z = 0
Tactic: simp only [top_add, meromorphicOrderAt_eq_top_iff] at h₂f ⊢
Cleared hypotheses: h₂f
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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 : 𝕜) in 𝓝[≠] x, (f • g) z = 0
have 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
Tactic: filter_upwards [h₂f] with z hz using by simp [hz]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f • g) z = 0
have h₁ : ∀ (a : 𝕜), f a = 0 → (f • g) a = 0
Tactic: filter_upwards [h₂f] with z hz using by simp [hz]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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 = ⊤
⊢ meromorphicOrderAt (f • g) x = (↑m : WithTop ℤ) + ⊤
have coe : ∀ (h₂g : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, g z = 0), ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f • g) z = 0
Tactic: simp only [add_top, meromorphicOrderAt_eq_top_iff] at h₂g ⊢
Cleared hypotheses: h₂g
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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 : 𝕜) in 𝓝[≠] x, (f • g) z = 0
have 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
Tactic: filter_upwards [h₂g] with z hz using by simp [hz]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f • g) z = 0
have h₁ : ∀ (a : 𝕜), g a = 0 → (f • g) a = 0
Tactic: filter_upwards [h₂g] with z hz using by simp [hz]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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 ℤ)
⊢ meromorphicOrderAt (f • g) x = (↑m : WithTop ℤ) + (↑n : WithTop ℤ)
have 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
Tactic: rw [← WithTop.coe_add, meromorphicOrderAt_eq_int_iff (hf.smul hg)]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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 ℤ)
⊢ ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 x ∧ g_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f • g) z = (z - x) ^ (m + n) • g_1 z
have 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
Tactic: obtain ⟨F, h₁F, h₂F, h₃F⟩ := (meromorphicOrderAt_eq_int_iff hf).1 h₂f
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 x ∧ g_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f • g) z = (z - x) ^ (m + n) • g_1 z
have 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
Tactic: obtain ⟨G, h₁G, h₂G, h₃G⟩ := (meromorphicOrderAt_eq_int_iff hg).1 h₂g
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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
⊢ ∃ (g_1 : 𝕜 → E), AnalyticAt 𝕜 g_1 x ∧ g_1 x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f • g) z = (z - x) ^ (m + n) • g_1 z
have right : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f • g) z = (z - x) ^ (m + n) • (F • G) z
Tactic: use F • G, h₁F.smul h₁G, by simp [h₂F, h₂G]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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
⊢ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, (f • g) z = (z - x) ^ (m + n) • (F • G) z
have 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
Tactic: filter_upwards [self_mem_nhdsWithin, h₃F, h₃G] with a ha hfa hga
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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 ℤ)
⊢ meromorphicOrderAt (f • g) x = (↑m : WithTop ℤ) + meromorphicOrderAt g x
have coe : ∀ (x_1 : WithTop ℤ) (h₂g : meromorphicOrderAt g x = x_1), meromorphicOrderAt (f • g) x = (↑m : WithTop ℤ) + x_1
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]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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
⊢ meromorphicOrderAt (f • g) x = meromorphicOrderAt f x + meromorphicOrderAt g x
have cases : ∀ (x_1 : WithTop ℤ) (h₂f : meromorphicOrderAt f x = x_1), meromorphicOrderAt (f • g) x = x_1 + 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]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → MeromorphicAt (f i) x
⊢ meromorphicOrderAt (E := 𝕜) (∏ i ∈ ∅, f i) x = ∑ i ∈ ∅, meromorphicOrderAt (f i) x
have empty : ∃ (g : 𝕜 → 𝕜), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] x, 1 z = HPow.hPow (β := ℤ) (z - x) 0 • g z
Tactic: rw [Finset.prod_empty, Finset.sum_empty, ← WithTop.coe_zero, meromorphicOrderAt_eq_int_iff]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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
⊢ meromorphicOrderAt (E := 𝕜) (∏ i ∈ ∅, f i) x = ∑ i ∈ ∅, meromorphicOrderAt (f i) x
have empty₁ : MeromorphicAt (E := 𝕜) 1 x
Tactic: rw [Finset.prod_empty, Finset.sum_empty, ← WithTop.coe_zero, meromorphicOrderAt_eq_int_iff]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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 a s, MeromorphicAt (f i) x
⊢ meromorphicOrderAt (E := 𝕜) (∏ i ∈ insert a s, f i) x = ∑ i ∈ insert a s, meromorphicOrderAt (f i) x
have insert : meromorphicOrderAt (f a) x + meromorphicOrderAt (E := 𝕜) (∏ i ∈ s, f i) x =
  meromorphicOrderAt (f a) x + ∑ x_1 ∈ s, meromorphicOrderAt (f x_1) 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)))]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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 a s, MeromorphicAt (f i) x
⊢ meromorphicOrderAt (f a) x + meromorphicOrderAt (E := 𝕜) (∏ i ∈ s, f i) x =
    meromorphicOrderAt (f a) x + ∑ x_1 ∈ s, meromorphicOrderAt (f x_1) x
have insert : meromorphicOrderAt (E := 𝕜) (∏ i ∈ s, f i) x = ∑ x_1 ∈ s, meromorphicOrderAt (f x_1) x
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
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 a s, MeromorphicAt (f i) x
⊢ meromorphicOrderAt (E := 𝕜) (∏ i ∈ s, f i) x = ∑ x_1 ∈ s, meromorphicOrderAt (f x_1) x
have insert : Eq (α := WithTop ℤ) (∑ i ∈ s, meromorphicOrderAt (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))]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
hf : ∀ i ∈ s, MeromorphicAt (f i) x
⊢ meromorphicOrderAt (E := 𝕜) (∏ i ∈ s, f i) x = ∑ i ∈ s, meromorphicOrderAt (f i) x
have empty : ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → MeromorphicAt (f i) x),
  meromorphicOrderAt (E := 𝕜) (∏ i ∈ ∅, f i) x = ∑ i ∈ ∅, meromorphicOrderAt (f i) x
Tactic: induction s using Finset.induction with
  | empty =>
    rw [Finset.prod_empty, Finset.sum_empty, ← WithTop.coe_zero, meromorphicOrderAt_eq_int_iff]
    · exact ⟨1, analyticAt_const, by simp⟩
    · apply MeromorphicAt.const
  | insert a s ha hs =>
    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)))]
    congr
    rw [hs (fun i hi ↦ hf i (Finset.mem_insert_of_mem hi))]
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
hf : ∀ i ∈ s, MeromorphicAt (f i) x
empty :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → MeromorphicAt (f i) x),
    meromorphicOrderAt (E := 𝕜) (∏ i ∈ ∅, f i) x = ∑ i ∈ ∅, meromorphicOrderAt (f i) x
⊢ meromorphicOrderAt (E := 𝕜) (∏ i ∈ s, f i) x = ∑ i ∈ s, meromorphicOrderAt (f i) x
have insert : ∀ (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 a s, MeromorphicAt (f i) x),
  meromorphicOrderAt (E := 𝕜) (∏ i ∈ insert a s, f i) x = ∑ i ∈ insert a s, meromorphicOrderAt (f i) x
Tactic: induction s using Finset.induction with
  | empty =>
    rw [Finset.prod_empty, Finset.sum_empty, ← WithTop.coe_zero, meromorphicOrderAt_eq_int_iff]
    · exact ⟨1, analyticAt_const, by simp⟩
    · apply MeromorphicAt.const
  | insert a s ha hs =>
    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)))]
    congr
    rw [hs (fun i hi ↦ hf i (Finset.mem_insert_of_mem hi))]
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Order (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
hf : ∀ i ∈ s, MeromorphicAt (f i) x
⊢ meromorphicOrderAt (E := 𝕜) (∏ i ∈ s, f i) x = ∑ i ∈ s, meromorphicOrderAt (f i) x
have empty : ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → MeromorphicAt (f i) x),
  meromorphicOrderAt (E := 𝕜) (∏ i ∈ ∅, f i) x = ∑ i ∈ ∅, meromorphicOrderAt (f i) x
Tactic: classical
  induction s using Finset.induction with
  | empty =>
    rw [Finset.prod_empty, Finset.sum_empty, ← WithTop.coe_zero, meromorphicOrderAt_eq_int_iff]
    · exact ⟨1, analyticAt_const, by simp⟩
    · apply MeromorphicAt.const
  | insert a s ha hs =>
    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)))]
    congr
    rw [hs (fun i hi ↦ hf i (Finset.mem_insert_of_mem hi))]
Cleared hypotheses: s, hf