awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
z : 𝕜
pos :
  ∀ (hz : z ∉ U),
    LE.le (α := (fun (a : 𝕜) ↦ ℤ) z) (((divisor (f₁ + f₂) U)⁻ : (a : 𝕜) → ℤ) z : ℤ)
      (((divisor f₁ U)⁻ ⊔ (divisor f₂ U)⁻ : (a : 𝕜) → ℤ) z : ℤ)
⊢ LE.le (α := (fun (a : 𝕜) ↦ ℤ) z) (((divisor (f₁ + f₂) U)⁻ : (a : 𝕜) → ℤ) z : ℤ)
    (((divisor f₁ U)⁻ ⊔ (divisor f₂ U)⁻ : (a : 𝕜) → ℤ) z : ℤ)
have neg : ∀ (hz : z ∈ U),
  LE.le (α := (fun (a : 𝕜) ↦ ℤ) z) (((divisor (f₁ + f₂) U)⁻ : (a : 𝕜) → ℤ) z : ℤ)
    (((divisor f₁ U)⁻ ⊔ (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 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
z : 𝕜
hz : z ∈ U
⊢ LE.le (α := ℤ) (((divisor (f₁ + f₂) U : (a : 𝕜) → ℤ) z)⁻ : ℤ)
    (max ((divisor f₁ U : (a : 𝕜) → ℤ) z)⁻ ((divisor f₂ U : (a : 𝕜) → ℤ) z)⁻ : ℤ)
have pos : ∀ (hf₁₂ : meromorphicOrderAt (f₁ + f₂) z = ⊤),
  LE.le (α := ℤ) (((divisor (f₁ + f₂) U : (a : 𝕜) → ℤ) z)⁻ : ℤ)
    (max ((divisor f₁ U : (a : 𝕜) → ℤ) z)⁻ ((divisor f₂ U : (a : 𝕜) → ℤ) z)⁻ : ℤ)
Tactic: by_cases hf₁₂ : meromorphicOrderAt (f₁ + f₂) z = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
z : 𝕜
hz : z ∈ U
pos :
  ∀ (hf₁₂ : meromorphicOrderAt (f₁ + f₂) z = ⊤),
    LE.le (α := ℤ) (((divisor (f₁ + f₂) U : (a : 𝕜) → ℤ) z)⁻ : ℤ)
      (max ((divisor f₁ U : (a : 𝕜) → ℤ) z)⁻ ((divisor f₂ U : (a : 𝕜) → ℤ) z)⁻ : ℤ)
⊢ LE.le (α := ℤ) (((divisor (f₁ + f₂) U : (a : 𝕜) → ℤ) z)⁻ : ℤ)
    (max ((divisor f₁ U : (a : 𝕜) → ℤ) z)⁻ ((divisor f₂ U : (a : 𝕜) → ℤ) z)⁻ : ℤ)
have neg : ∀ (hf₁₂ : ¬meromorphicOrderAt (f₁ + f₂) z = ⊤),
  LE.le (α := ℤ) (((divisor (f₁ + f₂) U : (a : 𝕜) → ℤ) z)⁻ : ℤ)
    (max ((divisor f₁ U : (a : 𝕜) → ℤ) z)⁻ ((divisor f₂ U : (a : 𝕜) → ℤ) z)⁻ : ℤ)
Tactic: by_cases hf₁₂ : meromorphicOrderAt (f₁ + f₂) z = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
z : 𝕜
hz : z ∈ U
hf₁₂ : ¬meromorphicOrderAt (f₁ + f₂) z = ⊤
⊢ LE.le (α := ℤ) (((divisor (f₁ + f₂) U : (a : 𝕜) → ℤ) z)⁻ : ℤ)
    (max ((divisor f₁ U : (a : 𝕜) → ℤ) z)⁻ ((divisor f₂ U : (a : 𝕜) → ℤ) z)⁻ : ℤ)
have neg : LE.le (α := ℤ) (((divisor (f₁ + f₂) U : (a : 𝕜) → ℤ) z)⁻ : ℤ)
  ((min ((divisor f₁ U : (a : 𝕜) → ℤ) z) ((divisor f₂ U : (a : 𝕜) → ℤ) z))⁻ : ℤ)
Tactic: rw [← negPart_min]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
⊢ (divisor f₁ U)⁻ ⊔ (divisor f₂ U)⁻ ≤ HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U)⁻ (divisor f₂ U)⁻
have pos : ∀ (h : LE.le (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U)⁻ (divisor f₂ U)⁻),
  (divisor f₁ U)⁻ ⊔ (divisor f₂ U)⁻ ≤ HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U)⁻ (divisor f₂ U)⁻
Tactic: by_cases h : (divisor f₁ U)⁻ ≤ (divisor f₂ U)⁻
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
pos :
  ∀ (h : LE.le (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U)⁻ (divisor f₂ U)⁻),
    (divisor f₁ U)⁻ ⊔ (divisor f₂ U)⁻ ≤
      HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U)⁻ (divisor f₂ U)⁻
