awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicOn f U
n : ℕ
⊢ divisor (f ^ n) U = HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U)
have h : ∀ (z : 𝕜),
  Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
Tactic: ext z
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicOn f U
n : ℕ
z : 𝕜
⊢ Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
have pos : ∀ (hn : n = 0),
  Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicOn f U
n : ℕ
z : 𝕜
pos :
  ∀ (hn : n = 0),
    Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
      ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
⊢ Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
have neg : ∀ (hn : ¬n = 0),
  Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicOn f U
n : ℕ
z : 𝕜
hn : ¬n = 0
⊢ Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
have pos : ∀ (hz : z ∈ U),
  Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
Tactic: by_cases hz : z ∈ U
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicOn f U
n : ℕ
z : 𝕜
hn : ¬n = 0
pos :
  ∀ (hz : z ∈ U),
    Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
      ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
⊢ Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
have neg : ∀ (hz : z ∉ U),
  Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
Tactic: by_cases hz : z ∈ U
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicOn f U
n : ℕ
⊢ divisor (f ^ n) U = HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U)
have h : ∀ (z : 𝕜),
  Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
Tactic: classical
  ext z
  by_cases hn : n = 0
  · simp [hn]
  by_cases hz : z ∈ U
  · simp [hf.pow, divisor_apply, meromorphicOrderAt_pow (hf z hz), hf, hz]
  · simp [hz]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicOn f U
n : ℕ
h :
  ∀ (z : 𝕜),
    Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
      ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
⊢ divisor (f ^ n) U = HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U)
have pos : ∀ (z : 𝕜) (hn : n = 0),
  Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
Tactic: classical
  ext z
  by_cases hn : n = 0
  · simp [hn]
  by_cases hz : z ∈ U
  · simp [hf.pow, divisor_apply, meromorphicOrderAt_pow (hf z hz), hf, hz]
  · simp [hz]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicOn f U
n : ℕ
h :
  ∀ (z : 𝕜),
    Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
      ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
pos :
  ∀ (z : 𝕜) (hn : n = 0),
    Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
      ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
⊢ divisor (f ^ n) U = HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U)
have neg : ∀ (z : 𝕜) (hn : ¬n = 0),
  Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
Tactic: classical
  ext z
  by_cases hn : n = 0
  · simp [hn]
  by_cases hz : z ∈ U
  · simp [hf.pow, divisor_apply, meromorphicOrderAt_pow (hf z hz), hf, hz]
  · simp [hz]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicOn f U
n : ℕ
h :
  ∀ (z : 𝕜),
    Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
      ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
pos :
  ∀ (z : 𝕜) (hn : n = 0),
    Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
      ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
neg neg₁ :
  ∀ (z : 𝕜) (hn : ¬n = 0),
    Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
      ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
⊢ divisor (f ^ n) U = HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U)
have pos₁ : ∀ (z : 𝕜) (hn : ¬n = 0) (hz : z ∈ U),
  Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
Tactic: classical
  ext z
  by_cases hn : n = 0
  · simp [hn]
  by_cases hz : z ∈ U
  · simp [hf.pow, divisor_apply, meromorphicOrderAt_pow (hf z hz), hf, hz]
  · simp [hz]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicOn f U
n : ℕ
h :
  ∀ (z : 𝕜),
    Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
      ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
pos :
  ∀ (z : 𝕜) (hn : n = 0),
    Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
      ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
neg neg₁ :
  ∀ (z : 𝕜) (hn : ¬n = 0),
    Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
      ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
pos₁ :
  ∀ (z : 𝕜) (hn : ¬n = 0) (hz : z ∈ U),
    Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
      ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
⊢ divisor (f ^ n) U = HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U)
have neg₂ : ∀ (z : 𝕜) (hn : ¬n = 0) (hz : z ∉ U),
  Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
Tactic: classical
  ext z
  by_cases hn : n = 0
  · simp [hn]
  by_cases hz : z ∈ U
  · simp [hf.pow, divisor_apply, meromorphicOrderAt_pow (hf z hz), hf, hz]
  · simp [hz]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicOn f U
n : ℤ
⊢ divisor (f ^ n) U = HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U)
have h : ∀ (z : 𝕜),
  Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
Tactic: ext z
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicOn f U
n : ℤ
z : 𝕜
⊢ Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
have pos : ∀ (hn : n = 0),
  Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicOn f U
n : ℤ
z : 𝕜
pos :
  ∀ (hn : n = 0),
    Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
      ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
