awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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
⊢ meromorphicOrderAt f₂ z ≠ ⊤

Tactic:
(h₂f₂ z hz)
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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
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 : ℤ)
⊢ 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₂

Premises used: meromorphicOrderAt
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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
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:
simp [h₁f₁, h₁f₂, h₁f₁.smul h₁f₂, hz, meromorphicOrderAt_smul (h₁f₁ z hz) (h₁f₂ z hz),
      ← ha₁, ← ha₂, ← WithTop.coe_add]

Premises used: meromorphicOrderAt_smul, MeromorphicOn.smul, WithTop.coe_add
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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 : ℤ)

Tactic:
simp [hz]
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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.{u_1, u_2} (E := E) (fun (z : 𝕜) ↦ f₁ z • f₂ z) U =
    HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U) (divisor f₂ U)

Tactic:
divisor_smul h₁f₁ h₁f₂ h₂f₁ h₂f₂

Premises used: MeromorphicOn.divisor_smul
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f₁ f₂ : 𝕜 → 𝕜
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)

Tactic:
divisor_smul h₁f₁ h₁f₂ h₂f₁ h₂f₂

Premises used: MeromorphicOn.divisor_smul
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f₁ f₂ : 𝕜 → 𝕜
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 (E := 𝕜) (fun (z : 𝕜) ↦ f₁ z * f₂ z) U =
    HAdd.hAdd (α := Function.locallyFinsuppWithin U ℤ) (divisor f₁ U) (divisor f₂ U)

Tactic:
divisor_smul h₁f₁ h₁f₂ h₂f₁ h₂f₂

Premises used: MeromorphicOn.divisor_smul
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
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 := 𝕜) 1 U) 0

Tactic:
divisor_ofNat 1

Premises used: MeromorphicOn.divisor_ofNat, OfNat.ofNat
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
ι : Type u_3
f : ι → 𝕜 → 𝕜
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 := 𝕜) 1 U) 0

Tactic:
exact divisor_ofNat 1

Premises used: MeromorphicOn.divisor_ofNat, OfNat.ofNat
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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 ≠ ⊤
z : 𝕜
hz : z ∈ U
⊢ meromorphicOrderAt (E := 𝕜) (∏ i ∈ s, f i) z ≠ ⊤

Tactic:
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

Premises used: Finset.mem_insert_of_mem, meromorphicOrderAt_prod
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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 ≠ ⊤
⊢ ∀ (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
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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 ≠ ⊤
⊢ MeromorphicOn (f a) U

Tactic:
aesop
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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)
insert₃ 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)
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (E := 𝕜) (∏ i ∈ Insert.insert a s, f i) U)
    (∑ i ∈ Insert.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))]

Premises used: Finset.prod_insert, Finset.mem_insert_self, MeromorphicOn.prod, Finset.mem_insert_of_mem, Finset.sum_insert, MeromorphicOn.divisor_mul
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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)
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.insert a s, MeromorphicOn (f i) U)
    (h₂f : ∀ i ∈ Insert.insert a s, ∀ z ∈ U, meromorphicOrderAt (f i) z ≠ ⊤),
    Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (E := 𝕜) (∏ i ∈ Insert.insert a s, f i) U)
      (∑ i ∈ Insert.insert a s, divisor (f i) U)
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (E := 𝕜) (∏ i ∈ s, f i) U) (∑ i ∈ 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))]

Premises used: Finset.prod_empty, Insert.insert, MeromorphicOn.divisor_ofNat, Finset.sum_empty, OfNat.ofNat
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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)
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.insert a s, MeromorphicOn (f i) U)
    (h₂f : ∀ i ∈ Insert.insert a s, ∀ z ∈ U, meromorphicOrderAt (f i) z ≠ ⊤),
    Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (E := 𝕜) (∏ i ∈ Insert.insert a s, f i) U)
      (∑ i ∈ Insert.insert a s, divisor (f i) U)
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (E := 𝕜) (∏ i ∈ s, f i) U) (∑ i ∈ 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))]

Premises used: Finset.prod_empty, Insert.insert, MeromorphicOn.divisor_ofNat, Finset.sum_empty, OfNat.ofNat
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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)

Tactic:
divisor_prod h₁f h₂f

Premises used: MeromorphicOn.divisor_prod
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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 ≠ ⊤
h : ∀ (x : 𝕜), Eq.{u_1 + 1} (α := 𝕜) (∏ i ∈ s, f i x) ((∏ i ∈ s, f i) x)
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (E := 𝕜) (fun (x : 𝕜) ↦ ∏ i ∈ s, f i x) U)
    (∑ i ∈ s, divisor (f i) U)

