awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem (goal)
Goal:
f : ℂ → ℂ
h : Meromorphic f
calc :
  characteristic f ⊤ - characteristic f⁻¹ ⊤ = proximity f ⊤ - proximity f⁻¹ ⊤ - (logCounting f⁻¹ ⊤ - logCounting f ⊤)
calc₁ :
  proximity f ⊤ - proximity f⁻¹ ⊤ - (logCounting f⁻¹ ⊤ - logCounting f ⊤) =
    circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 - (logCounting f⁻¹ ⊤ - logCounting f ⊤)
calc₂ :
  circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 - (logCounting f⁻¹ ⊤ - logCounting f ⊤) =
    circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 - (logCounting f 0 - logCounting f ⊤)
⊢ characteristic f ⊤ - characteristic f⁻¹ ⊤ =
    HSub.hSub (α := (R : ℝ) → ℝ) (β := ℝ → ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0)
      ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) :
        ℝ → ℝ)
have calc₃ : circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 - (logCounting f 0 - logCounting f ⊤) =
  HSub.hSub (α := (R : ℝ) → ℝ) (β := ℝ → ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0)
    ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) :
      ℝ → ℝ)
Tactic: calc characteristic f ⊤ - characteristic f⁻¹ ⊤
  _ = proximity f ⊤ - proximity f⁻¹ ⊤ - (logCounting f⁻¹ ⊤ - logCounting f ⊤) := by
    unfold characteristic
    ring
  _ = circleAverage (log ‖f ·‖) 0 - (logCounting f⁻¹ ⊤ - logCounting f ⊤) := by
    rw [proximity_sub_proximity_inv_eq_circleAverage h]
  _ = circleAverage (log ‖f ·‖) 0 - (logCounting f 0 - logCounting f ⊤) := by
    rw [logCounting_inv]
  _ = circleAverage (log ‖f ·‖) 0 - (divisor f Set.univ).logCounting := by
    rw [← ValueDistribution.log_counting_zero_sub_logCounting_top]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem (goal)
Goal:
f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
hR : R ≠ 0
⊢ (characteristic f ⊤ - characteristic f⁻¹ ⊤) R =
    HSub.hSub (α := ℝ) (β := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R : ℝ)
      ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) R :
        ℝ)
have rw : HSub.hSub (α := (R : ℝ) → ℝ) (β := ℝ → ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0)
    ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) :
      ℝ → ℝ)
    R =
  HSub.hSub (α := ℝ) (β := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R : ℝ)
    ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) R : ℝ)
Tactic: rw [characteristic_sub_characteristic_inv hf, Pi.sub_apply]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem (goal)
Goal:
f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
hR : R ≠ 0
rw :
  HSub.hSub (α := (R : ℝ) → ℝ) (β := ℝ → ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0)
      ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) :
        ℝ → ℝ)
      R =
    HSub.hSub (α := ℝ) (β := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R : ℝ)
      ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) R :
        ℝ)
⊢ (characteristic f ⊤ - characteristic f⁻¹ ⊤) R =
    HSub.hSub (α := ℝ) (β := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R : ℝ)
      ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) R :
        ℝ)
have rw₁ : HSub.hSub (α := ℝ) (β := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R : ℝ)
    ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) R :
      ℝ) =
  HSub.hSub (α := ℝ) (β := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R : ℝ)
    ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) R : ℝ)
Tactic: rw [characteristic_sub_characteristic_inv hf, Pi.sub_apply]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem (goal)
Goal:
f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
hR : R ≠ 0
⊢ HSub.hSub (α := ℝ) (β := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R : ℝ)
      ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) R :
        ℝ) =
    log ‖meromorphicTrailingCoeffAt f 0‖
have rw : HSub.hSub (β := ℝ)
    (∑ᶠ (u : ℂ), (↑((divisor f (closedBall 0 |R|) : (a : ℂ) → ℤ) u) : ℝ) * log (R * ‖0 - u‖⁻¹) +
        (↑((divisor f (closedBall 0 |R|) : (a : ℂ) → ℤ) 0) : ℝ) * log R +
      log ‖meromorphicTrailingCoeffAt f 0‖)
    ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) R :
      ℝ) =
  log ‖meromorphicTrailingCoeffAt f 0‖