⊢ Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
have neg : ∀ (hn : ¬n = 0),
  Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicOn f U
n : ℤ
z : 𝕜
hn : ¬n = 0
⊢ Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
have pos : ∀ (hz : z ∈ U),
  Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
Tactic: by_cases hz : z ∈ U
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicOn f U
n : ℤ
z : 𝕜
hn : ¬n = 0
pos :
  ∀ (hz : z ∈ U),
    Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
      ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
⊢ Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
have neg : ∀ (hz : z ∉ U),
  Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
Tactic: by_cases hz : z ∈ U
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicOn f U
n : ℤ
⊢ divisor (f ^ n) U = HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U)
have h : ∀ (z : 𝕜),
  Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
Tactic: classical
  ext z
  by_cases hn : n = 0
  · simp [hn]
  by_cases hz : z ∈ U
  · simp [hf.zpow, divisor_apply, meromorphicOrderAt_zpow (hf z hz), hf, hz]
  · simp [hz]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicOn f U
n : ℤ
h :
  ∀ (z : 𝕜),
    Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
      ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
⊢ divisor (f ^ n) U = HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U)
have pos : ∀ (z : 𝕜) (hn : n = 0),
  Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
Tactic: classical
  ext z
  by_cases hn : n = 0
  · simp [hn]
  by_cases hz : z ∈ U
  · simp [hf.zpow, divisor_apply, meromorphicOrderAt_zpow (hf z hz), hf, hz]
  · simp [hz]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicOn f U
n : ℤ
h :
  ∀ (z : 𝕜),
    Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
      ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
pos :
  ∀ (z : 𝕜) (hn : n = 0),
    Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
      ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
⊢ divisor (f ^ n) U = HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U)
have neg : ∀ (z : 𝕜) (hn : ¬n = 0),
  Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
Tactic: classical
  ext z
  by_cases hn : n = 0
  · simp [hn]
  by_cases hz : z ∈ U
  · simp [hf.zpow, divisor_apply, meromorphicOrderAt_zpow (hf z hz), hf, hz]
  · simp [hz]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicOn f U
n : ℤ
h :
  ∀ (z : 𝕜),
    Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
      ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
pos :
  ∀ (z : 𝕜) (hn : n = 0),
    Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
      ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
neg neg₁ :
  ∀ (z : 𝕜) (hn : ¬n = 0),
    Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
      ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
⊢ divisor (f ^ n) U = HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U)
have pos₁ : ∀ (z : 𝕜) (hn : ¬n = 0) (hz : z ∈ U),
  Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
Tactic: classical
  ext z
  by_cases hn : n = 0
  · simp [hn]
  by_cases hz : z ∈ U
  · simp [hf.zpow, divisor_apply, meromorphicOrderAt_zpow (hf z hz), hf, hz]
  · simp [hz]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicOn f U
n : ℤ
h :
  ∀ (z : 𝕜),
    Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
      ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
pos :
  ∀ (z : 𝕜) (hn : n = 0),
    Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
      ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
neg neg₁ :
  ∀ (z : 𝕜) (hn : ¬n = 0),
    Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
      ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
pos₁ :
  ∀ (z : 𝕜) (hn : ¬n = 0) (hz : z ∈ U),
    Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
      ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
⊢ divisor (f ^ n) U = HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U)
have neg₂ : ∀ (z : 𝕜) (hn : ¬n = 0) (hz : z ∉ U),
  Eq (α := ℤ) ((divisor (f ^ n) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U) : (a : 𝕜) → ℤ) z : ℤ)
Tactic: classical
  ext z
  by_cases hn : n = 0
  · simp [hn]
  by_cases hz : z ∈ U
  · simp [hf.zpow, divisor_apply, meromorphicOrderAt_zpow (hf z hz), hf, hz]
  · simp [hz]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
V : Set 𝕜
hf : MeromorphicOn f U
hV : V ⊆ U
⊢ Eq (α := Function.locallyFinsuppWithin V ℤ)
    (Function.locallyFinsuppWithin.restrict (U := U) (V := V) (divisor f U) hV) (divisor f V)
