awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
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 :
        ℝ)
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‖
⊢ characteristic f ⊤ R - characteristic f⁻¹ ⊤ 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]

Premises used: Norm.norm, Set.univ, HSub.hSub, Function.locallyFinsuppWithin.logCounting, ValueDistribution.characteristic, MeromorphicOn.divisor, Real.log, Inv.inv, meromorphicTrailingCoeffAt, Top.top, OfNat.ofNat, DFunLike.coe, Real.circleAverage
-- Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
Goal:
f : ℂ → ℂ
h : Meromorphic f
⊢ characteristic f ⊤ 0 - characteristic f⁻¹ ⊤ 0 = (characteristic f ⊤ - characteristic f⁻¹ ⊤) 0

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
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 :
        ℝ)
rw₁ 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 :
        ℝ)
⊢ (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:
rw [ValueDistribution.characteristic_sub_characteristic_inv h, Pi.sub_apply]

Premises used: ValueDistribution.characteristic_sub_characteristic_inv, Pi.sub_apply
-- Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
Goal:
f : ℂ → ℂ
h : Meromorphic f
⊢ 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:
simp
-- Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
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 :
        ℝ)
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‖
⊢ characteristic f ⊤ 0 - characteristic f⁻¹ ⊤ 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

Premises used: Norm.norm, Set.univ, HSub.hSub, Function.locallyFinsuppWithin.logCounting, ValueDistribution.characteristic, MeromorphicOn.divisor, Real.log, Inv.inv, Top.top, OfNat.ofNat, DFunLike.coe, Real.circleAverage
-- Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
Goal:
f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
pos :
  ∀ (h : R = 0),
    |characteristic f ⊤ R - characteristic f⁻¹ ⊤ R| ≤ max |log ‖f 0‖| |log ‖meromorphicTrailingCoeffAt f 0‖|
neg :
  ∀ (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‖|

Tactic:
by_cases h : R = 0
-- Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
Goal:
f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
h : R = 0
⊢ |characteristic f ⊤ R - characteristic f⁻¹ ⊤ R| ≤ max |log ‖f 0‖| |log ‖meromorphicTrailingCoeffAt f 0‖|

Tactic:
simp [h, characteristic_sub_characteristic_inv_at_zero hf]

Premises used: ValueDistribution.characteristic_sub_characteristic_inv_at_zero
-- Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
Goal:
f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
h : ¬R = 0
⊢ |characteristic f ⊤ R - characteristic f⁻¹ ⊤ R| ≤ max |log ‖f 0‖| |log ‖meromorphicTrailingCoeffAt f 0‖|

Tactic:
simp [characteristic_sub_characteristic_inv_of_ne_zero hf h]

Premises used: ValueDistribution.characteristic_sub_characteristic_inv_of_ne_zero
-- Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
Goal:
f : ℂ → ℂ
h : Meromorphic f
R : ℝ
⊢ ‖(characteristic f ⊤ - characteristic f⁻¹ ⊤) R‖ ≤
    max |log ‖f 0‖| |log ‖meromorphicTrailingCoeffAt f 0‖| * Norm.norm (E := ℝ) (1 R)

Tactic:
simpa using characteristic_sub_characteristic_inv_le h (R := R)

Premises used: ValueDistribution.characteristic_sub_characteristic_inv_le
-- Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h : Meromorphic 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
-- Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
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
hf : MeromorphicOn.{0, u_1} (E := E) (fun (x : ℂ) ↦ f x - a₀) (sphere 0 |r|)
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x - a₀‖) 0 r

Tactic:
apply MeromorphicOn.circleIntegrable_posLog_norm

Premises used: MeromorphicOn.circleIntegrable_posLog_norm
-- Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
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
⊢ MeromorphicOn.{0, u_1} (E := E) (fun (x : ℂ) ↦ f x - a₀) (sphere 0 |r|)

Tactic:
apply h.meromorphicOn.sub (MeromorphicOn.const a₀)

Premises used: Meromorphic.meromorphicOn, MeromorphicOn.const, MeromorphicOn.sub
-- Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
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

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₀)
-- Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
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
rw : |(proximity f ⊤ - proximity.{u_1} (E := E) (fun (x : ℂ) ↦ f x - a₀) ⊤) r| ≤ log⁺ ‖a₀‖ + log 2
⊢ |characteristic f ⊤ r - characteristic.{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]

Premises used: ValueDistribution.characteristic_sub_characteristic_eq_proximity_sub_proximity, Pi.sub_apply
-- Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
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
simp :
  |circleAverage (HSub.hSub (α := ℂ → ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) fun (x : ℂ) ↦ log⁺ ‖f x - a₀‖) 0 r| ≤
    log⁺ ‖a₀‖ + log 2
⊢ |(proximity f ⊤ - proximity.{u_1} (E := E) (fun (x : ℂ) ↦ f x - a₀) ⊤) r| ≤ log⁺ ‖a₀‖ + log 2

Tactic:
simp only [proximity, reduceDIte, Pi.sub_apply, ← circleAverage_sub h₁f h₂f]

