awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
α : Type u_3
s : Finset α
f : α → 𝕜 → E
h₁f : ∀ a ∈ s, Meromorphic (f a)
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 1 ≤ x) x} x →
          Membership.mem (γ := Set ℝ)
            {x : ℝ |
              (fun (x : ℝ) ↦
                  logCounting.{u_1, u_2} (𝕜 := 𝕜) (E := E) (∑ a ∈ s, f a) ⊤ x ≤ (∑ a ∈ s, logCounting (f a) ⊤) x)
                x}
            x}
      a
⊢ logCounting.{u_1, u_2} (𝕜 := 𝕜) (E := E) (∑ a ∈ s, f a) ⊤ ≤ᶠ[atTop] ∑ a ∈ s, logCounting (f a) ⊤
have h₁ : ∀ (a : ℝ), 1 ≤ a → logCounting.{u_1, u_2} (𝕜 := 𝕜) (E := E) (∑ a ∈ s, f a) ⊤ a ≤ (∑ a ∈ s, logCounting (f a) ⊤) a
Tactic: filter_upwards [eventually_ge_atTop 1] using fun _ hr ↦ logCounting_sum_top_le s f h₁f hr
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
f₁ f₂ : 𝕜 → 𝕜
r : ℝ
hr : 1 ≤ r
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤
⊢ logCounting (f₁ * f₂) 0 r ≤ (logCounting f₁ 0 + logCounting f₂ 0) r
have simp : (locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
    (divisor (E := 𝕜) (fun (x : 𝕜) ↦ (f₁ * f₂) x) univ)⁺ r ≤
  HAdd.hAdd (α := ℝ → ℝ) (β := ℝ → ℝ)
    ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
        (divisor (E := 𝕜) (fun (x : 𝕜) ↦ f₁ x) univ)⁺ :
      ℝ → ℝ)
    ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
        (divisor (E := 𝕜) (fun (x : 𝕜) ↦ f₂ x) univ)⁺ :
      ℝ → ℝ)
    r
Tactic: simp only [logCounting, WithTop.zero_ne_top, reduceDIte, WithTop.untop₀_zero, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
f₁ f₂ : 𝕜 → 𝕜
r : ℝ
hr : 1 ≤ r
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤
⊢ (locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
      (divisor (E := 𝕜) (fun (x : 𝕜) ↦ (f₁ * f₂) x) univ)⁺ r ≤
    HAdd.hAdd (α := ℝ → ℝ) (β := ℝ → ℝ)
      ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
          (divisor (E := 𝕜) (fun (x : 𝕜) ↦ f₁ x) univ)⁺ :
        ℝ → ℝ)
      ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
          (divisor (E := 𝕜) (fun (x : 𝕜) ↦ f₂ x) univ)⁺ :
        ℝ → ℝ)
      r
have rw : LE.le (α := ℝ)
  ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
      (HAdd.hAdd (α := locallyFinsuppWithin (X := 𝕜) univ ℤ) (divisor f₁ univ) (divisor f₂ univ))⁺ r :
    ℝ)
  ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
      (HAdd.hAdd (α := locallyFinsupp 𝕜 ℤ) (divisor (E := 𝕜) (fun (x : 𝕜) ↦ f₁ x) univ)⁺
        (divisor (E := 𝕜) (fun (x : 𝕜) ↦ f₂ x) univ)⁺)
      r :
    ℝ)
Tactic: rw [divisor_mul h₁f₁.meromorphicOn h₁f₂.meromorphicOn (fun z _ ↦ h₂f₁ z) (fun z _ ↦ h₂f₂ z),
    ← locallyFinsuppWithin.logCounting.map_add]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