Tactic: rw [MeromorphicOn.circleAverage_log_norm hR hf.meromorphicOn]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem (goal)
Goal:
f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
hR : R ≠ 0
⊢ Subset (α := Set ℂ) (closedBall 0 |R|) Set.univ
have tauto : ∀ ⦃a : ℂ⦄, Membership.mem (γ := Set ℂ) (closedBall 0 |R|) a → Membership.mem (γ := Set ℂ) Set.univ a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem (hypothesis)
Goal:
f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
hR : R ≠ 0
⊢ HSub.hSub (β := ℝ)
      (∑ᶠ (u : ℂ), (↑((divisor f (closedBall 0 |R|) : (a : ℂ) → ℤ) u) : ℝ) * log (R * ‖0 - u‖⁻¹) +
          (↑((divisor f (closedBall 0 |R|) : (a : ℂ) → ℤ) 0) : ℝ) * log R +
        log ‖meromorphicTrailingCoeffAt f 0‖)
      (({
              toFun := fun (D : Function.locallyFinsupp ℂ ℤ) (r : ℝ) ↦
                ∑ᶠ (z : ℂ),
                    (↑((((toClosedBall r :
                                    (a : Function.locallyFinsupp ℂ ℤ) →
                                      Function.locallyFinsuppWithin (closedBall 0 |r|) ℤ)
                                  D :
                                Function.locallyFinsuppWithin (X := ℂ) (closedBall 0 |r|) ℤ) :
                              (a : ℂ) → ℤ)
                            z) :
                        ℝ) *
                      log (r * ‖z‖⁻¹) +
                  (↑((D : (a : ℂ) → ℤ) 0) : ℝ) * log r,
              map_zero' := ⋯, map_add' := ⋯ : Function.locallyFinsupp ℂ ℤ →+ ℝ → ℝ } :
            (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ)
          (divisor f Set.univ) R :
        ℝ) =
    log ‖meromorphicTrailingCoeffAt f 0‖
have this : Eq (α := Function.locallyFinsuppWithin (X := ℂ) (closedBall 0 |R|) ℤ) (divisor f (closedBall 0 |R|))
  ((toClosedBall R : (a : Function.locallyFinsupp ℂ ℤ) → Function.locallyFinsuppWithin (closedBall 0 |R|) ℤ)
    (divisor f Set.univ))
Tactic: have : (divisor f (closedBall 0 |R|)) = (divisor f Set.univ).toClosedBall R :=
      (divisor_restrict hf.meromorphicOn (by tauto)).symm
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem (goal)
Goal:
f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
hR : R ≠ 0
⊢ characteristic f ⊤ R - characteristic f⁻¹ ⊤ R = log ‖meromorphicTrailingCoeffAt f 0‖
have calc : characteristic f ⊤ R - characteristic f⁻¹ ⊤ R = (characteristic f ⊤ - characteristic f⁻¹ ⊤) R
Tactic: calc characteristic f ⊤ R - characteristic f⁻¹ ⊤ R
  _ = (characteristic f ⊤ - characteristic f⁻¹ ⊤) R := by simp
  _ = circleAverage (log ‖f ·‖) 0 R - (divisor f Set.univ).logCounting R := by
    rw [characteristic_sub_characteristic_inv hf, Pi.sub_apply]
  _ = log ‖meromorphicTrailingCoeffAt f 0‖ := by
    rw [MeromorphicOn.circleAverage_log_norm hR hf.meromorphicOn]
    unfold Function.locallyFinsuppWithin.logCounting
    have : (divisor f (closedBall 0 |R|)) = (divisor f Set.univ).toClosedBall R :=
      (divisor_restrict hf.meromorphicOn (by tauto)).symm
    simp [this, toClosedBall, restrictMonoidHom, restrict_apply]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem (goal)
Goal:
f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
hR : R ≠ 0
calc : characteristic f ⊤ R - characteristic f⁻¹ ⊤ R = (characteristic f ⊤ - characteristic f⁻¹ ⊤) R
⊢ characteristic f ⊤ R - characteristic f⁻¹ ⊤ R = log ‖meromorphicTrailingCoeffAt f 0‖
have calc₁ : (characteristic f ⊤ - characteristic f⁻¹ ⊤) R =
  HSub.hSub (α := ℝ) (β := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R : ℝ)
    ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) R : ℝ)