Premises used: Real.circleAverage_sub, reduceDIte, ValueDistribution.proximity, Pi.sub_apply
-- Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
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
apply :
  circleAverage |HSub.hSub (α := ℂ → ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) fun (x : ℂ) ↦ log⁺ ‖f x - a₀‖| 0 r ≤
    log⁺ ‖a₀‖ + log 2
⊢ |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

Premises used: Real.abs_circleAverage_le_circleAverage_abs, le_trans
-- Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
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
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
⊢ circleAverage |HSub.hSub (α := ℂ → ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) fun (x : ℂ) ↦ log⁺ ‖f x - a₀‖| 0 r ≤
    log⁺ ‖a₀‖ + log 2

Tactic:
apply circleAverage_mono_on_of_le_circle

Premises used: Real.circleAverage_mono_on_of_le_circle
-- Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
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
⊢ CircleIntegrable |HSub.hSub (α := ℂ → ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) fun (x : ℂ) ↦ log⁺ ‖f x - a₀‖| 0 r

Tactic:
apply (h₁f.sub h₂f).abs

Premises used: CircleIntegrable.sub, CircleIntegrable.abs
-- Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
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
neg : ∀ (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

Tactic:
by_cases h : 0 ≤ log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖

Premises used: Norm.norm, Real.posLog, HSub.hSub
-- Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
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

Tactic:
simpa [abs_of_nonneg h, sub_le_iff_le_add, add_comm (log⁺ ‖a₀‖ + log 2), ← add_assoc]
        using (posLog_norm_add_le (f θ - a₀) a₀)

Premises used: Norm.norm, Real.posLog_norm_add_le, Real.posLog, add_assoc, HSub.hSub, sub_le_iff_le_add, Real.log, add_comm, HAdd.hAdd, abs_of_nonneg, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
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₀‖
neg : log⁺ ‖f θ - a₀‖ ≤ log⁺ ‖f θ‖ + log⁺ ‖a₀‖ + log 2
⊢ |log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖| ≤ 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]

Premises used: Norm.norm, neg_sub, Real.posLog, add_assoc, le_of_not_ge, tsub_le_iff_right, Real.log, add_comm, abs_of_nonpos, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
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

Tactic:
posLog_norm_add_le (-f θ) (a₀)

Premises used: Real.posLog_norm_add_le, Neg.neg
-- Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
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₀‖
h₁ : ‖f θ - a₀‖ = ‖-f θ + a₀‖
h₂ : log⁺ ‖f θ‖ + log⁺ ‖a₀‖ = log⁺ ‖-f θ‖ + log⁺ ‖a₀‖
⊢ log⁺ ‖f θ - a₀‖ ≤ log⁺ ‖f θ‖ + log⁺ ‖a₀‖ + log 2

Tactic:
convert! posLog_norm_add_le (-f θ) (a₀) using 2

Premises used: Real.posLog_norm_add_le, Neg.neg
-- Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
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₀‖
h₁ : ‖-(f θ - a₀)‖ = ‖-f θ + a₀‖
⊢ ‖f θ - a₀‖ = ‖-f θ + a₀‖

Tactic:
rw [← norm_neg]

Premises used: norm_neg
-- Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
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₀‖
⊢ ‖-(f θ - a₀)‖ = ‖-f θ + a₀‖

Tactic:
abel_nf
-- Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
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⁺ ‖a₀‖ = log⁺ ‖-f θ‖ + log⁺ ‖a₀‖

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
a₀ : E
f : ℂ → E
h : Meromorphic f
R : ℝ
⊢ ‖(characteristic f ⊤ - characteristic.{u_1} (E := E) (fun (x : ℂ) ↦ f x - a₀) ⊤) R‖ ≤
    (log⁺ ‖a₀‖ + log 2) * Norm.norm (E := ℝ) (1 R)

Tactic:
simpa using abs_characteristic_sub_characteristic_shift_le h

Premises used: ValueDistribution.abs_characteristic_sub_characteristic_shift_le
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : DecidableEq E
inst_2 : ProperSpace E
e : E
⊢ IsTheta (E := ℝ) atTop (fun (r : ℝ) ↦ log r - log ‖e‖) log

Tactic:
have hΘ : (fun r ↦ log r - log ‖e‖) =Θ[atTop] log :=
    (IsEquivalent.sub_isLittleO IsEquivalent.refl isLittleO_const_log_atTop).isTheta
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : DecidableEq E
inst_2 : ProperSpace E
e : E
hΘ : IsTheta (E := ℝ) atTop (fun (r : ℝ) ↦ log r - log ‖e‖) log
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop 1 fun (r : ℝ) ↦ log r - log ‖e‖

Tactic:
have h₁ : (1 : ℝ → ℝ) =o[atTop] fun r ↦ log r - log ‖e‖ :=
    (hΘ.isLittleO_congr_right).2 isLittleO_const_log_atTop
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : DecidableEq E
inst_2 : ProperSpace E
e : E
hΘ : IsTheta (E := ℝ) atTop (fun (r : ℝ) ↦ log r - log ‖e‖) log
h₁ : IsLittleO (E := ℝ) (F := ℝ) atTop 1 fun (r : ℝ) ↦ log r - log ‖e‖
⊢ IsLittleO (α := ℝ) (E := ℝ) (F := ℝ) atTop 1 ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1))