f₁ f₂ : 𝕜 → 𝕜
r : ℝ
hr : 1 ≤ r
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤
⊢ LE.le (α := ℝ)
    ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
        (HAdd.hAdd (α := locallyFinsuppWithin (X := 𝕜) univ ℤ) (divisor f₁ univ) (divisor f₂ univ))⁺ r :
      ℝ)
    ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
        (HAdd.hAdd (α := locallyFinsupp 𝕜 ℤ) (divisor (E := 𝕜) (fun (x : 𝕜) ↦ f₁ x) univ)⁺
          (divisor (E := 𝕜) (fun (x : 𝕜) ↦ f₂ x) univ)⁺)
        r :
      ℝ)
have apply : (HAdd.hAdd (α := locallyFinsuppWithin (X := 𝕜) univ ℤ) (divisor f₁ univ) (divisor f₂ univ))⁺ ≤
  HAdd.hAdd (α := locallyFinsupp 𝕜 ℤ) (divisor (E := 𝕜) (fun (x : 𝕜) ↦ f₁ x) univ)⁺
    (divisor (E := 𝕜) (fun (x : 𝕜) ↦ f₂ x) univ)⁺
Tactic: apply locallyFinsuppWithin.logCounting_le _ hr
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
f₁ f₂ : 𝕜 → 𝕜
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤
⊢ logCounting (f₁ * f₂) 0 ≤ᶠ[atTop] logCounting f₁ 0 + logCounting f₂ 0
have h : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ)
    {x : ℝ |
      Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 1 ≤ x) x} x →
        Membership.mem (γ := Set ℝ)
          {x : ℝ | (fun (x : ℝ) ↦ logCounting (f₁ * f₂) 0 x ≤ (logCounting f₁ 0 + logCounting f₂ 0) x) x} x}
    a
Tactic: filter_upwards [eventually_ge_atTop 1] using
    fun _ hr ↦ logCounting_mul_zero_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
f₁ f₂ : 𝕜 → 𝕜
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 1 ≤ x) x} x →
          Membership.mem (γ := Set ℝ)
            {x : ℝ | (fun (x : ℝ) ↦ logCounting (f₁ * f₂) 0 x ≤ (logCounting f₁ 0 + logCounting f₂ 0) x) x} x}
      a
⊢ logCounting (f₁ * f₂) 0 ≤ᶠ[atTop] logCounting f₁ 0 + logCounting f₂ 0
have h₁ : ∀ (a : ℝ), 1 ≤ a → logCounting (f₁ * f₂) 0 a ≤ (logCounting f₁ 0 + logCounting f₂ 0) a
Tactic: filter_upwards [eventually_ge_atTop 1] using
    fun _ hr ↦ logCounting_mul_zero_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
f₁ f₂ : 𝕜 → 𝕜
r : ℝ
hr : 1 ≤ r
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤
⊢ (locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ) (divisor (f₁ * f₂) univ)⁻ r ≤
    HAdd.hAdd (α := ℝ → ℝ) (β := ℝ → ℝ)
      ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ) (divisor f₁ univ)⁻ : ℝ → ℝ)
      ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ) (divisor f₂ univ)⁻ : ℝ → ℝ) r
have rw : LE.le (α := ℝ)
  ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
      (HAdd.hAdd (α := locallyFinsuppWithin (X := 𝕜) univ ℤ) (divisor f₁ univ) (divisor f₂ univ))⁻ r :
    ℝ)
  ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
      (HAdd.hAdd (α := locallyFinsupp 𝕜 ℤ) (divisor f₁ univ)⁻ (divisor f₂ univ)⁻) r :
    ℝ)
Tactic: rw [divisor_mul h₁f₁.meromorphicOn h₁f₂.meromorphicOn (fun z _ ↦ h₂f₁ z) (fun z _ ↦ h₂f₂ z),
    ← locallyFinsuppWithin.logCounting.map_add]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
f₁ f₂ : 𝕜 → 𝕜
r : ℝ
hr : 1 ≤ r
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤
⊢ LE.le (α := ℝ)
    ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
        (HAdd.hAdd (α := locallyFinsuppWithin (X := 𝕜) univ ℤ) (divisor f₁ univ) (divisor f₂ univ))⁻ r :
      ℝ)
    ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
        (HAdd.hAdd (α := locallyFinsupp 𝕜 ℤ) (divisor f₁ univ)⁻ (divisor f₂ univ)⁻) r :
      ℝ)