Tactic: calc characteristic f ⊤ R - characteristic f⁻¹ ⊤ R
  _ = (characteristic f ⊤ - characteristic f⁻¹ ⊤) R := by simp
  _ = circleAverage (log ‖f ·‖) 0 R - (divisor f Set.univ).logCounting R := by
    rw [characteristic_sub_characteristic_inv hf, Pi.sub_apply]
  _ = log ‖meromorphicTrailingCoeffAt f 0‖ := by
    rw [MeromorphicOn.circleAverage_log_norm hR hf.meromorphicOn]
    unfold Function.locallyFinsuppWithin.logCounting
    have : (divisor f (closedBall 0 |R|)) = (divisor f Set.univ).toClosedBall R :=
      (divisor_restrict hf.meromorphicOn (by tauto)).symm
    simp [this, toClosedBall, restrictMonoidHom, restrict_apply]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem (goal)
Goal:
f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
hR : R ≠ 0
calc : characteristic f ⊤ R - characteristic f⁻¹ ⊤ R = (characteristic f ⊤ - characteristic f⁻¹ ⊤) R
calc₁ :
  (characteristic f ⊤ - characteristic f⁻¹ ⊤) R =
    HSub.hSub (α := ℝ) (β := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R : ℝ)
      ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) R :
        ℝ)
⊢ characteristic f ⊤ R - characteristic f⁻¹ ⊤ R = log ‖meromorphicTrailingCoeffAt f 0‖
have calc₂ : HSub.hSub (α := ℝ) (β := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R : ℝ)
    ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) R :
      ℝ) =
  log ‖meromorphicTrailingCoeffAt f 0‖
Tactic: calc characteristic f ⊤ R - characteristic f⁻¹ ⊤ R
  _ = (characteristic f ⊤ - characteristic f⁻¹ ⊤) R := by simp
  _ = circleAverage (log ‖f ·‖) 0 R - (divisor f Set.univ).logCounting R := by
    rw [characteristic_sub_characteristic_inv hf, Pi.sub_apply]
  _ = log ‖meromorphicTrailingCoeffAt f 0‖ := by
    rw [MeromorphicOn.circleAverage_log_norm hR hf.meromorphicOn]
    unfold Function.locallyFinsuppWithin.logCounting
    have : (divisor f (closedBall 0 |R|)) = (divisor f Set.univ).toClosedBall R :=
      (divisor_restrict hf.meromorphicOn (by tauto)).symm
    simp [this, toClosedBall, restrictMonoidHom, restrict_apply]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem (goal)
Goal:
f : ℂ → ℂ
h : Meromorphic f
⊢ (characteristic f ⊤ - characteristic f⁻¹ ⊤) 0 =
    HSub.hSub (α := ℝ) (β := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 0 : ℝ)
      ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) 0 :
        ℝ)
have rw : HSub.hSub (α := (R : ℝ) → ℝ) (β := ℝ → ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0)
    ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) :
      ℝ → ℝ)
    0 =
  HSub.hSub (α := ℝ) (β := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 0 : ℝ)
    ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) 0 : ℝ)
Tactic: rw [ValueDistribution.characteristic_sub_characteristic_inv h, Pi.sub_apply]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem (goal)
Goal:
f : ℂ → ℂ
h : Meromorphic f
rw :
  HSub.hSub (α := (R : ℝ) → ℝ) (β := ℝ → ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0)
      ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) :
        ℝ → ℝ)
      0 =
    HSub.hSub (α := ℝ) (β := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 0 : ℝ)
      ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) 0 :
        ℝ)