⊢ (divisor f₁ U)⁻ ⊔ (divisor f₂ U)⁻ ≤ HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U)⁻ (divisor f₂ U)⁻
have neg : ∀ (h : ¬LE.le (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U)⁻ (divisor f₂ U)⁻),
  (divisor f₁ U)⁻ ⊔ (divisor f₂ U)⁻ ≤ HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U)⁻ (divisor f₂ U)⁻
Tactic: by_cases h : (divisor f₁ U)⁻ ≤ (divisor f₂ U)⁻
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
U : Set 𝕜
hf₁ : MeromorphicOn f₁ U
hf₂ : MeromorphicOn f₂ U
⊢ (divisor (f₁ + f₂) U)⁻ ≤ HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U)⁻ (divisor f₂ U)⁻
have calc : (divisor f₁ U)⁻ ⊔ (divisor f₂ U)⁻ ≤ HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U)⁻ (divisor f₂ U)⁻
Tactic: calc (divisor (f₁ + f₂) U)⁻
    _ ≤ max (divisor f₁ U)⁻ (divisor f₂ U)⁻ :=
      negPart_divisor_add_le_max hf₁ hf₂
    _ ≤ (divisor f₁ U)⁻ + (divisor f₂ U)⁻ := by
      by_cases h : (divisor f₁ U)⁻ ≤ (divisor f₂ U)⁻
      <;> simp_all [negPart_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
h₁f₁ : MeromorphicOn f₁ U
h₁f₂ : MeromorphicOn f₂ U
h₂f₁ : ∀ z ∈ U, meromorphicOrderAt f₁ z ≠ ⊤
h₂f₂ : ∀ z ∈ U, meromorphicOrderAt f₂ z ≠ ⊤
⊢ divisor (f₁ • f₂) U = HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U) (divisor f₂ U)
have h : ∀ (z : 𝕜),
  Eq (α := ℤ) ((divisor (f₁ • f₂) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U) (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 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ : 𝕜 → 𝕜
f₂ : 𝕜 → E
h₁f₁ : MeromorphicOn f₁ U
h₁f₂ : MeromorphicOn f₂ U
h₂f₁ : ∀ z ∈ U, meromorphicOrderAt f₁ z ≠ ⊤
h₂f₂ : ∀ z ∈ U, meromorphicOrderAt f₂ z ≠ ⊤
z : 𝕜
⊢ Eq (α := ℤ) ((divisor (f₁ • f₂) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U) (divisor f₂ U) : (a : 𝕜) → ℤ) z : ℤ)
have pos : ∀ (hz : z ∈ U),
  Eq (α := ℤ) ((divisor (f₁ • f₂) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U) (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 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ : 𝕜 → 𝕜
f₂ : 𝕜 → E
h₁f₁ : MeromorphicOn f₁ U
h₁f₂ : MeromorphicOn f₂ U
h₂f₁ : ∀ z ∈ U, meromorphicOrderAt f₁ z ≠ ⊤
h₂f₂ : ∀ z ∈ U, meromorphicOrderAt f₂ z ≠ ⊤
z : 𝕜
pos :
  ∀ (hz : z ∈ U),
    Eq (α := ℤ) ((divisor (f₁ • f₂) U : (a : 𝕜) → ℤ) z : ℤ)
      ((HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U) (divisor f₂ U) : (a : 𝕜) → ℤ) z : ℤ)
⊢ Eq (α := ℤ) ((divisor (f₁ • f₂) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U) (divisor f₂ U) : (a : 𝕜) → ℤ) z : ℤ)
have neg : ∀ (hz : z ∉ U),
  Eq (α := ℤ) ((divisor (f₁ • f₂) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U) (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 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f₁ : 𝕜 → 𝕜
f₂ : 𝕜 → E
h₁f₁ : MeromorphicOn f₁ U
h₁f₂ : MeromorphicOn f₂ U
h₂f₁ : ∀ z ∈ U, meromorphicOrderAt f₁ z ≠ ⊤
h₂f₂ : ∀ z ∈ U, meromorphicOrderAt f₂ z ≠ ⊤
z : 𝕜
hz : z ∈ U
⊢ Eq (α := ℤ) ((divisor (f₁ • f₂) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U) (divisor f₂ U) : (a : 𝕜) → ℤ) z : ℤ)
have pos : ∀ (a₁ : ℤ) (ha₁ : (↑a₁ : WithTop ℤ) = meromorphicOrderAt f₁ z),
  Eq (α := ℤ) ((divisor (f₁ • f₂) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U) (divisor f₂ U) : (a : 𝕜) → ℤ) z : ℤ)
Tactic: lift meromorphicOrderAt f₁ z to ℤ using (h₂f₁ z hz) with a₁ ha₁
-- 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
h₁f₁ : MeromorphicOn f₁ U
h₁f₂ : MeromorphicOn f₂ U
h₂f₁ : ∀ z ∈ U, meromorphicOrderAt f₁ z ≠ ⊤
h₂f₂ : ∀ z ∈ U, meromorphicOrderAt f₂ z ≠ ⊤
z : 𝕜
hz : z ∈ U
a₁ : ℤ
ha₁ : (↑a₁ : WithTop ℤ) = meromorphicOrderAt f₁ z
⊢ Eq (α := ℤ) ((divisor (f₁ • f₂) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U) (divisor f₂ U) : (a : 𝕜) → ℤ) z : ℤ)
have pos : ∀ (a₂ : ℤ) (ha₂ : (↑a₂ : WithTop ℤ) = meromorphicOrderAt f₂ z),
  Eq (α := ℤ) ((divisor (f₁ • f₂) U : (a : 𝕜) → ℤ) z : ℤ)
    ((HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U) (divisor f₂ U) : (a : 𝕜) → ℤ) z : ℤ)