Tactic:
convert! divisor_prod h₁f h₂f

Premises used: MeromorphicOn.divisor_prod
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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 ≠ ⊤
x : 𝕜
⊢ Eq.{u_1 + 1} (α := 𝕜) (∏ i ∈ s, f i x) ((∏ i ∈ s, f i) x)

Tactic:
(Finset.prod_apply _ s f).symm

Premises used: Finset.prod_apply, Eq.symm
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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 ≠ ⊤
x : 𝕜
⊢ Eq.{u_1 + 1} (α := 𝕜) (∏ i ∈ s, f i x) ((∏ i ∈ s, f i) x)

Tactic:
exact (Finset.prod_apply _ s f).symm

Premises used: Finset.prod_apply, Eq.symm
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
h : ∀ (z : 𝕜), Eq (α := ℤ) ((divisor f⁻¹ U : (a : 𝕜) → ℤ) z : ℤ) ((-divisor f U : (a : 𝕜) → ℤ) z : ℤ)
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor f⁻¹ U) (-divisor f U)

Tactic:
ext z
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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 : ℤ)
neg :
  ∀ (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 : ℤ)

Tactic:
by_cases h : MeromorphicOn f U ∧ z ∈ U

Premises used: MeromorphicOn
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
z : 𝕜
h : MeromorphicOn f U ∧ z ∈ U
⊢ Eq (α := ℤ) ((divisor f⁻¹ U : (a : 𝕜) → ℤ) z : ℤ) ((-divisor f U : (a : 𝕜) → ℤ) z : ℤ)

Tactic:
simp [divisor_apply, h, meromorphicOrderAt_inv]

Premises used: meromorphicOrderAt_inv, MeromorphicOn.divisor_apply
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
z : 𝕜
h : ¬(MeromorphicOn f U ∧ z ∈ U)
⊢ Eq (α := ℤ) ((divisor f⁻¹ U : (a : 𝕜) → ℤ) z : ℤ) ((-divisor f U : (a : 𝕜) → ℤ) z : ℤ)

Tactic:
simp [divisor_def, h]

Premises used: MeromorphicOn.divisor_def
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
⊢ Eq (α := Function.locallyFinsuppWithin U ℤ) (divisor (E := 𝕜) (fun (z : 𝕜) ↦ (f z)⁻¹) U) (-divisor f U)

Tactic:
divisor_inv

Premises used: MeromorphicOn.divisor_inv
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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)

Tactic:
ext z
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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 : ℤ)
neg :
  ∀ (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 : ℤ)

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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 : ℤ)

Tactic:
simp [hn]
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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 : ℤ)
neg :
  ∀ (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 : ℤ)

Tactic:
by_cases hz : z ∈ U
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicOn f U
n : ℕ
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:
simp [hf.pow, divisor_apply, meromorphicOrderAt_pow (hf z hz), hf, hz]

Premises used: MeromorphicOn.divisor_apply, meromorphicOrderAt_pow, MeromorphicOn.pow
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicOn f U
n : ℕ
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:
simp [hz]
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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 : ℤ)
neg₂ 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 : ℤ)
⊢ divisor (f ^ n) U = HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U)

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]

Premises used: MeromorphicOn.divisor_apply, MeromorphicOn.pow
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicOn f U
n : ℕ
⊢ divisor (E := 𝕜) (fun (z : 𝕜) ↦ f z ^ n) U = HSMul.hSMul (β := Function.locallyFinsuppWithin U ℤ) n (divisor f U)

Tactic:
divisor_pow hf n

Premises used: MeromorphicOn.divisor_pow
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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)

Tactic:
ext z
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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 : ℤ)
neg :
  ∀ (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 : ℤ)

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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 : ℤ)

Tactic:
simp [hn]
-- Module: Mathlib.Analysis.Meromorphic.Divisor
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 : ℤ)
neg :
  ∀ (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 : ℤ)

Tactic:
by_cases hz : z ∈ U
-- Module: Mathlib.Analysis.Meromorphic.Divisor
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
U : Set 𝕜
f : 𝕜 → 𝕜
hf : MeromorphicOn f U
n : ℤ
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:
simp [hf.zpow, divisor_apply, meromorphicOrderAt_zpow (hf z hz), hf, hz]

Premises used: MeromorphicOn.divisor_apply, MeromorphicOn.zpow, meromorphicOrderAt_zpow