awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
this :
  (Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) ⊆
    (↑(Finite.toFinset (s := support d) h) : Set 𝕜)
⊢ Eq (α := 𝕜)
    (∏ n ∈ Finite.toFinset (s := support d) h,
      meromorphicTrailingCoeffAt (HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - n) (d n)) x)
    (∏ i ∈ Finite.toFinset (s := support d) h, (x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i)
have apply : ∀ x_1 ∈ Finite.toFinset (s := support d) h,
  meromorphicTrailingCoeffAt (HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - x_1) (d x_1)) x =
    (x - x_1) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 x_1
Tactic: apply Finset.prod_congr rfl
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
this :
  (Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) ⊆
    (↑(Finite.toFinset (s := support d) h) : Set 𝕜)
y : 𝕜
hy : y ∈ Finite.toFinset (s := support d) h
⊢ meromorphicTrailingCoeffAt (HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - y) (d y)) x =
    (x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y
have rw : HPow.hPow (α := 𝕜) (meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ x - y) x) (d y) =
  (x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y
Tactic: rw [MeromorphicAt.meromorphicTrailingCoeffAt_zpow (by fun_prop)]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
this :
  (Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) ⊆
    (↑(Finite.toFinset (s := support d) h) : Set 𝕜)
y : 𝕜
hy : y ∈ Finite.toFinset (s := support d) h
⊢ HPow.hPow (α := 𝕜) (meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ x - y) x) (d y) =
    (x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y
have pos : ∀ (hxy : x = y),
  HPow.hPow (α := 𝕜) (meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ x - y) x) (d y) =
    (x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y
Tactic: by_cases hxy : x = y
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
this :
  (Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) ⊆
    (↑(Finite.toFinset (s := support d) h) : Set 𝕜)
y : 𝕜
hy : y ∈ Finite.toFinset (s := support d) h
pos :
  ∀ (hxy : x = y),
    HPow.hPow (α := 𝕜) (meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ x - y) x) (d y) =
      (x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y
⊢ HPow.hPow (α := 𝕜) (meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ x - y) x) (d y) =
    (x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y
have neg : ∀ (hxy : ¬x = y),
  HPow.hPow (α := 𝕜) (meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ x - y) x) (d y) =
    (x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y
Tactic: by_cases hxy : x = y
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
this :
  (Function.mulSupport (M := 𝕜 → 𝕜) fun (u : 𝕜) ↦ HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) ⊆
    (↑(Finite.toFinset (s := support d) h) : Set 𝕜)
y : 𝕜
hy : y ∈ Finite.toFinset (s := support d) h
hxy : x = y
⊢ HPow.hPow (α := 𝕜) (meromorphicTrailingCoeffAt (fun (x : 𝕜) ↦ x - y) x) (d y) =
    (x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y
have pos : (if y = y then 1 else y - y) ^ d y = (y - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d y 0 y
Tactic: rw [hxy, meromorphicTrailingCoeffAt_id_sub_const]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h₁ : HasFiniteSupport d
h₂ : x ∉ support d
⊢ Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x)
    (∏ᶠ (u : 𝕜), (x - u) ^ d u)
have rw : Eq (α := 𝕜) (∏ i ∈ Finite.toFinset (s := support d) h₁, (x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i)
  (∏ᶠ (u : 𝕜), (x - u) ^ d u)
Tactic: rw [meromorphicTrailingCoeffAt_factorizedRational h₁,
    finprod_eq_prod_of_mulSupport_subset _ (mulSupport_update h₁)]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h₁ : HasFiniteSupport d
h₂ : x ∉ support d
u : 𝕜
⊢ Membership.mem (γ := Set 𝕜) (Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ d u) u →
    u ∈ (↑(Finite.toFinset (s := support d) h₁) : Set 𝕜)
have contrapose : u ∉ (↑(Finite.toFinset (s := support d) h₁) : Set 𝕜) → u ∉ Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ d u
Tactic: contrapose
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h₁ : HasFiniteSupport d
h₂ : x ∉ support d
⊢ Eq (α := 𝕜) (∏ i ∈ Finite.toFinset (s := support d) h₁, (x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i)
    (∏ᶠ (u : 𝕜), (x - u) ^ d u)
have this : (Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ d u) ⊆ (↑(Finite.toFinset (s := support d) h₁) : Set 𝕜)
Tactic: have : (fun u ↦ (x - u) ^ d u).mulSupport ⊆ h₁.toFinset := by
    intro u
    contrapose
    simp_all
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h₁ : HasFiniteSupport d
h₂ : x ∉ support d
this : (Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ d u) ⊆ (↑(Finite.toFinset (s := support d) h₁) : Set 𝕜)
⊢ Eq (α := 𝕜) (∏ i ∈ Finite.toFinset (s := support d) h₁, (x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i)
    (∏ᶠ (u : 𝕜), (x - u) ^ d u)
have rw : ∀ x_1 ∈ Finite.toFinset (s := support d) h₁, (x - x_1) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 x_1 = (x - x_1) ^ d x_1
Tactic: rw [finprod_eq_prod_of_mulSupport_subset _ this, Finset.prod_congr rfl]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h₁ : HasFiniteSupport d
h₂ : x ∉ support d
this : (Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ d u) ⊆ (↑(Finite.toFinset (s := support d) h₁) : Set 𝕜)
y : 𝕜
hy : y ∈ Finite.toFinset (s := support d) h₁
⊢ (x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y = (x - y) ^ d y
have e_a : update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y = d y
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h₁ : HasFiniteSupport d
h₂ : x ∉ support d
this : (Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ d u) ⊆ (↑(Finite.toFinset (s := support d) h₁) : Set 𝕜)
y : 𝕜
hy : y ∈ Finite.toFinset (s := support d) h₁
⊢ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y = d y
have e_a : y ≠ x
Tactic: apply Function.update_of_ne
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h₁ : HasFiniteSupport d
h₂ : x ∉ support d
⊢ Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x)
    (∏ᶠ (u : 𝕜), (x - u) ^ d u)
have rw : Eq.{u_1 + 1} (α := 𝕜) (∏ᶠ (u : 𝕜), (x - u) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 u) (∏ᶠ (u : 𝕜), (x - u) ^ d u)
Tactic: classical
  rw [meromorphicTrailingCoeffAt_factorizedRational h₁,
    finprod_eq_prod_of_mulSupport_subset _ (mulSupport_update h₁)]
  have : (fun u ↦ (x - u) ^ d u).mulSupport ⊆ h₁.toFinset := by
    intro u
    contrapose
    simp_all
  rw [finprod_eq_prod_of_mulSupport_subset _ this, Finset.prod_congr rfl]
  intro y hy
  congr
  apply Function.update_of_ne
  by_contra hCon
  simp_all
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h₁ : HasFiniteSupport d
h₂ : x ∉ support d
rw : Eq.{u_1 + 1} (α := 𝕜) (∏ᶠ (u : 𝕜), (x - u) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 u) (∏ᶠ (u : 𝕜), (x - u) ^ d u)
⊢ Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x)
    (∏ᶠ (u : 𝕜), (x - u) ^ d u)
have rw₁ : Eq (α := 𝕜) (∏ i ∈ Finite.toFinset (s := support d) h₁, (x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i)
  (∏ᶠ (u : 𝕜), (x - u) ^ d u)
Tactic: classical
  rw [meromorphicTrailingCoeffAt_factorizedRational h₁,
    finprod_eq_prod_of_mulSupport_subset _ (mulSupport_update h₁)]
  have : (fun u ↦ (x - u) ^ d u).mulSupport ⊆ h₁.toFinset := by
    intro u
    contrapose
    simp_all
  rw [finprod_eq_prod_of_mulSupport_subset _ this, Finset.prod_congr rfl]
  intro y hy
  congr
  apply Function.update_of_ne
  by_contra hCon
  simp_all
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h₁ : HasFiniteSupport d
h₂ : x ∉ support d
rw : Eq.{u_1 + 1} (α := 𝕜) (∏ᶠ (u : 𝕜), (x - u) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 u) (∏ᶠ (u : 𝕜), (x - u) ^ d u)
rw₁ rw₂ rw₃ :
  Eq (α := 𝕜) (∏ i ∈ Finite.toFinset (s := support d) h₁, (x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i)
    (∏ᶠ (u : 𝕜), (x - u) ^ d u)
⊢ Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x)
    (∏ᶠ (u : 𝕜), (x - u) ^ d u)
have rw₄ : ∀
  (this :
    (Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ d u) ⊆ (↑(Finite.toFinset (s := support d) h₁) : Set 𝕜)),
  Eq (α := 𝕜) (∏ i ∈ Finite.toFinset (s := support d) h₁, (x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i)
    (∏ᶠ (u : 𝕜), (x - u) ^ d u)
Tactic: classical
  rw [meromorphicTrailingCoeffAt_factorizedRational h₁,
    finprod_eq_prod_of_mulSupport_subset _ (mulSupport_update h₁)]
  have : (fun u ↦ (x - u) ^ d u).mulSupport ⊆ h₁.toFinset := by
    intro u
    contrapose
    simp_all
  rw [finprod_eq_prod_of_mulSupport_subset _ this, Finset.prod_congr rfl]
  intro y hy
  congr
  apply Function.update_of_ne
  by_contra hCon
  simp_all
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h₁ : HasFiniteSupport d
h₂ : x ∉ support d
rw : Eq.{u_1 + 1} (α := 𝕜) (∏ᶠ (u : 𝕜), (x - u) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 u) (∏ᶠ (u : 𝕜), (x - u) ^ d u)
rw₁ rw₂ rw₃ :
  Eq (α := 𝕜) (∏ i ∈ Finite.toFinset (s := support d) h₁, (x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i)
    (∏ᶠ (u : 𝕜), (x - u) ^ d u)
rw₄ :
  ∀
    (this :
      (Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ d u) ⊆ (↑(Finite.toFinset (s := support d) h₁) : Set 𝕜)),
    Eq (α := 𝕜) (∏ i ∈ Finite.toFinset (s := support d) h₁, (x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i)
      (∏ᶠ (u : 𝕜), (x - u) ^ d u)
⊢ Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x)
    (∏ᶠ (u : 𝕜), (x - u) ^ d u)
have rw₅ : ∀
  (this :
    (Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ d u) ⊆ (↑(Finite.toFinset (s := support d) h₁) : Set 𝕜)),
  ∀ x_1 ∈ Finite.toFinset (s := support d) h₁, (x - x_1) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 x_1 = (x - x_1) ^ d x_1
Tactic: classical
  rw [meromorphicTrailingCoeffAt_factorizedRational h₁,
    finprod_eq_prod_of_mulSupport_subset _ (mulSupport_update h₁)]
  have : (fun u ↦ (x - u) ^ d u).mulSupport ⊆ h₁.toFinset := by
    intro u
    contrapose
    simp_all
  rw [finprod_eq_prod_of_mulSupport_subset _ this, Finset.prod_congr rfl]
  intro y hy
  congr
  apply Function.update_of_ne
  by_contra hCon
  simp_all
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h₁ : HasFiniteSupport d
h₂ : x ∉ support d
rw : Eq.{u_1 + 1} (α := 𝕜) (∏ᶠ (u : 𝕜), (x - u) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 u) (∏ᶠ (u : 𝕜), (x - u) ^ d u)
rw₁ rw₂ rw₃ :
  Eq (α := 𝕜) (∏ i ∈ Finite.toFinset (s := support d) h₁, (x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i)
    (∏ᶠ (u : 𝕜), (x - u) ^ d u)
rw₄ :
  ∀
    (this :
      (Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ d u) ⊆ (↑(Finite.toFinset (s := support d) h₁) : Set 𝕜)),
    Eq (α := 𝕜) (∏ i ∈ Finite.toFinset (s := support d) h₁, (x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i)
      (∏ᶠ (u : 𝕜), (x - u) ^ d u)
rw₅ rw₆ :
  ∀
    (this :
      (Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ d u) ⊆ (↑(Finite.toFinset (s := support d) h₁) : Set 𝕜))
    (y : 𝕜) (hy : y ∈ Finite.toFinset (s := support d) h₁),
    (x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y = (x - y) ^ d y
⊢ Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x)
    (∏ᶠ (u : 𝕜), (x - u) ^ d u)
have e_a : ∀ (this : (Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ d u) ⊆ (↑(Finite.toFinset (s := support d) h₁) : Set 𝕜))
  (y : 𝕜) (hy : y ∈ Finite.toFinset (s := support d) h₁), update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y = d y
Tactic: classical
  rw [meromorphicTrailingCoeffAt_factorizedRational h₁,
    finprod_eq_prod_of_mulSupport_subset _ (mulSupport_update h₁)]
  have : (fun u ↦ (x - u) ^ d u).mulSupport ⊆ h₁.toFinset := by
    intro u
    contrapose
    simp_all
  rw [finprod_eq_prod_of_mulSupport_subset _ this, Finset.prod_congr rfl]
  intro y hy
  congr
  apply Function.update_of_ne
  by_contra hCon
  simp_all
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h₁ : HasFiniteSupport d
h₂ : x ∉ support d
rw : Eq.{u_1 + 1} (α := 𝕜) (∏ᶠ (u : 𝕜), (x - u) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 u) (∏ᶠ (u : 𝕜), (x - u) ^ d u)
rw₁ rw₂ rw₃ :
  Eq (α := 𝕜) (∏ i ∈ Finite.toFinset (s := support d) h₁, (x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i)
    (∏ᶠ (u : 𝕜), (x - u) ^ d u)
rw₄ :
  ∀
    (this :
      (Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ d u) ⊆ (↑(Finite.toFinset (s := support d) h₁) : Set 𝕜)),
    Eq (α := 𝕜) (∏ i ∈ Finite.toFinset (s := support d) h₁, (x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i)
      (∏ᶠ (u : 𝕜), (x - u) ^ d u)
rw₅ rw₆ :
  ∀
    (this :
      (Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ d u) ⊆ (↑(Finite.toFinset (s := support d) h₁) : Set 𝕜))
    (y : 𝕜) (hy : y ∈ Finite.toFinset (s := support d) h₁),
    (x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y = (x - y) ^ d y
e_a :
  ∀
    (this :
      (Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ d u) ⊆ (↑(Finite.toFinset (s := support d) h₁) : Set 𝕜))
    (y : 𝕜) (hy : y ∈ Finite.toFinset (s := support d) h₁), update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y = d y
⊢ Eq (α := 𝕜) (meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x)
    (∏ᶠ (u : 𝕜), (x - u) ^ d u)
have e_a₁ : ∀ (this : (Function.mulSupport (M := 𝕜) fun (u : 𝕜) ↦ (x - u) ^ d u) ⊆ (↑(Finite.toFinset (s := support d) h₁) : Set 𝕜))
  (y : 𝕜) (hy : y ∈ Finite.toFinset (s := support d) h₁), y ≠ x
Tactic: classical
  rw [meromorphicTrailingCoeffAt_factorizedRational h₁,
    finprod_eq_prod_of_mulSupport_subset _ (mulSupport_update h₁)]
  have : (fun u ↦ (x - u) ^ d u).mulSupport ⊆ h₁.toFinset := by
    intro u
    contrapose
    simp_all
  rw [finprod_eq_prod_of_mulSupport_subset _ this, Finset.prod_congr rfl]
  intro y hy
  congr
  apply Function.update_of_ne
  by_contra hCon
  simp_all
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
⊢ log
      (Norm.norm (E := 𝕜)
        (meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x)) =
    ∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖
have rw : log (Norm.norm (E := 𝕜) (∏ i ∈ Finite.toFinset (s := support d) h, (x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i)) =
  ∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖
Tactic: rw [meromorphicTrailingCoeffAt_factorizedRational h,
    finprod_eq_prod_of_mulSupport_subset _ (mulSupport_update h)]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
y : 𝕜
h_1 : y ∈ Finite.toFinset (s := support d) h
⊢ ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0
have pos : ∀ (h : x = y), ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0
Tactic: by_cases h : x = y
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
y : 𝕜
h_1 : y ∈ Finite.toFinset (s := support d) h
pos : ∀ (h : x = y), ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0
⊢ ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0
have neg : ∀ (h : ¬x = y), ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0
Tactic: by_cases h : x = y
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h_1 : HasFiniteSupport d
y : 𝕜
h_2 : y ∈ Finite.toFinset (s := support d) h_1
h : x = y
⊢ ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0
have pos : ‖(y - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d y 0 y‖ ≠ 0
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
⊢ log (Norm.norm (E := 𝕜) (∏ i ∈ Finite.toFinset (s := support d) h, (x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i)) =
    ∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖
have this : ∀ y ∈ Finite.toFinset (s := support d) h, ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0
Tactic: have : ∀ y ∈ h.toFinset, ‖(x - y) ^ update d x 0 y‖ ≠ 0 := by
    intro y _
    by_cases h : x = y
    · rw [h]
      simp_all
    · simp_all [zpow_ne_zero, sub_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
this : ∀ y ∈ Finite.toFinset (s := support d) h, ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0
⊢ log (Norm.norm (E := 𝕜) (∏ i ∈ Finite.toFinset (s := support d) h, (x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i)) =
    ∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖
have rw : Eq (α := ℝ) (∑ i ∈ Finite.toFinset (s := support d) h, log ‖(x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i‖)
  (∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖)
Tactic: rw [norm_prod, log_prod this]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
this : ∀ y ∈ Finite.toFinset (s := support d) h, ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0
u : 𝕜
⊢ Membership.mem (γ := Set 𝕜) (support (M := ℝ) fun (u : 𝕜) ↦ (↑(d u) : ℝ) * log ‖x - u‖) u →
    u ∈ (↑(Finite.toFinset (s := support d) h) : Set 𝕜)
have contrapose : u ∉ (↑(Finite.toFinset (s := support d) h) : Set 𝕜) → u ∉ support (M := ℝ) fun (u : 𝕜) ↦ (↑(d u) : ℝ) * log ‖x - u‖
Tactic: contrapose
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
this : ∀ y ∈ Finite.toFinset (s := support d) h, ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0
⊢ Eq (α := ℝ) (∑ i ∈ Finite.toFinset (s := support d) h, log ‖(x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i‖)
    (∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖)
have this₁ : (support (M := ℝ) fun (u : 𝕜) ↦ (↑(d u) : ℝ) * log ‖x - u‖) ⊆ (↑(Finite.toFinset (s := support d) h) : Set 𝕜)
Tactic: have : (fun u ↦ (d u) * log ‖x - u‖).support ⊆ h.toFinset := by
    intro u
    contrapose
    simp_all
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
this_1 : ∀ y ∈ Finite.toFinset (s := support d) h, ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0
this : (support (M := ℝ) fun (u : 𝕜) ↦ (↑(d u) : ℝ) * log ‖x - u‖) ⊆ (↑(Finite.toFinset (s := support d) h) : Set 𝕜)
⊢ Eq (α := ℝ) (∑ i ∈ Finite.toFinset (s := support d) h, log ‖(x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i‖)
    (∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖)
have rw : Eq (α := ℝ) (∑ i ∈ Finite.toFinset (s := support d) h, log ‖(x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i‖)
  (∑ i ∈ Finite.toFinset (s := support d) h, (↑(d i) : ℝ) * log ‖x - i‖)
Tactic: rw [finsum_eq_sum_of_support_subset _ this]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
this_1 : ∀ y ∈ Finite.toFinset (s := support d) h, ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0
this : (support (M := ℝ) fun (u : 𝕜) ↦ (↑(d u) : ℝ) * log ‖x - u‖) ⊆ (↑(Finite.toFinset (s := support d) h) : Set 𝕜)
⊢ Eq (α := ℝ) (∑ i ∈ Finite.toFinset (s := support d) h, log ‖(x - i) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 i‖)
    (∑ i ∈ Finite.toFinset (s := support d) h, (↑(d i) : ℝ) * log ‖x - i‖)
have apply : ∀ x_1 ∈ Finite.toFinset (s := support d) h,
  log ‖(x - x_1) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 x_1‖ = (↑(d x_1) : ℝ) * log ‖x - x_1‖
Tactic: apply Finset.sum_congr rfl
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
this_1 : ∀ y ∈ Finite.toFinset (s := support d) h, ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0
this : (support (M := ℝ) fun (u : 𝕜) ↦ (↑(d u) : ℝ) * log ‖x - u‖) ⊆ (↑(Finite.toFinset (s := support d) h) : Set 𝕜)
y : 𝕜
hy : y ∈ Finite.toFinset (s := support d) h
⊢ log ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ = (↑(d y) : ℝ) * log ‖x - y‖
have rw : (↑(update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y) : ℝ) * log ‖x - y‖ = (↑(d y) : ℝ) * log ‖x - y‖
Tactic: rw [norm_zpow, Real.log_zpow]
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
this_1 : ∀ y ∈ Finite.toFinset (s := support d) h, ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0
this : (support (M := ℝ) fun (u : 𝕜) ↦ (↑(d u) : ℝ) * log ‖x - u‖) ⊆ (↑(Finite.toFinset (s := support d) h) : Set 𝕜)
y : 𝕜
hy : y ∈ Finite.toFinset (s := support d) h
⊢ (↑(update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y) : ℝ) * log ‖x - y‖ = (↑(d y) : ℝ) * log ‖x - y‖
have pos : ∀ (h : x = y), (↑(update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y) : ℝ) * log ‖x - y‖ = (↑(d y) : ℝ) * log ‖x - y‖
Tactic: by_cases h : x = y
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
this_1 : ∀ y ∈ Finite.toFinset (s := support d) h, ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0
this : (support (M := ℝ) fun (u : 𝕜) ↦ (↑(d u) : ℝ) * log ‖x - u‖) ⊆ (↑(Finite.toFinset (s := support d) h) : Set 𝕜)
y : 𝕜
hy : y ∈ Finite.toFinset (s := support d) h
pos : ∀ (h : x = y), (↑(update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y) : ℝ) * log ‖x - y‖ = (↑(d y) : ℝ) * log ‖x - y‖
⊢ (↑(update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y) : ℝ) * log ‖x - y‖ = (↑(d y) : ℝ) * log ‖x - y‖
have neg : ∀ (h : ¬x = y), (↑(update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y) : ℝ) * log ‖x - y‖ = (↑(d y) : ℝ) * log ‖x - y‖
Tactic: by_cases h : x = y
-- Lean 4 proof step from Mathlib.Analysis.Meromorphic.FactorizedRational (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h_1 : HasFiniteSupport d
this_1 : ∀ y ∈ Finite.toFinset (s := support d) h_1, ‖(x - y) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y‖ ≠ 0
this : (support (M := ℝ) fun (u : 𝕜) ↦ (↑(d u) : ℝ) * log ‖x - u‖) ⊆ (↑(Finite.toFinset (s := support d) h_1) : Set 𝕜)
y : 𝕜
hy : y ∈ Finite.toFinset (s := support d) h_1
h : ¬x = y
⊢ (↑(update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y) : ℝ) * log ‖x - y‖ = (↑(d y) : ℝ) * log ‖x - y‖
have neg : (↑(d y) : ℝ) * log ‖x - y‖ = (↑(d y) : ℝ) * log ‖x - y‖
Tactic: rw [Function.update_of_ne (by tauto)]