⊢ (characteristic f ⊤ - characteristic f⁻¹ ⊤) 0 =
    HSub.hSub (α := ℝ) (β := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 0 : ℝ)
      ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) 0 :
        ℝ)
have rw₁ : HSub.hSub (α := ℝ) (β := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 0 : ℝ)
    ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) 0 :
      ℝ) =
  HSub.hSub (α := ℝ) (β := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 0 : ℝ)
    ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) 0 : ℝ)
Tactic: rw [ValueDistribution.characteristic_sub_characteristic_inv h, Pi.sub_apply]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem (goal)
Goal:
f : ℂ → ℂ
h : Meromorphic f
⊢ characteristic f ⊤ 0 - characteristic f⁻¹ ⊤ 0 = log ‖f 0‖
have calc : characteristic f ⊤ 0 - characteristic f⁻¹ ⊤ 0 = (characteristic f ⊤ - characteristic f⁻¹ ⊤) 0
Tactic: calc characteristic f ⊤ 0 - characteristic f⁻¹ ⊤ 0
  _ = (characteristic f ⊤ - characteristic f⁻¹ ⊤) 0 := by simp
  _ = circleAverage (log ‖f ·‖) 0 0 - (divisor f Set.univ).logCounting 0 := by
    rw [ValueDistribution.characteristic_sub_characteristic_inv h, Pi.sub_apply]
  _ = log ‖f 0‖ := by
    simp
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem (goal)
Goal:
f : ℂ → ℂ
h : Meromorphic f
calc : characteristic f ⊤ 0 - characteristic f⁻¹ ⊤ 0 = (characteristic f ⊤ - characteristic f⁻¹ ⊤) 0
⊢ characteristic f ⊤ 0 - characteristic f⁻¹ ⊤ 0 = log ‖f 0‖
have calc₁ : (characteristic f ⊤ - characteristic f⁻¹ ⊤) 0 =
  HSub.hSub (α := ℝ) (β := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 0 : ℝ)
    ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) 0 : ℝ)
Tactic: calc characteristic f ⊤ 0 - characteristic f⁻¹ ⊤ 0
  _ = (characteristic f ⊤ - characteristic f⁻¹ ⊤) 0 := by simp
  _ = circleAverage (log ‖f ·‖) 0 0 - (divisor f Set.univ).logCounting 0 := by
    rw [ValueDistribution.characteristic_sub_characteristic_inv h, Pi.sub_apply]
  _ = log ‖f 0‖ := by
    simp
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem (goal)
Goal:
f : ℂ → ℂ
h : Meromorphic f
calc : characteristic f ⊤ 0 - characteristic f⁻¹ ⊤ 0 = (characteristic f ⊤ - characteristic f⁻¹ ⊤) 0
calc₁ :
  (characteristic f ⊤ - characteristic f⁻¹ ⊤) 0 =
    HSub.hSub (α := ℝ) (β := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 0 : ℝ)
      ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) 0 :
        ℝ)
⊢ characteristic f ⊤ 0 - characteristic f⁻¹ ⊤ 0 = log ‖f 0‖
have calc₂ : HSub.hSub (α := ℝ) (β := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 0 : ℝ)
    ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) 0 :
      ℝ) =
  log ‖f 0‖