have apply : (HAdd.hAdd (α := locallyFinsuppWithin (X := 𝕜) univ ℤ) (divisor f₁ univ) (divisor f₂ univ))⁻ ≤
  HAdd.hAdd (α := locallyFinsupp 𝕜 ℤ) (divisor f₁ univ)⁻ (divisor f₂ univ)⁻
Tactic: apply locallyFinsuppWithin.logCounting_le _ hr
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
f₁ f₂ : 𝕜 → 𝕜
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤
⊢ logCounting (f₁ * f₂) ⊤ ≤ᶠ[atTop] logCounting f₁ ⊤ + logCounting f₂ ⊤
have h : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ)
    {x : ℝ |
      Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 1 ≤ x) x} x →
        Membership.mem (γ := Set ℝ)
          {x : ℝ | (fun (x : ℝ) ↦ logCounting (f₁ * f₂) ⊤ x ≤ (logCounting f₁ ⊤ + logCounting f₂ ⊤) x) x} x}
    a
Tactic: filter_upwards [eventually_ge_atTop 1] using
    fun _ hr ↦ logCounting_mul_top_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
f₁ f₂ : 𝕜 → 𝕜
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 1 ≤ x) x} x →
          Membership.mem (γ := Set ℝ)
            {x : ℝ | (fun (x : ℝ) ↦ logCounting (f₁ * f₂) ⊤ x ≤ (logCounting f₁ ⊤ + logCounting f₂ ⊤) x) x} x}
      a
⊢ logCounting (f₁ * f₂) ⊤ ≤ᶠ[atTop] logCounting f₁ ⊤ + logCounting f₂ ⊤
have h₁ : ∀ (a : ℝ), 1 ≤ a → logCounting (f₁ * f₂) ⊤ a ≤ (logCounting f₁ ⊤ + logCounting f₂ ⊤) a
Tactic: filter_upwards [eventually_ge_atTop 1] using
    fun _ hr ↦ logCounting_mul_top_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
R : ℝ
f : ℂ → ℂ
h : Meromorphic f
hR : R ≠ 0
⊢ MeromorphicOn f (closedBall 0 |R|)
have tauto : ∀ (x : ℂ), Membership.mem (γ := Set ℂ) (closedBall 0 |R|) x → MeromorphicAt f x
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (hypothesis)
Goal:
R : ℝ
f : ℂ → ℂ
h : Meromorphic f
hR : R ≠ 0
⊢ (logCounting : (a : locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f univ) R =
    circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R - log ‖meromorphicTrailingCoeffAt f 0‖
have h₁f : MeromorphicOn f (closedBall 0 |R|)
Tactic: have h₁f : MeromorphicOn f (closedBall 0 |R|) := by tauto
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
R : ℝ
f : ℂ → ℂ
h : Meromorphic f
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall 0 |R|)
⊢ (logCounting : (a : locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f univ) R =
    circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R - log ‖meromorphicTrailingCoeffAt f 0‖
have simp : ∑ᶠ (z : ℂ),
      (↑((((toClosedBall R : (a : locallyFinsupp ℂ ℤ) → locallyFinsuppWithin (closedBall 0 |R|) ℤ) (divisor f univ) :
                  locallyFinsuppWithin (X := ℂ) (closedBall 0 |R|) ℤ) :
                (a : ℂ) → ℤ)
              z) :
          ℝ) *
        log (R * ‖z‖⁻¹) +
    (↑((divisor f univ : (a : ℂ) → ℤ) 0) : ℝ) * log R =
  ∑ᶠ (u : ℂ), (↑((divisor f (closedBall 0 |R|) : (a : ℂ) → ℤ) u) : ℝ) * log (R * ‖u‖⁻¹) +
    (↑((divisor f (closedBall 0 |R|) : (a : ℂ) → ℤ) 0) : ℝ) * log R
Tactic: simp only [MeromorphicOn.circleAverage_log_norm hR h₁f, logCounting, AddMonoidHom.coe_mk,
    ZeroHom.coe_mk, zero_sub, norm_neg, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
R : ℝ
f : ℂ → ℂ
h : Meromorphic f
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall 0 |R|)
⊢ ∑ᶠ (z : ℂ),
        (↑((((toClosedBall R : (a : locallyFinsupp ℂ ℤ) → locallyFinsuppWithin (closedBall 0 |R|) ℤ) (divisor f univ) :
                    locallyFinsuppWithin (X := ℂ) (closedBall 0 |R|) ℤ) :
                  (a : ℂ) → ℤ)
                z) :
            ℝ) *
          log (R * ‖z‖⁻¹) +
      (↑((divisor f univ : (a : ℂ) → ℤ) 0) : ℝ) * log R =
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall 0 |R|) : (a : ℂ) → ℤ) u) : ℝ) * log (R * ‖u‖⁻¹) +
      (↑((divisor f (closedBall 0 |R|) : (a : ℂ) → ℤ) 0) : ℝ) * log R