Tactic: lift meromorphicOrderAt f₂ z to ℤ using (h₂f₂ z hz) with a₂ ha₂
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
a : ι
s : Finset ι
ha : a ∉ s
hs :
  ∀ (h₁f : ∀ i ∈ s, MeromorphicOn (f i) U) (h₂f : ∀ i ∈ s, ∀ z ∈ U, meromorphicOrderAt (f i) z ≠ ⊤),
    Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (E := 𝕜) (∏ i ∈ s, f i) U) (∑ i ∈ s, divisor (f i) U)
h₁f : ∀ i ∈ insert a s, MeromorphicOn (f i) U
h₂f : ∀ i ∈ insert a s, ∀ z ∈ U, meromorphicOrderAt (f i) z ≠ ⊤
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (E := 𝕜) (∏ i ∈ insert a s, f i) U)
    (∑ i ∈ insert a s, divisor (f i) U)
have this : ∀ (z : 𝕜) (hz : z ∈ U), meromorphicOrderAt (E := 𝕜) (∏ i ∈ s, f i) z ≠ ⊤
Tactic: have (z) (hz : z ∈ U) : meromorphicOrderAt (∏ i ∈ s, f i) z ≠ ⊤ := by
      simpa [meromorphicOrderAt_prod (fun i hi ↦ h₁f i (mem_insert_of_mem hi) z hz)]
        using fun i hi ↦ h₂f i (mem_insert_of_mem hi) z hz
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
a : ι
s : Finset ι
ha : a ∉ s
hs :
  ∀ (h₁f : ∀ i ∈ s, MeromorphicOn (f i) U) (h₂f : ∀ i ∈ s, ∀ z ∈ U, meromorphicOrderAt (f i) z ≠ ⊤),
    Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (E := 𝕜) (∏ i ∈ s, f i) U) (∑ i ∈ s, divisor (f i) U)