Tactic: calc characteristic f ⊤ 0 - characteristic f⁻¹ ⊤ 0
  _ = (characteristic f ⊤ - characteristic f⁻¹ ⊤) 0 := by simp
  _ = circleAverage (log ‖f ·‖) 0 0 - (divisor f Set.univ).logCounting 0 := by
    rw [ValueDistribution.characteristic_sub_characteristic_inv h, Pi.sub_apply]
  _ = log ‖f 0‖ := by
    simp
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem (goal)
Goal:
f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
⊢ |characteristic f ⊤ R - characteristic f⁻¹ ⊤ R| ≤ max |log ‖f 0‖| |log ‖meromorphicTrailingCoeffAt f 0‖|
have pos : ∀ (h : R = 0), |characteristic f ⊤ R - characteristic f⁻¹ ⊤ R| ≤ max |log ‖f 0‖| |log ‖meromorphicTrailingCoeffAt f 0‖|
Tactic: by_cases h : R = 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem (goal)
Goal:
f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
pos :
  ∀ (h : R = 0),
    |characteristic f ⊤ R - characteristic f⁻¹ ⊤ R| ≤ max |log ‖f 0‖| |log ‖meromorphicTrailingCoeffAt f 0‖|
⊢ |characteristic f ⊤ R - characteristic f⁻¹ ⊤ R| ≤ max |log ‖f 0‖| |log ‖meromorphicTrailingCoeffAt f 0‖|
have neg : ∀ (h : ¬R = 0), |characteristic f ⊤ R - characteristic f⁻¹ ⊤ R| ≤ max |log ‖f 0‖| |log ‖meromorphicTrailingCoeffAt f 0‖|
Tactic: by_cases h : R = 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h : Meromorphic f
⊢ |characteristic f ⊤ r - characteristic.{u_1} (E := E) (fun (x : ℂ) ↦ f x - a₀) ⊤ r| ≤ log⁺ ‖a₀‖ + log 2
have h₁f : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) 0 r
Tactic: have h₁f : CircleIntegrable (fun x ↦ log⁺ ‖f x‖) 0 r :=
    h.meromorphicOn.circleIntegrable_posLog_norm
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h : Meromorphic f
h₁f : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) 0 r
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x - a₀‖) 0 r
have hf : MeromorphicOn.{0, u_1} (E := E) (fun (x : ℂ) ↦ f x - a₀) (sphere 0 |r|)
Tactic: apply MeromorphicOn.circleIntegrable_posLog_norm
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h : Meromorphic f
h₁f : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) 0 r
⊢ |characteristic f ⊤ r - characteristic.{u_1} (E := E) (fun (x : ℂ) ↦ f x - a₀) ⊤ r| ≤ log⁺ ‖a₀‖ + log 2
have h₂f : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x - a₀‖) 0 r
Tactic: have h₂f : CircleIntegrable (fun x ↦ log⁺ ‖f x - a₀‖) 0 r := by
    apply MeromorphicOn.circleIntegrable_posLog_norm
    apply h.meromorphicOn.sub (MeromorphicOn.const a₀)
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h : Meromorphic f
h₁f : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x - a₀‖) 0 r
⊢ |characteristic f ⊤ r - characteristic.{u_1} (E := E) (fun (x : ℂ) ↦ f x - a₀) ⊤ r| ≤ log⁺ ‖a₀‖ + log 2
have rw : |(proximity f ⊤ - proximity.{u_1} (E := E) (fun (x : ℂ) ↦ f x - a₀) ⊤) r| ≤ log⁺ ‖a₀‖ + log 2
Tactic: rw [← Pi.sub_apply, characteristic_sub_characteristic_eq_proximity_sub_proximity h]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h : Meromorphic f
h₁f : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x - a₀‖) 0 r
⊢ |(proximity f ⊤ - proximity.{u_1} (E := E) (fun (x : ℂ) ↦ f x - a₀) ⊤) r| ≤ log⁺ ‖a₀‖ + log 2
have simp : |circleAverage (HSub.hSub (α := ℂ → ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) fun (x : ℂ) ↦ log⁺ ‖f x - a₀‖) 0 r| ≤
  log⁺ ‖a₀‖ + log 2
Tactic: simp only [proximity, reduceDIte, Pi.sub_apply, ← circleAverage_sub h₁f h₂f]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h : Meromorphic f
h₁f : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x - a₀‖) 0 r
⊢ |circleAverage (HSub.hSub (α := ℂ → ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) fun (x : ℂ) ↦ log⁺ ‖f x - a₀‖) 0 r| ≤
    log⁺ ‖a₀‖ + log 2