have e_a : Eq (α := ℝ)
  (∑ᶠ (z : ℂ),
    (↑((((toClosedBall R : (a : locallyFinsupp ℂ ℤ) → locallyFinsuppWithin (closedBall 0 |R|) ℤ) (divisor f univ) :
                locallyFinsuppWithin (X := ℂ) (closedBall 0 |R|) ℤ) :
              (a : ℂ) → ℤ)
            z) :
        ℝ) *
      log (R * ‖z‖⁻¹))
  (∑ᶠ (u : ℂ), (↑((divisor f (closedBall 0 |R|) : (a : ℂ) → ℤ) u) : ℝ) * log (R * ‖u‖⁻¹))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
R : ℝ
f : ℂ → ℂ
h : Meromorphic f
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall 0 |R|)
e_a :
  Eq (α := ℝ)
    (∑ᶠ (z : ℂ),
      (↑((((toClosedBall R : (a : locallyFinsupp ℂ ℤ) → locallyFinsuppWithin (closedBall 0 |R|) ℤ) (divisor f univ) :
                  locallyFinsuppWithin (X := ℂ) (closedBall 0 |R|) ℤ) :
                (a : ℂ) → ℤ)
              z) :
          ℝ) *
        log (R * ‖z‖⁻¹))
    (∑ᶠ (u : ℂ), (↑((divisor f (closedBall 0 |R|) : (a : ℂ) → ℤ) u) : ℝ) * log (R * ‖u‖⁻¹))
⊢ ∑ᶠ (z : ℂ),
        (↑((((toClosedBall R : (a : locallyFinsupp ℂ ℤ) → locallyFinsuppWithin (closedBall 0 |R|) ℤ) (divisor f univ) :
                    locallyFinsuppWithin (X := ℂ) (closedBall 0 |R|) ℤ) :
                  (a : ℂ) → ℤ)
                z) :
            ℝ) *
          log (R * ‖z‖⁻¹) +
      (↑((divisor f univ : (a : ℂ) → ℤ) 0) : ℝ) * log R =
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall 0 |R|) : (a : ℂ) → ℤ) u) : ℝ) * log (R * ‖u‖⁻¹) +
      (↑((divisor f (closedBall 0 |R|) : (a : ℂ) → ℤ) 0) : ℝ) * log R