h₁f : ∀ i ∈ insert a s, MeromorphicOn (f i) U
h₂f : ∀ i ∈ insert a s, ∀ z ∈ U, meromorphicOrderAt (f i) z ≠ ⊤
this : ∀ (z : 𝕜) (hz : z ∈ U), meromorphicOrderAt (E := 𝕜) (∏ i ∈ s, f i) z ≠ ⊤
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (E := 𝕜) (∏ i ∈ insert a s, f i) U)
    (∑ i ∈ insert a s, divisor (f i) U)
have insert : Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (f a * ∏ x ∈ s, f x) U) (∑ i ∈ insert a s, divisor (f i) U)
Tactic: rw [prod_insert ha, sum_insert ha, divisor_mul (by aesop)
        (prod (fun i hi ↦ h₁f i (mem_insert_of_mem hi)))
        (h₂f a (mem_insert_self a s)) this,
      hs (fun i hi ↦ h₁f i (mem_insert_of_mem hi))
        (fun i hi ↦ h₂f i (mem_insert_of_mem hi))]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
a : ι
s : Finset ι
ha : a ∉ s
hs :
  ∀ (h₁f : ∀ i ∈ s, MeromorphicOn (f i) U) (h₂f : ∀ i ∈ s, ∀ z ∈ U, meromorphicOrderAt (f i) z ≠ ⊤),
    Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (E := 𝕜) (∏ i ∈ s, f i) U) (∑ i ∈ s, divisor (f i) U)
h₁f : ∀ i ∈ Insert.insert a s, MeromorphicOn (f i) U
h₂f : ∀ i ∈ Insert.insert a s, ∀ z ∈ U, meromorphicOrderAt (f i) z ≠ ⊤
this : ∀ (z : 𝕜) (hz : z ∈ U), meromorphicOrderAt (E := 𝕜) (∏ i ∈ s, f i) z ≠ ⊤
insert :
  Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (f a * ∏ x ∈ s, f x) U)
    (∑ i ∈ Insert.insert a s, divisor (f i) U)
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (E := 𝕜) (∏ i ∈ Insert.insert a s, f i) U)
    (∑ i ∈ Insert.insert a s, divisor (f i) U)
have insert₁ : divisor (f a * ∏ x ∈ s, f x) U =
  HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor (f a) U) (∑ x ∈ s, divisor (f x) U)
Tactic: rw [prod_insert ha, sum_insert ha, divisor_mul (by aesop)
        (prod (fun i hi ↦ h₁f i (mem_insert_of_mem hi)))
        (h₂f a (mem_insert_self a s)) this,
      hs (fun i hi ↦ h₁f i (mem_insert_of_mem hi))
        (fun i hi ↦ h₂f i (mem_insert_of_mem hi))]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
a : ι
s : Finset ι
ha : a ∉ s
hs :
  ∀ (h₁f : ∀ i ∈ s, MeromorphicOn (f i) U) (h₂f : ∀ i ∈ s, ∀ z ∈ U, meromorphicOrderAt (f i) z ≠ ⊤),
    Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (E := 𝕜) (∏ i ∈ s, f i) U) (∑ i ∈ s, divisor (f i) U)
h₁f : ∀ i ∈ Insert.insert a s, MeromorphicOn (f i) U
h₂f : ∀ i ∈ Insert.insert a s, ∀ z ∈ U, meromorphicOrderAt (f i) z ≠ ⊤
this : ∀ (z : 𝕜) (hz : z ∈ U), meromorphicOrderAt (E := 𝕜) (∏ i ∈ s, f i) z ≠ ⊤
insert :
  Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (f a * ∏ x ∈ s, f x) U)
    (∑ i ∈ Insert.insert a s, divisor (f i) U)
insert₁ :
  divisor (f a * ∏ x ∈ s, f x) U =
    HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor (f a) U) (∑ x ∈ s, divisor (f x) U)
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (E := 𝕜) (∏ i ∈ Insert.insert a s, f i) U)
    (∑ i ∈ Insert.insert a s, divisor (f i) U)
have insert₂ : HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor (f a) U) (divisor (E := 𝕜) (∏ n ∈ s, f n) U) =
  HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor (f a) U) (∑ x ∈ s, divisor (f x) U)