Tactic:
h₁.congr' EventuallyEq.rfl ?_

Premises used: Asymptotics.IsLittleO.congr', Filter.EventuallyEq.rfl
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : DecidableEq E
inst_2 : ProperSpace E
e : E
hΘ : IsTheta (E := ℝ) atTop (fun (r : ℝ) ↦ log r - log ‖e‖) log
h₁ : IsLittleO (E := ℝ) (F := ℝ) atTop 1 fun (r : ℝ) ↦ log r - log ‖e‖
refine :
  EventuallyEq (β := ℝ) atTop (fun (r : ℝ) ↦ log r - log ‖e‖)
    ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1))
⊢ IsLittleO (α := ℝ) (E := ℝ) (F := ℝ) atTop 1 ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1))

Tactic:
refine h₁.congr' EventuallyEq.rfl ?_

Premises used: Asymptotics.IsLittleO.congr', Filter.EventuallyEq.rfl
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : DecidableEq E
inst_2 : ProperSpace E
e : E
hΘ : IsTheta (E := ℝ) atTop (fun (r : ℝ) ↦ log r - log ‖e‖) log
h₁ : IsLittleO (E := ℝ) (F := ℝ) atTop 1 fun (r : ℝ) ↦ log r - log ‖e‖
h : ∀ (r : ℝ) (hr : ‖e‖ ≤ r), log r - log ‖e‖ = (logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) r
⊢ EventuallyEq (β := ℝ) atTop (fun (r : ℝ) ↦ log r - log ‖e‖)
    ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1))

Tactic:
filter_upwards [eventually_ge_atTop ‖e‖] with r hr

Premises used: Norm.norm, Filter.eventually_ge_atTop
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : DecidableEq E
inst_2 : ProperSpace E
e : E
hΘ : IsTheta (E := ℝ) atTop (fun (r : ℝ) ↦ log r - log ‖e‖) log
h₁ : IsLittleO (E := ℝ) (F := ℝ) atTop 1 fun (r : ℝ) ↦ log r - log ‖e‖
r : ℝ
hr : ‖e‖ ≤ r
⊢ log r - log ‖e‖ = (logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) r

Tactic:
simp [logCounting_single_eq_log_sub_const hr]

Premises used: Function.locallyFinsuppWithin.logCounting_single_eq_log_sub_const
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsuppWithin (X := E) univ ℤ
h : 0 ≤ D
h₂ : D = 0
⊢ IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1

Tactic:
simp [isBigO_of_le' (c := 0), h₂]

Premises used: Asymptotics.isBigO_of_le'
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsuppWithin (X := E) univ ℤ
h : 0 ≤ D
refine : IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1 → D = 0
⊢ D = 0 ↔ IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1

Tactic:
refine ⟨fun h₂ ↦ by simp [isBigO_of_le' (c := 0), h₂], ?_⟩
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsuppWithin (X := E) univ ℤ
h : 0 ≤ D
contrapose : ¬D = 0 → ¬IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1
⊢ IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1 → D = 0

Tactic:
contrapose
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsuppWithin (X := E) univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
obtain :
  ∀ (e : E) (he : single e 1 ≤ D),
    ¬IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1
⊢ ¬IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1

Tactic:
obtain ⟨e, he⟩ := exists_single_le_pos (lt_of_le_of_ne h (h₁ ·.symm))

Premises used: Function.locallyFinsuppWithin.exists_single_le_pos, Eq.symm, lt_of_le_of_ne
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsuppWithin (X := E) univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
rw :
  ¬∃ c > 0,
      ∀ᶠ (x : ℝ) in atTop,
        c * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D x : ℝ) ≤ Norm.norm (E := ℝ) (1 x)
⊢ ¬IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D) 1

Tactic:
rw [isBigO_iff'']

Premises used: Asymptotics.isBigO_iff''
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsuppWithin (X := E) univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
push :
  ∀ (c : ℝ) (_ : c > 0),
    ∃ᶠ (x : ℝ) in atTop,
      Norm.norm (E := ℝ) (1 x) < c * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D x : ℝ)
⊢ ¬∃ c > 0,
      ∀ᶠ (x : ℝ) in atTop,
        c * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D x : ℝ) ≤ Norm.norm (E := ℝ) (1 x)

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsuppWithin (X := E) univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
simp : ∀ (a_1 : ℝ), ∃ b ≥ a_1, 1 < HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D b| : ℝ)
⊢ ∃ᶠ (x : ℝ) in atTop,
    Norm.norm (E := ℝ) (1 x) < a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D x : ℝ)

Tactic:
simp only [Pi.one_apply, norm_eq_abs, frequently_atTop, abs_one]

Premises used: Pi.one_apply, Filter.frequently_atTop, abs_one, Real.norm_eq_abs