-- Module: Mathlib.Analysis.Meromorphic.FactorizedRational
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
d : 𝕜 → ℤ
x : 𝕜
h : HasFiniteSupport d
rw :
  log (Norm.norm.{u_1} (E := 𝕜) (∏ᶠ (u : 𝕜), (x - u) ^ update (β := fun (a : 𝕜) ↦ ℤ) d x 0 u)) =
    ∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖
rw₁ rw₂ 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‖
rw₄ :
  ∀ (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‖
rw₅ :
  ∀ (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‖)
rw₆ :
  ∀ (this : ∀ 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‖)
rw₇ :
  ∀ (this : ∀ 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‖)
rw₈ rw₉ :
  ∀ (this : ∀ 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‖
rw₁₀ :
  ∀ (this : ∀ 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‖
pos :
  ∀ (this : ∀ 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) (h : x = y),
    (↑(update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y) : ℝ) * log ‖x - y‖ = (↑(d y) : ℝ) * log ‖x - y‖
neg neg₁ :
  ∀ (this : ∀ 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) (h : ¬x = y),
    (↑(update (β := fun (a : 𝕜) ↦ ℤ) d x 0 y) : ℝ) * log ‖x - y‖ = (↑(d y) : ℝ) * log ‖x - y‖
⊢ log
      (Norm.norm (E := 𝕜)
        (meromorphicTrailingCoeffAt (∏ᶠ (u : 𝕜), HPow.hPow (α := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ x - u) (d u)) x)) =
    ∑ᶠ (u : 𝕜), (↑(d u) : ℝ) * log ‖x - u‖

Tactic:
classical
  rw [meromorphicTrailingCoeffAt_factorizedRational h,
    finprod_eq_prod_of_mulSupport_subset _ (mulSupport_update h)]
  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]
  rw [norm_prod, log_prod this]
  have : (fun u ↦ (d u) * log ‖x - u‖).support ⊆ h.toFinset := by
    intro u
    contrapose
    simp_all
  rw [finsum_eq_sum_of_support_subset _ this]
  apply Finset.sum_congr rfl
  intro y hy
  rw [norm_zpow, Real.log_zpow]
  by_cases h : x = y
  · simp [h]
  · rw [Function.update_of_ne (by tauto)]

Premises used: _private.0.Function.FactorizedRational.mulSupport_update, Real.log_zpow, norm_prod, Function.FactorizedRational.meromorphicTrailingCoeffAt_factorizedRational, norm_zpow, Finset.sum_congr, finprod_eq_prod_of_mulSupport_subset, rfl, Function.update_of_ne