have e_a₁ : (↑((divisor f univ : (a : ℂ) → ℤ) 0) : ℝ) * log R = (↑((divisor f (closedBall 0 |R|) : (a : ℂ) → ℤ) 0) : ℝ) * log R
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
R : ℝ
f : ℂ → ℂ
h : Meromorphic f
hR : R ≠ 0
h₁f e_a : MeromorphicOn f (closedBall 0 |R|)
⊢ (↑((divisor f univ : (a : ℂ) → ℤ) 0) : ℝ) * log R = (↑((divisor f (closedBall 0 |R|) : (a : ℂ) → ℤ) 0) : ℝ) * log R
have e_a₁ : Membership.mem (γ := Set ℂ) (closedBall 0 |R|) 0
Tactic: rw [divisor_apply, divisor_apply]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
R : ℝ
f : ℂ → ℂ
h : Meromorphic f
hR : R ≠ 0
h₁f e_a : MeromorphicOn f (closedBall 0 |R|)
e_a₁ : Membership.mem (γ := Set ℂ) (closedBall 0 |R|) 0
⊢ (↑((divisor f univ : (a : ℂ) → ℤ) 0) : ℝ) * log R = (↑((divisor f (closedBall 0 |R|) : (a : ℂ) → ℤ) 0) : ℝ) * log R
have e_a₂ : MeromorphicOn f univ
Tactic: rw [divisor_apply, divisor_apply]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
R : ℝ
f : ℂ → ℂ
h : Meromorphic f
hR : R ≠ 0
h₁f e_a : MeromorphicOn f (closedBall 0 |R|)
e_a₁ : Membership.mem (γ := Set ℂ) (closedBall 0 |R|) 0
e_a₂ : MeromorphicOn f univ
⊢ (↑((divisor f univ : (a : ℂ) → ℤ) 0) : ℝ) * log R = (↑((divisor f (closedBall 0 |R|) : (a : ℂ) → ℤ) 0) : ℝ) * log R
have e_a₃ : Membership.mem (γ := Set ℂ) univ 0
Tactic: rw [divisor_apply, divisor_apply]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
R : ℝ
f : ℂ → ℂ
h : Meromorphic f
hR : R ≠ 0
⊢ (logCounting f 0 - logCounting f ⊤) R =
    circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R - log ‖meromorphicTrailingCoeffAt f 0‖
have rw : (locallyFinsuppWithin.logCounting : (a : locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f univ) R =
  circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R - log ‖meromorphicTrailingCoeffAt f 0‖
Tactic: rw [← locallyFinsuppWithin.logCounting_divisor]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
a₀ : E
⊢ ℝ → ℝ
have pos : (h : a = ⊤) → ℝ → ℝ
Tactic: by_cases h : a = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
a₀ : E
pos : (h : a = ⊤) → ℝ → ℝ
⊢ ℝ → ℝ
have neg : (h : ¬a = ⊤) → ℝ → ℝ
Tactic: by_cases h : a = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
r : ℝ
hfg : f =ᶠ[codiscreteWithin (sphere 0 |r|)] g
hr : r ≠ 0
⊢ proximity f a r = proximity g a r
have pos : ∀ (h : a = ⊤), proximity f a r = proximity g a r
Tactic: by_cases h : a = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
r : ℝ
hfg : f =ᶠ[codiscreteWithin (sphere 0 |r|)] g
hr : r ≠ 0
pos : ∀ (h : a = ⊤), proximity f a r = proximity g a r
⊢ proximity f a r = proximity g a r
have neg : ∀ (h : ¬a = ⊤), proximity f a r = proximity g a r
Tactic: by_cases h : a = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
r : ℝ
hfg : f =ᶠ[codiscreteWithin (sphere 0 |r|)] g
hr : r ≠ 0
h : a = ⊤
⊢ proximity f a r = proximity g a r
have pos : Eq (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f x‖) 0 r) (circleAverage (fun (x : ℂ) ↦ log⁺ ‖g x‖) 0 r)
Tactic: simp only [proximity, h, ↓reduceDIte]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
r : ℝ
hfg : f =ᶠ[codiscreteWithin (sphere 0 |r|)] g
hr : r ≠ 0
h : a = ⊤
⊢ Eq (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f x‖) 0 r) (circleAverage (fun (x : ℂ) ↦ log⁺ ‖g x‖) 0 r)
have apply : EventuallyEq (β := ℝ) (codiscreteWithin (sphere 0 |r|)) (fun (x : ℂ) ↦ log⁺ ‖f x‖) fun (x : ℂ) ↦ log⁺ ‖g x‖
Tactic: apply circleAverage_congr_codiscreteWithin _ hr
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
r : ℝ
hfg : f =ᶠ[codiscreteWithin (sphere 0 |r|)] g
hr : r ≠ 0
h : a = ⊤
⊢ EventuallyEq (β := ℝ) (codiscreteWithin (sphere 0 |r|)) (fun (x : ℂ) ↦ log⁺ ‖f x‖) fun (x : ℂ) ↦ log⁺ ‖g x‖
have h₁ : ∀ (a : ℂ),
  Membership.mem (γ := Set ℂ)
    {x : ℂ |
      Membership.mem (γ := Set ℂ) {x : ℂ | (fun (x : ℂ) ↦ f x = g x) x} x →
        Membership.mem (γ := Set ℂ)
          {x : ℂ | (fun (x : ℂ) ↦ Eq (α := ℝ) ((fun (x : ℂ) ↦ log⁺ ‖f x‖) x) ((fun (x : ℂ) ↦ log⁺ ‖g x‖) x)) x} x}
    a