Tactic: rw [prod_insert ha, sum_insert ha, divisor_mul (by aesop)
        (prod (fun i hi ↦ h₁f i (mem_insert_of_mem hi)))
        (h₂f a (mem_insert_self a s)) this,
      hs (fun i hi ↦ h₁f i (mem_insert_of_mem hi))
        (fun i hi ↦ h₂f i (mem_insert_of_mem hi))]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
a : ι
s : Finset ι
ha : a ∉ s
hs :
  ∀ (h₁f : ∀ i ∈ s, MeromorphicOn (f i) U) (h₂f : ∀ i ∈ s, ∀ z ∈ U, meromorphicOrderAt (f i) z ≠ ⊤),
    Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (E := 𝕜) (∏ i ∈ s, f i) U) (∑ i ∈ s, divisor (f i) U)
h₁f : ∀ i ∈ Insert.insert a s, MeromorphicOn (f i) U
h₂f : ∀ i ∈ Insert.insert a s, ∀ z ∈ U, meromorphicOrderAt (f i) z ≠ ⊤
this : ∀ (z : 𝕜) (hz : z ∈ U), meromorphicOrderAt (E := 𝕜) (∏ i ∈ s, f i) z ≠ ⊤
insert :
  Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (f a * ∏ x ∈ s, f x) U)
    (∑ i ∈ Insert.insert a s, divisor (f i) U)
insert₁ :
  divisor (f a * ∏ x ∈ s, f x) U =
    HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor (f a) U) (∑ x ∈ s, divisor (f x) U)
insert₂ :
  HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor (f a) U) (divisor (E := 𝕜) (∏ n ∈ s, f n) U) =
    HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor (f a) U) (∑ x ∈ s, divisor (f x) U)
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (E := 𝕜) (∏ i ∈ Insert.insert a s, f i) U)
    (∑ i ∈ Insert.insert a s, divisor (f i) U)
have insert₃ : HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor (f a) U) (∑ i ∈ s, divisor (f i) U) =
  HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor (f a) U) (∑ x ∈ s, divisor (f x) U)
Tactic: rw [prod_insert ha, sum_insert ha, divisor_mul (by aesop)
        (prod (fun i hi ↦ h₁f i (mem_insert_of_mem hi)))
        (h₂f a (mem_insert_self a s)) this,
      hs (fun i hi ↦ h₁f i (mem_insert_of_mem hi))
        (fun i hi ↦ h₂f i (mem_insert_of_mem hi))]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicOn (f i) U
h₂f : ∀ i ∈ s, ∀ z ∈ U, meromorphicOrderAt (f i) z ≠ ⊤
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (E := 𝕜) (∏ i ∈ s, f i) U) (∑ i ∈ s, divisor (f i) U)
have empty : ∀ (h₁f : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → MeromorphicOn (f i) U)
  (h₂f : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → ∀ z ∈ U, meromorphicOrderAt (f i) z ≠ ⊤),
  Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (E := 𝕜) (∏ i ∈ ∅, f i) U) (∑ i ∈ ∅, divisor (f i) U)
Tactic: induction s using Finset.induction with
  | empty =>
    rw [prod_empty, sum_empty]
    exact divisor_ofNat 1
  | insert a s ha hs =>
    have (z) (hz : z ∈ U) : meromorphicOrderAt (∏ i ∈ s, f i) z ≠ ⊤ := by
      simpa [meromorphicOrderAt_prod (fun i hi ↦ h₁f i (mem_insert_of_mem hi) z hz)]
        using fun i hi ↦ h₂f i (mem_insert_of_mem hi) z hz
    rw [prod_insert ha, sum_insert ha, divisor_mul (by aesop)
        (prod (fun i hi ↦ h₁f i (mem_insert_of_mem hi)))
        (h₂f a (mem_insert_self a s)) this,
      hs (fun i hi ↦ h₁f i (mem_insert_of_mem hi))
        (fun i hi ↦ h₂f i (mem_insert_of_mem hi))]