have h : ∀ (x : 𝕜),
  Eq (α := ℤ) ((Function.locallyFinsuppWithin.restrict (U := U) (V := V) (divisor f U) hV : (a : 𝕜) → ℤ) x : ℤ)
    ((divisor f V : (a : 𝕜) → ℤ) x : ℤ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
V : Set 𝕜
hf : MeromorphicOn f U
hV : V ⊆ U
x : 𝕜
⊢ Eq (α := ℤ) ((Function.locallyFinsuppWithin.restrict (U := U) (V := V) (divisor f U) hV : (a : 𝕜) → ℤ) x : ℤ)
    ((divisor f V : (a : 𝕜) → ℤ) x : ℤ)
have pos : ∀ (hx : x ∈ V),
  Eq (α := ℤ) ((Function.locallyFinsuppWithin.restrict (U := U) (V := V) (divisor f U) hV : (a : 𝕜) → ℤ) x : ℤ)
    ((divisor f V : (a : 𝕜) → ℤ) x : ℤ)
Tactic: by_cases hx : x ∈ V
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 → E
V : Set 𝕜
hf : MeromorphicOn f U
hV : V ⊆ U
x : 𝕜
pos :
  ∀ (hx : x ∈ V),
    Eq (α := ℤ) ((Function.locallyFinsuppWithin.restrict (U := U) (V := V) (divisor f U) hV : (a : 𝕜) → ℤ) x : ℤ)
      ((divisor f V : (a : 𝕜) → ℤ) x : ℤ)
⊢ Eq (α := ℤ) ((Function.locallyFinsuppWithin.restrict (U := U) (V := V) (divisor f U) hV : (a : 𝕜) → ℤ) x : ℤ)
    ((divisor f V : (a : 𝕜) → ℤ) x : ℤ)
have neg : ∀ (hx : x ∉ V),
  Eq (α := ℤ) ((Function.locallyFinsuppWithin.restrict (U := U) (V := V) (divisor f U) hV : (a : 𝕜) → ℤ) x : ℤ)
    ((divisor f V : (a : 𝕜) → ℤ) x : ℤ)
Tactic: by_cases hx : x ∈ V
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : AnalyticOnNhd 𝕜 f₂ U
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (f₁ + f₂) U)⁻ (divisor f₁ U)⁻
have h : ∀ (x : 𝕜), Eq (α := ℤ) (((divisor (f₁ + f₂) U)⁻ : (a : 𝕜) → ℤ) x : ℤ) (((divisor f₁ U)⁻ : (a : 𝕜) → ℤ) x : ℤ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : AnalyticOnNhd 𝕜 f₂ U
x : 𝕜
⊢ Eq (α := ℤ) (((divisor (f₁ + f₂) U)⁻ : (a : 𝕜) → ℤ) x : ℤ) (((divisor f₁ U)⁻ : (a : 𝕜) → ℤ) x : ℤ)
have pos : ∀ (hx : x ∈ U), Eq (α := ℤ) (((divisor (f₁ + f₂) U)⁻ : (a : 𝕜) → ℤ) x : ℤ) (((divisor f₁ U)⁻ : (a : 𝕜) → ℤ) x : ℤ)
Tactic: by_cases hx : x ∈ U
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : AnalyticOnNhd 𝕜 f₂ U
x : 𝕜
pos : ∀ (hx : x ∈ U), Eq (α := ℤ) (((divisor (f₁ + f₂) U)⁻ : (a : 𝕜) → ℤ) x : ℤ) (((divisor f₁ U)⁻ : (a : 𝕜) → ℤ) x : ℤ)
⊢ Eq (α := ℤ) (((divisor (f₁ + f₂) U)⁻ : (a : 𝕜) → ℤ) x : ℤ) (((divisor f₁ U)⁻ : (a : 𝕜) → ℤ) x : ℤ)
have neg : ∀ (hx : x ∉ U), Eq (α := ℤ) (((divisor (f₁ + f₂) U)⁻ : (a : 𝕜) → ℤ) x : ℤ) (((divisor f₁ U)⁻ : (a : 𝕜) → ℤ) x : ℤ)
Tactic: by_cases hx : x ∈ U
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : AnalyticOnNhd 𝕜 f₂ U
x : 𝕜
hx : x ∈ U
⊢ Eq (α := ℤ) (((divisor (f₁ + f₂) U)⁻ : (a : 𝕜) → ℤ) x : ℤ) (((divisor f₁ U)⁻ : (a : 𝕜) → ℤ) x : ℤ)
have pos : max (-(meromorphicOrderAt (f₁ + f₂) x).untop₀) 0 = max (-(meromorphicOrderAt f₁ x).untop₀) 0
Tactic: suffices -(meromorphicOrderAt (f₁ + f₂) x).untop₀ ⊔ 0 = -(meromorphicOrderAt f₁ x).untop₀ ⊔ 0 by
      simpa [negPart_def, hx, hf₁, hf₁.add hf₂.meromorphicOn]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : AnalyticOnNhd 𝕜 f₂ U
x : 𝕜
hx : x ∈ U
⊢ max (-(meromorphicOrderAt (f₁ + f₂) x).untop₀) 0 = max (-(meromorphicOrderAt f₁ x).untop₀) 0
have pos : ∀ (h : 0 ≤ meromorphicOrderAt f₁ x),
  max (-(meromorphicOrderAt (f₁ + f₂) x).untop₀) 0 = max (-(meromorphicOrderAt f₁ x).untop₀) 0
Tactic: by_cases h : 0 ≤ meromorphicOrderAt f₁ x
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : AnalyticOnNhd 𝕜 f₂ U
x : 𝕜
hx : x ∈ U
pos :
  ∀ (h : 0 ≤ meromorphicOrderAt f₁ x),
    max (-(meromorphicOrderAt (f₁ + f₂) x).untop₀) 0 = max (-(meromorphicOrderAt f₁ x).untop₀) 0
⊢ max (-(meromorphicOrderAt (f₁ + f₂) x).untop₀) 0 = max (-(meromorphicOrderAt f₁ x).untop₀) 0
have neg : ∀ (h : ¬0 ≤ meromorphicOrderAt f₁ x),
  max (-(meromorphicOrderAt (f₁ + f₂) x).untop₀) 0 = max (-(meromorphicOrderAt f₁ x).untop₀) 0
Tactic: by_cases h : 0 ≤ meromorphicOrderAt f₁ x
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : AnalyticOnNhd 𝕜 f₂ U
x : 𝕜
hx : x ∈ U
h : 0 ≤ meromorphicOrderAt f₁ x
⊢ max (-(meromorphicOrderAt (f₁ + f₂) x).untop₀) 0 = max (-(meromorphicOrderAt f₁ x).untop₀) 0
have pos : 0 ≤ meromorphicOrderAt (f₁ + f₂) x
Tactic: suffices 0 ≤ meromorphicOrderAt (f₁ + f₂) x by simp_all
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : AnalyticOnNhd 𝕜 f₂ U
x : 𝕜
hx : x ∈ U
h : ¬0 ≤ meromorphicOrderAt f₁ x
this : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
⊢ max (-(meromorphicOrderAt (f₁ + f₂) x).untop₀) 0 = max (-(meromorphicOrderAt f₁ x).untop₀) 0
have rwa : max (-(meromorphicOrderAt f₁ x).untop₀) 0 = max (-(meromorphicOrderAt f₁ x).untop₀) 0
Tactic: rwa [meromorphicOrderAt_add_eq_left_of_lt (hf₂.meromorphicOn x hx)]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : AnalyticOnNhd 𝕜 f₂ U
x : 𝕜
hx : x ∈ U
h : ¬0 ≤ meromorphicOrderAt f₁ x
⊢ max (-(meromorphicOrderAt (f₁ + f₂) x).untop₀) 0 = max (-(meromorphicOrderAt f₁ x).untop₀) 0
have neg : meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
Tactic: suffices meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x by
        rwa [meromorphicOrderAt_add_eq_left_of_lt (hf₂.meromorphicOn x hx)]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : MeromorphicOn f₁ U
hf₂ : AnalyticOnNhd 𝕜 f₂ U
x : 𝕜
hx : x ∈ U
h : ¬0 ≤ meromorphicOrderAt f₁ x
⊢ meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x
have calc : meromorphicOrderAt f₁ x < 0
Tactic: calc meromorphicOrderAt f₁ x
      _ < 0 := by simpa using h
      _ ≤ meromorphicOrderAt f₂ x := (hf₂ x hx).meromorphicOrderAt_nonneg
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
hf₁ : AnalyticOnNhd 𝕜 f₁ U
hf₂ : MeromorphicOn f₂ U
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (f₁ + f₂) U)⁻ (divisor f₂ U)⁻
have rw : Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (f₂ + f₁) U)⁻ (divisor f₂ U)⁻
Tactic: rw [add_comm]