Tactic: filter_upwards [hfg] using by aesop
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
r : ℝ
hfg : f =ᶠ[codiscreteWithin (sphere 0 |r|)] g
hr : r ≠ 0
h : a = ⊤
h₁ :
  ∀ (a : ℂ),
    Membership.mem (γ := Set ℂ)
      {x : ℂ |
        Membership.mem (γ := Set ℂ) {x : ℂ | (fun (x : ℂ) ↦ f x = g x) x} x →
          Membership.mem (γ := Set ℂ)
            {x : ℂ | (fun (x : ℂ) ↦ Eq (α := ℝ) ((fun (x : ℂ) ↦ log⁺ ‖f x‖) x) ((fun (x : ℂ) ↦ log⁺ ‖g x‖) x)) x} x}
      a
⊢ EventuallyEq (β := ℝ) (codiscreteWithin (sphere 0 |r|)) (fun (x : ℂ) ↦ log⁺ ‖f x‖) fun (x : ℂ) ↦ log⁺ ‖g x‖
have h₂ : ∀ (a : ℂ), f a = g a → log⁺ ‖f a‖ = log⁺ ‖g a‖
Tactic: filter_upwards [hfg] using by aesop
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
r : ℝ
hfg : f =ᶠ[codiscreteWithin (sphere 0 |r|)] g
hr : r ≠ 0
h : ¬a = ⊤
⊢ proximity f a r = proximity g a r
have neg : Eq (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f x - a.untop₀‖⁻¹) 0 r)
  (circleAverage (fun (x : ℂ) ↦ log⁺ ‖g x - a.untop₀‖⁻¹) 0 r)
Tactic: simp only [proximity, h, ↓reduceDIte]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
r : ℝ
hfg : f =ᶠ[codiscreteWithin (sphere 0 |r|)] g
hr : r ≠ 0
h : ¬a = ⊤
⊢ Eq (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f x - a.untop₀‖⁻¹) 0 r)
    (circleAverage (fun (x : ℂ) ↦ log⁺ ‖g x - a.untop₀‖⁻¹) 0 r)
have apply : EventuallyEq (β := ℝ) (codiscreteWithin (sphere 0 |r|)) (fun (x : ℂ) ↦ log⁺ ‖f x - a.untop₀‖⁻¹) fun (x : ℂ) ↦
  log⁺ ‖g x - a.untop₀‖⁻¹
Tactic: apply circleAverage_congr_codiscreteWithin _ hr
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
r : ℝ
hfg : f =ᶠ[codiscreteWithin (sphere 0 |r|)] g
hr : r ≠ 0
h : ¬a = ⊤
⊢ EventuallyEq (β := ℝ) (codiscreteWithin (sphere 0 |r|)) (fun (x : ℂ) ↦ log⁺ ‖f x - a.untop₀‖⁻¹) fun (x : ℂ) ↦
    log⁺ ‖g x - a.untop₀‖⁻¹
