Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f : ∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₃f : (divisor f CB).support.Finite
g : ℂ → ℂ
h₁g : AnalyticOnNhd ℂ g (closedBall c |R|)
h₂g : ∀ (u : ↑(closedBall c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (closedBall c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (closedBall c |R|)) u) • g
⊢ ∑ᶠ (i : ℂ), (↑((divisor f CB) i) * log R - ↑((divisor f CB) i) * log ‖c - i‖) + log ‖meromorphicTrailingCoeffAt f c‖ =
    ∑ᶠ (u : ℂ), ↑((divisor f CB) u) * (log R - log ‖c - u‖) + log ‖meromorphicTrailingCoeffAt f c‖

pp: case hf
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f : ∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₃f : (divisor f CB).support.Finite
g : ℂ → ℂ
h₁g : AnalyticOnNhd ℂ g (closedBall c |R|)
h₂g : ∀ (u : ↑(closedBall c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (closedBall c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (closedBall c |R|)) u) • g
⊢ Function.HasFiniteSupport fun u ↦ ↑((divisor f CB) u) * log R

pp: case hg
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f : ∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₃f : (divisor f CB).support.Finite
g : ℂ → ℂ
h₁g : AnalyticOnNhd ℂ g (closedBall c |R|)
h₂g : ∀ (u : ↑(closedBall c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (closedBall c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (closedBall c |R|)) u) • g
⊢ Function.HasFiniteSupport fun u ↦ ↑((divisor f CB) u) * log ‖c - u‖

Tactic:
]

Goal state after:
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f : ∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₃f : (divisor f CB).support.Finite
g : ℂ → ℂ
h₁g : AnalyticOnNhd ℂ g (closedBall c |R|)
h₂g : ∀ (u : ↑(closedBall c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (closedBall c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (closedBall c |R|)) u) • g
⊢ ∑ᶠ (i : ℂ), (↑((divisor f CB) i) * log R - ↑((divisor f CB) i) * log ‖c - i‖) + log ‖meromorphicTrailingCoeffAt f c‖ =
    ∑ᶠ (u : ℂ), ↑((divisor f CB) u) * (log R - log ‖c - u‖) + log ‖meromorphicTrailingCoeffAt f c‖

case hf
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f : ∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₃f : (divisor f CB).support.Finite
g : ℂ → ℂ
h₁g : AnalyticOnNhd ℂ g (closedBall c |R|)
h₂g : ∀ (u : ↑(closedBall c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (closedBall c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (closedBall c |R|)) u) • g
⊢ Function.HasFiniteSupport fun u ↦ ↑((divisor f CB) u) * log R

case hg
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f : ∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₃f : (divisor f CB).support.Finite
g : ℂ → ℂ
h₁g : AnalyticOnNhd ℂ g (closedBall c |R|)
h₂g : ∀ (u : ↑(closedBall c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (closedBall c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (closedBall c |R|)) u) • g
⊢ Function.HasFiniteSupport fun u ↦ ↑((divisor f CB) u) * log ‖c - u‖