Cleared hypotheses: s, h₁f, h₂f
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicOn (f i) U
h₂f : ∀ i ∈ s, ∀ z ∈ U, meromorphicOrderAt (f i) z ≠ ⊤
empty :
  ∀ (h₁f : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → MeromorphicOn (f i) U)
    (h₂f : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → ∀ z ∈ U, meromorphicOrderAt (f i) z ≠ ⊤),
    Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (E := 𝕜) (∏ i ∈ ∅, f i) U) (∑ i ∈ ∅, divisor (f i) U)
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (E := 𝕜) (∏ i ∈ s, f i) U) (∑ i ∈ s, divisor (f i) U)
have insert : ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
  (hs :
    ∀ (h₁f : ∀ i ∈ s, MeromorphicOn (f i) U) (h₂f : ∀ i ∈ s, ∀ z ∈ U, meromorphicOrderAt (f i) z ≠ ⊤),
      Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (E := 𝕜) (∏ i ∈ s, f i) U) (∑ i ∈ s, divisor (f i) U))
  (h₁f : ∀ i ∈ insert a s, MeromorphicOn (f i) U) (h₂f : ∀ i ∈ insert a s, ∀ z ∈ U, meromorphicOrderAt (f i) z ≠ ⊤),
  Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (E := 𝕜) (∏ i ∈ insert a s, f i) U)
    (∑ i ∈ insert a s, divisor (f i) U)
Tactic: induction s using Finset.induction with
  | empty =>
    rw [prod_empty, sum_empty]
    exact divisor_ofNat 1
  | insert a s ha hs =>
    have (z) (hz : z ∈ U) : meromorphicOrderAt (∏ i ∈ s, f i) z ≠ ⊤ := by
      simpa [meromorphicOrderAt_prod (fun i hi ↦ h₁f i (mem_insert_of_mem hi) z hz)]
        using fun i hi ↦ h₂f i (mem_insert_of_mem hi) z hz
    rw [prod_insert ha, sum_insert ha, divisor_mul (by aesop)
        (prod (fun i hi ↦ h₁f i (mem_insert_of_mem hi)))
        (h₂f a (mem_insert_self a s)) this,
      hs (fun i hi ↦ h₁f i (mem_insert_of_mem hi))
        (fun i hi ↦ h₂f i (mem_insert_of_mem hi))]
Cleared hypotheses: s, h₁f, h₂f
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicOn (f i) U
h₂f : ∀ i ∈ s, ∀ z ∈ U, meromorphicOrderAt (f i) z ≠ ⊤
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (E := 𝕜) (∏ i ∈ s, f i) U) (∑ i ∈ s, divisor (f i) U)
have empty : ∀ (h₁f : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → MeromorphicOn (f i) U)
  (h₂f : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → ∀ z ∈ U, meromorphicOrderAt (f i) z ≠ ⊤),
  Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (E := 𝕜) (∏ i ∈ ∅, f i) U) (∑ i ∈ ∅, divisor (f i) U)
Tactic: classical
  induction s using Finset.induction with
  | empty =>
    rw [prod_empty, sum_empty]
    exact divisor_ofNat 1
  | insert a s ha hs =>
    have (z) (hz : z ∈ U) : meromorphicOrderAt (∏ i ∈ s, f i) z ≠ ⊤ := by
      simpa [meromorphicOrderAt_prod (fun i hi ↦ h₁f i (mem_insert_of_mem hi) z hz)]
        using fun i hi ↦ h₂f i (mem_insert_of_mem hi) z hz
    rw [prod_insert ha, sum_insert ha, divisor_mul (by aesop)
        (prod (fun i hi ↦ h₁f i (mem_insert_of_mem hi)))
        (h₂f a (mem_insert_self a s)) this,
      hs (fun i hi ↦ h₁f i (mem_insert_of_mem hi))
        (fun i hi ↦ h₂f i (mem_insert_of_mem hi))]