have h₁ : ∀ (a_1 : ℂ),
  Membership.mem (γ := Set ℂ)
    {x : ℂ |
      Membership.mem (γ := Set ℂ) {x : ℂ | (fun (x : ℂ) ↦ f x = g x) x} x →
        Membership.mem (γ := Set ℂ)
          {x : ℂ |
            (fun (x : ℂ) ↦
                Eq (α := ℝ) ((fun (x : ℂ) ↦ log⁺ ‖f x - a.untop₀‖⁻¹) x) ((fun (x : ℂ) ↦ log⁺ ‖g x - a.untop₀‖⁻¹) x))
              x}
          x}
    a_1
Tactic: filter_upwards [hfg] using by aesop
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
r : ℝ
hfg : f =ᶠ[codiscreteWithin (sphere 0 |r|)] g
hr : r ≠ 0
h : ¬a = ⊤
h₁ :
  ∀ (a_1 : ℂ),
    Membership.mem (γ := Set ℂ)
      {x : ℂ |
        Membership.mem (γ := Set ℂ) {x : ℂ | (fun (x : ℂ) ↦ f x = g x) x} x →
          Membership.mem (γ := Set ℂ)
            {x : ℂ |
              (fun (x : ℂ) ↦
                  Eq (α := ℝ) ((fun (x : ℂ) ↦ log⁺ ‖f x - a.untop₀‖⁻¹) x) ((fun (x : ℂ) ↦ log⁺ ‖g x - a.untop₀‖⁻¹) x))
                x}
            x}
      a_1
⊢ EventuallyEq (β := ℝ) (codiscreteWithin (sphere 0 |r|)) (fun (x : ℂ) ↦ log⁺ ‖f x - a.untop₀‖⁻¹) fun (x : ℂ) ↦
    log⁺ ‖g x - a.untop₀‖⁻¹
have h₂ : ∀ (a_1 : ℂ), f a_1 = g a_1 → log⁺ ‖f a_1 - a.untop₀‖⁻¹ = log⁺ ‖g a_1 - a.untop₀‖⁻¹
Tactic: filter_upwards [hfg] using by aesop
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
r : ℝ
hfg : f =ᶠ[codiscrete ℂ] g
hr : r ≠ 0
⊢ Subset (α := Set ℂ) (sphere 0 |r|) univ
have tauto : ∀ ⦃a : ℂ⦄, Membership.mem (γ := Set ℂ) (sphere 0 |r|) a → Membership.mem (γ := Set ℂ) univ a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
f : ℂ → ℂ
h₁f : Meromorphic f
⊢ proximity f ⊤ - proximity f⁻¹ ⊤ = circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0
have h : ∀ (R : ℝ), (proximity f ⊤ - proximity f⁻¹ ⊤) R = circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R
Tactic: ext R
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
f : ℂ → ℂ
h₁f : Meromorphic f
R : ℝ
⊢ (proximity f ⊤ - proximity f⁻¹ ⊤) R = circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R
have h : HSub.hSub (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f x‖) 0 R) (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f x‖⁻¹) 0 R) =
  circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R
Tactic: simp only [proximity, ↓reduceDIte, Pi.inv_apply, norm_inv, Pi.sub_apply]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic (goal)
Goal:
f : ℂ → ℂ
h₁f : Meromorphic f
R : ℝ
⊢ HSub.hSub (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f x‖) 0 R) (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f x‖⁻¹) 0 R) =
    circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R
have h : circleAverage (HSub.hSub (α := ℂ → ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) fun (x : ℂ) ↦ log⁺ ‖f x‖⁻¹) 0 R =
  circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R
Tactic: rw [← circleAverage_sub]