have apply : circleAverage |HSub.hSub (α := ℂ → ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) fun (x : ℂ) ↦ log⁺ ‖f x - a₀‖| 0 r ≤ log⁺ ‖a₀‖ + log 2
Tactic: apply le_trans abs_circleAverage_le_circleAverage_abs
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h : Meromorphic f
h₁f : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x - a₀‖) 0 r
⊢ circleAverage |HSub.hSub (α := ℂ → ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) fun (x : ℂ) ↦ log⁺ ‖f x - a₀‖| 0 r ≤
    log⁺ ‖a₀‖ + log 2
have hf : CircleIntegrable |HSub.hSub (α := ℂ → ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) fun (x : ℂ) ↦ log⁺ ‖f x - a₀‖| 0 r
Tactic: apply circleAverage_mono_on_of_le_circle
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h : Meromorphic f
h₁f : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x - a₀‖) 0 r
hf : CircleIntegrable |HSub.hSub (α := ℂ → ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) fun (x : ℂ) ↦ log⁺ ‖f x - a₀‖| 0 r
⊢ circleAverage |HSub.hSub (α := ℂ → ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) fun (x : ℂ) ↦ log⁺ ‖f x - a₀‖| 0 r ≤
    log⁺ ‖a₀‖ + log 2
have h₂f₁ : ∀ (x : ℂ),
  Membership.mem (γ := Set ℂ) (sphere 0 |r|) x →
    |HSub.hSub (α := ℂ → ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) fun (x : ℂ) ↦ log⁺ ‖f x - a₀‖| x ≤ log⁺ ‖a₀‖ + log 2
Tactic: apply circleAverage_mono_on_of_le_circle
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h : Meromorphic f
h₁f : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x - a₀‖) 0 r
θ : ℂ
hθ : Membership.mem (γ := Set ℂ) (sphere 0 |r|) θ
⊢ |log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖| ≤ log⁺ ‖a₀‖ + log 2
have pos : ∀ (h : 0 ≤ log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖), |log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖| ≤ log⁺ ‖a₀‖ + log 2
Tactic: by_cases h : 0 ≤ log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h : Meromorphic f
h₁f : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x - a₀‖) 0 r
θ : ℂ
hθ : Membership.mem (γ := Set ℂ) (sphere 0 |r|) θ
pos : ∀ (h : 0 ≤ log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖), |log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖| ≤ log⁺ ‖a₀‖ + log 2
⊢ |log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖| ≤ log⁺ ‖a₀‖ + log 2
have neg : ∀ (h : ¬0 ≤ log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖), |log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖| ≤ log⁺ ‖a₀‖ + log 2
Tactic: by_cases h : 0 ≤ log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h_1 : Meromorphic f
h₁f : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x - a₀‖) 0 r
θ : ℂ
hθ : Membership.mem (γ := Set ℂ) (sphere 0 |r|) θ
h : ¬0 ≤ log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖
⊢ |log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖| ≤ log⁺ ‖a₀‖ + log 2
have neg : log⁺ ‖f θ - a₀‖ ≤ log⁺ ‖f θ‖ + log⁺ ‖a₀‖ + log 2
Tactic: simp only [abs_of_nonpos (le_of_not_ge h), neg_sub, tsub_le_iff_right,
        add_comm (log⁺ ‖a₀‖ + log 2), ← add_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h_1 : Meromorphic f
h₁f : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x - a₀‖) 0 r
θ : ℂ
hθ : Membership.mem (γ := Set ℂ) (sphere 0 |r|) θ
h : ¬0 ≤ log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖
⊢ log⁺ ‖f θ - a₀‖ ≤ log⁺ ‖f θ‖ + log⁺ ‖a₀‖ + log 2
have h₁ : ‖f θ - a₀‖ = ‖-f θ + a₀‖
Tactic: convert! posLog_norm_add_le (-f θ) (a₀) using 2