Cleared hypotheses: s, h₁f, h₂f
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicOn (f i) U
h₂f : ∀ i ∈ s, ∀ z ∈ U, meromorphicOrderAt (f i) z ≠ ⊤
empty :
  ∀ (h₁f : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → MeromorphicOn (f i) U)
    (h₂f : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → ∀ z ∈ U, meromorphicOrderAt (f i) z ≠ ⊤),
    Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (E := 𝕜) (∏ i ∈ ∅, f i) U) (∑ i ∈ ∅, divisor (f i) U)
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (E := 𝕜) (∏ i ∈ s, f i) U) (∑ i ∈ s, divisor (f i) U)
have insert : ∀ (a : ι) (s : Finset ι) (ha : a ∉ s)
  (hs :
    ∀ (h₁f : ∀ i ∈ s, MeromorphicOn (f i) U) (h₂f : ∀ i ∈ s, ∀ z ∈ U, meromorphicOrderAt (f i) z ≠ ⊤),
      Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (E := 𝕜) (∏ i ∈ s, f i) U) (∑ i ∈ s, divisor (f i) U))
  (h₁f : ∀ i ∈ insert a s, MeromorphicOn (f i) U) (h₂f : ∀ i ∈ insert a s, ∀ z ∈ U, meromorphicOrderAt (f i) z ≠ ⊤),
  Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (E := 𝕜) (∏ i ∈ insert a s, f i) U)
    (∑ i ∈ insert a s, divisor (f i) U)
Tactic: classical
  induction s using Finset.induction with
  | empty =>
    rw [prod_empty, sum_empty]
    exact divisor_ofNat 1
  | insert a s ha hs =>
    have (z) (hz : z ∈ U) : meromorphicOrderAt (∏ i ∈ s, f i) z ≠ ⊤ := by
      simpa [meromorphicOrderAt_prod (fun i hi ↦ h₁f i (mem_insert_of_mem hi) z hz)]
        using fun i hi ↦ h₂f i (mem_insert_of_mem hi) z hz
    rw [prod_insert ha, sum_insert ha, divisor_mul (by aesop)
        (prod (fun i hi ↦ h₁f i (mem_insert_of_mem hi)))
        (h₂f a (mem_insert_self a s)) this,
      hs (fun i hi ↦ h₁f i (mem_insert_of_mem hi))
        (fun i hi ↦ h₂f i (mem_insert_of_mem hi))]
Cleared hypotheses: s, h₁f, h₂f
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
ι : Type u_3
s : Finset ι
f : ι → 𝕜 → 𝕜
h₁f : ∀ i ∈ s, MeromorphicOn (f i) U
h₂f : ∀ i ∈ s, ∀ z ∈ U, meromorphicOrderAt (f i) z ≠ ⊤
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (E := 𝕜) (fun (x : 𝕜) ↦ ∏ i ∈ s, f i x) U)
    (∑ i ∈ s, divisor (f i) U)
have h : ∀ (x : 𝕜), Eq.{u_1 + 1} (α := 𝕜) (∏ i ∈ s, f i x) ((∏ i ∈ s, f i) x)
Tactic: convert! divisor_prod h₁f h₂f
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor f⁻¹ U) (-divisor f U)
have h : ∀ (z : 𝕜), Eq (α := ℤ) ((divisor f⁻¹ U : (a : 𝕜) → ℤ) z : ℤ) ((-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 : 𝕜 → 𝕜
z : 𝕜
⊢ Eq (α := ℤ) ((divisor f⁻¹ U : (a : 𝕜) → ℤ) z : ℤ) ((-divisor f U : (a : 𝕜) → ℤ) z : ℤ)
have pos : ∀ (h : MeromorphicOn f U ∧ z ∈ U),
  Eq (α := ℤ) ((divisor f⁻¹ U : (a : 𝕜) → ℤ) z : ℤ) ((-divisor f U : (a : 𝕜) → ℤ) z : ℤ)
Tactic: by_cases h : MeromorphicOn f U ∧ z ∈ U
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.Divisor (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
z : 𝕜
pos :
  ∀ (h : MeromorphicOn f U ∧ z ∈ U),
    Eq (α := ℤ) ((divisor f⁻¹ U : (a : 𝕜) → ℤ) z : ℤ) ((-divisor f U : (a : 𝕜) → ℤ) z : ℤ)
⊢ Eq (α := ℤ) ((divisor f⁻¹ U : (a : 𝕜) → ℤ) z : ℤ) ((-divisor f U : (a : 𝕜) → ℤ) z : ℤ)
have neg : ∀ (h : ¬(MeromorphicOn f U ∧ z ∈ U)),
  Eq (α := ℤ) ((divisor f⁻¹ U : (a : 𝕜) → ℤ) z : ℤ) ((-divisor f U : (a : 𝕜) → ℤ) z : ℤ)
Tactic: by_cases h : MeromorphicOn f U ∧ z ∈ U