awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Cartan (goal)
Goal:
f : ℂ → ℂ
h : meromorphicOrderAt f 0 < 0
a : ℂ
ha : Membership.mem (γ := Set ℂ) (sphere 0 |1|) a
⊢ meromorphicTrailingCoeffAt (fun (x : ℂ) ↦ f x - a) 0 = meromorphicTrailingCoeffAt f 0
have e_x : meromorphicOrderAt f 0 < meromorphicOrderAt (E := ℂ) (fun (x : ℂ) ↦ a) 0
Tactic: rw [(MeromorphicAt.const a 0).meromorphicTrailingCoeffAt_fun_sub_eq_left_of_lt]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.Cartan (goal)
Goal:
f : ℂ → ℂ
h : meromorphicOrderAt f 0 < 0
a : ℂ
ha : Membership.mem (γ := Set ℂ) (sphere 0 |1|) a
⊢ meromorphicOrderAt f 0 < meromorphicOrderAt (E := ℂ) (fun (x : ℂ) ↦ a) 0
have e_x : meromorphicOrderAt f 0 < if a = 0 then ⊤ else 0
Tactic: rw [meromorphicOrderAt_const]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
a : WithTop E
⊢ 0 ≤ᶠ[atTop] characteristic f a
have h : ∀ (a_1 : ℝ),
  Membership.mem (γ := Set ℝ)
    {x : ℝ |
      Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 1 ≤ x) x} x →
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 0 x ≤ characteristic f a x) x} x}
    a_1
Tactic: filter_upwards [Filter.eventually_ge_atTop 1] using fun _ hr ↦ by simp [characteristic_nonneg hr]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
a : WithTop E
h :
  ∀ (a_1 : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 1 ≤ x) x} x →
          Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 0 x ≤ characteristic f a x) x} x}
      a_1
⊢ 0 ≤ᶠ[atTop] characteristic f a
have h₁ : ∀ (a_1 : ℝ), 1 ≤ a_1 → 0 a_1 ≤ characteristic f a a_1
Tactic: filter_upwards [Filter.eventually_ge_atTop 1] using fun _ hr ↦ by simp [characteristic_nonneg hr]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
r : ℝ
hf : ∀ a ∈ s, Meromorphic (f a)
hr : 1 ≤ r
⊢ characteristic.{u_1} (E := E) (∑ a ∈ s, f a) ⊤ r ≤ (∑ a ∈ s, characteristic (f a) ⊤) r + log (↑s.card : ℝ)
have simp : proximity.{u_1} (E := E) (∑ a ∈ s, f a) ⊤ r + logCounting.{0, u_1} (𝕜 := ℂ) (E := E) (∑ a ∈ s, f a) ⊤ r ≤
  ∑ x ∈ s, (proximity (f x) ⊤ r + logCounting (f x) ⊤ r) + log (↑s.card : ℝ)
Tactic: simp only [characteristic, Pi.add_apply, Finset.sum_apply]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
r : ℝ
hf : ∀ a ∈ s, Meromorphic (f a)
hr : 1 ≤ r
⊢ proximity.{u_1} (E := E) (∑ a ∈ s, f a) ⊤ r + logCounting.{0, u_1} (𝕜 := ℂ) (E := E) (∑ a ∈ s, f a) ⊤ r ≤
    (∑ a ∈ s, proximity (f a) ⊤) r + log (↑s.card : ℝ) + (∑ a ∈ s, logCounting (f a) ⊤) r
have h₁ : proximity.{u_1} (E := E) (∑ a ∈ s, f a) ⊤ r ≤ (∑ a ∈ s, proximity (f a) ⊤) r + log (↑s.card : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
r : ℝ
hf : ∀ a ∈ s, Meromorphic (f a)
hr : 1 ≤ r
h₁ : proximity.{u_1} (E := E) (∑ a ∈ s, f a) ⊤ r ≤ (∑ a ∈ s, proximity (f a) ⊤) r + log (↑s.card : ℝ)
⊢ proximity.{u_1} (E := E) (∑ a ∈ s, f a) ⊤ r + logCounting.{0, u_1} (𝕜 := ℂ) (E := E) (∑ a ∈ s, f a) ⊤ r ≤
    (∑ a ∈ s, proximity (f a) ⊤) r + log (↑s.card : ℝ) + (∑ a ∈ s, logCounting (f a) ⊤) r
have h₂ : logCounting.{0, u_1} (𝕜 := ℂ) (E := E) (∑ a ∈ s, f a) ⊤ r ≤ (∑ a ∈ s, logCounting (f a) ⊤) r
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
r : ℝ
hf : ∀ a ∈ s, Meromorphic (f a)
hr : 1 ≤ r
⊢ proximity.{u_1} (E := E) (∑ a ∈ s, f a) ⊤ r + logCounting.{0, u_1} (𝕜 := ℂ) (E := E) (∑ a ∈ s, f a) ⊤ r ≤
    ∑ x ∈ s, (proximity (f x) ⊤ r + logCounting (f x) ⊤ r) + log (↑s.card : ℝ)
have calc : proximity.{u_1} (E := E) (∑ a ∈ s, f a) ⊤ r + logCounting.{0, u_1} (𝕜 := ℂ) (E := E) (∑ a ∈ s, f a) ⊤ r ≤
  (∑ a ∈ s, proximity (f a) ⊤) r + log (↑s.card : ℝ) + (∑ a ∈ s, logCounting (f a) ⊤) r
Tactic: calc proximity (∑ a ∈ s, f a) ⊤ r + logCounting (∑ a ∈ s, f a) ⊤ r
  _ ≤ ((∑ a ∈ s, proximity (f a) ⊤) r) + log s.card + (∑ a ∈ s, (logCounting (f a) ⊤)) r := by
      gcongr
      · apply proximity_sum_top_le s f hf r
      · apply logCounting_sum_top_le s f hf hr
    _ = ((∑ a ∈ s, proximity (f a) ⊤) r) + (∑ a ∈ s, (logCounting (f a) ⊤)) r + log s.card := by
      ring
    _ = ∑ x ∈ s, (proximity (f x) ⊤ r + logCounting (f x) ⊤ r) + log s.card := by
      simp [Finset.sum_add_distrib]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
r : ℝ
hf : ∀ a ∈ s, Meromorphic (f a)
hr : 1 ≤ r
calc :
  proximity.{u_1} (E := E) (∑ a ∈ s, f a) ⊤ r + logCounting.{0, u_1} (𝕜 := ℂ) (E := E) (∑ a ∈ s, f a) ⊤ r ≤
    (∑ a ∈ s, proximity (f a) ⊤) r + log (↑s.card : ℝ) + (∑ a ∈ s, logCounting (f a) ⊤) r
⊢ proximity.{u_1} (E := E) (∑ a ∈ s, f a) ⊤ r + logCounting.{0, u_1} (𝕜 := ℂ) (E := E) (∑ a ∈ s, f a) ⊤ r ≤
    ∑ x ∈ s, (proximity (f x) ⊤ r + logCounting (f x) ⊤ r) + log (↑s.card : ℝ)
have calc₁ : (∑ a ∈ s, proximity (f a) ⊤) r + log (↑s.card : ℝ) + (∑ a ∈ s, logCounting (f a) ⊤) r =
  HAdd.hAdd (α := ℝ) ((∑ a ∈ s, proximity (f a) ⊤) r) ((∑ a ∈ s, logCounting (f a) ⊤) r) + log (↑s.card : ℝ)
Tactic: calc proximity (∑ a ∈ s, f a) ⊤ r + logCounting (∑ a ∈ s, f a) ⊤ r
  _ ≤ ((∑ a ∈ s, proximity (f a) ⊤) r) + log s.card + (∑ a ∈ s, (logCounting (f a) ⊤)) r := by
      gcongr
      · apply proximity_sum_top_le s f hf r
      · apply logCounting_sum_top_le s f hf hr
    _ = ((∑ a ∈ s, proximity (f a) ⊤) r) + (∑ a ∈ s, (logCounting (f a) ⊤)) r + log s.card := by
      ring
    _ = ∑ x ∈ s, (proximity (f x) ⊤ r + logCounting (f x) ⊤ r) + log s.card := by
      simp [Finset.sum_add_distrib]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
r : ℝ
hf : ∀ a ∈ s, Meromorphic (f a)
hr : 1 ≤ r
calc :
  proximity.{u_1} (E := E) (∑ a ∈ s, f a) ⊤ r + logCounting.{0, u_1} (𝕜 := ℂ) (E := E) (∑ a ∈ s, f a) ⊤ r ≤
    (∑ a ∈ s, proximity (f a) ⊤) r + log (↑s.card : ℝ) + (∑ a ∈ s, logCounting (f a) ⊤) r
calc₁ :
  (∑ a ∈ s, proximity (f a) ⊤) r + log (↑s.card : ℝ) + (∑ a ∈ s, logCounting (f a) ⊤) r =
    HAdd.hAdd (α := ℝ) ((∑ a ∈ s, proximity (f a) ⊤) r) ((∑ a ∈ s, logCounting (f a) ⊤) r) + log (↑s.card : ℝ)
⊢ proximity.{u_1} (E := E) (∑ a ∈ s, f a) ⊤ r + logCounting.{0, u_1} (𝕜 := ℂ) (E := E) (∑ a ∈ s, f a) ⊤ r ≤
    ∑ x ∈ s, (proximity (f x) ⊤ r + logCounting (f x) ⊤ r) + log (↑s.card : ℝ)
have calc₂ : HAdd.hAdd (α := ℝ) ((∑ a ∈ s, proximity (f a) ⊤) r) ((∑ a ∈ s, logCounting (f a) ⊤) r) + log (↑s.card : ℝ) =
  ∑ x ∈ s, (proximity (f x) ⊤ r + logCounting (f x) ⊤ r) + log (↑s.card : ℝ)
Tactic: calc proximity (∑ a ∈ s, f a) ⊤ r + logCounting (∑ a ∈ s, f a) ⊤ r
  _ ≤ ((∑ a ∈ s, proximity (f a) ⊤) r) + log s.card + (∑ a ∈ s, (logCounting (f a) ⊤)) r := by
      gcongr
      · apply proximity_sum_top_le s f hf r
      · apply logCounting_sum_top_le s f hf hr
    _ = ((∑ a ∈ s, proximity (f a) ⊤) r) + (∑ a ∈ s, (logCounting (f a) ⊤)) r + log s.card := by
      ring
    _ = ∑ x ∈ s, (proximity (f x) ⊤ r + logCounting (f x) ⊤ r) + log s.card := by
      simp [Finset.sum_add_distrib]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
⊢ characteristic.{u_1} (E := E) (∑ a ∈ s, f a) ⊤ ≤ᶠ[atTop]
    HAdd.hAdd (α := ℝ → ℝ) (∑ a ∈ s, characteristic (f a) ⊤) fun (x : ℝ) ↦ log (↑s.card : ℝ)
have h : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ)
    {x : ℝ |
      Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 1 ≤ x) x} x →
        Membership.mem (γ := Set ℝ)
          {x : ℝ |
            (fun (x : ℝ) ↦
                characteristic.{u_1} (E := E) (∑ a ∈ s, f a) ⊤ x ≤
                  HAdd.hAdd (α := ℝ → ℝ) (β := ℝ → ℝ) (∑ a ∈ s, characteristic (f a) ⊤)
                    (fun (x : ℝ) ↦ log (↑s.card : ℝ)) x)
              x}
          x}
    a
Tactic: filter_upwards [Filter.eventually_ge_atTop 1]
    using fun _ hr ↦ characteristic_sum_top_le s f hf hr
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ 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 : ℝ) ↦
                  characteristic.{u_1} (E := E) (∑ a ∈ s, f a) ⊤ x ≤
                    HAdd.hAdd (α := ℝ → ℝ) (β := ℝ → ℝ) (∑ a ∈ s, characteristic (f a) ⊤)
                      (fun (x : ℝ) ↦ log (↑s.card : ℝ)) x)
                x}
            x}
      a
⊢ characteristic.{u_1} (E := E) (∑ a ∈ s, f a) ⊤ ≤ᶠ[atTop]
    HAdd.hAdd (α := ℝ → ℝ) (∑ a ∈ s, characteristic (f a) ⊤) fun (x : ℝ) ↦ log (↑s.card : ℝ)
have h₁ : ∀ (a : ℝ),
  1 ≤ a →
    characteristic.{u_1} (E := E) (∑ a ∈ s, f a) ⊤ a ≤
      HAdd.hAdd (α := ℝ → ℝ) (β := ℝ → ℝ) (∑ a ∈ s, characteristic (f a) ⊤) (fun (x : ℝ) ↦ log (↑s.card : ℝ)) a
Tactic: filter_upwards [Filter.eventually_ge_atTop 1]
    using fun _ hr ↦ characteristic_sum_top_le s f hf hr
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f₁ f₂ : ℂ → E
r : ℝ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
hr : 1 ≤ r
⊢ characteristic (f₁ + f₂) ⊤ r ≤ characteristic f₁ ⊤ r + characteristic f₂ ⊤ r + log 2
have h_meromorphic : ∀ (a : Fin (Nat.succ 0).succ),
  Membership.mem (γ := Finset (Fin (Nat.succ 0).succ)) Finset.univ a → Meromorphic (![f₁, f₂] a)
Tactic: have h_meromorphic : ∀ a ∈ Finset.univ, Meromorphic (![f₁, f₂] a) := by
    simpa using ⟨h₁f₁, h₁f₂⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f₁ f₂ : ℂ → E
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ characteristic (f₁ + f₂) ⊤ ≤ᶠ[atTop] characteristic f₁ ⊤ + characteristic f₂ ⊤ + fun (x : ℝ) ↦ log 2
have h : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ)
    {x : ℝ |
      Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 1 ≤ x) x} x →
        Membership.mem (γ := Set ℝ)
          {x : ℝ |
            (fun (x : ℝ) ↦
                characteristic (f₁ + f₂) ⊤ x ≤
                  HAdd.hAdd (β := ℝ → ℝ) (characteristic f₁ ⊤ + characteristic f₂ ⊤) (fun (x : ℝ) ↦ log 2) x)
              x}
          x}
    a
Tactic: filter_upwards [Filter.eventually_ge_atTop 1] with r hr
    using characteristic_add_top_le h₁f₁ h₁f₂ hr
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f₁ f₂ : ℂ → E
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 1 ≤ x) x} x →
          Membership.mem (γ := Set ℝ)
            {x : ℝ |
              (fun (x : ℝ) ↦
                  characteristic (f₁ + f₂) ⊤ x ≤
                    HAdd.hAdd (β := ℝ → ℝ) (characteristic f₁ ⊤ + characteristic f₂ ⊤) (fun (x : ℝ) ↦ log 2) x)
                x}
            x}
      a
⊢ characteristic (f₁ + f₂) ⊤ ≤ᶠ[atTop] characteristic f₁ ⊤ + characteristic f₂ ⊤ + fun (x : ℝ) ↦ log 2
have h₁ : ∀ (a : ℝ),
  1 ≤ a →
    characteristic (f₁ + f₂) ⊤ a ≤
      HAdd.hAdd (β := ℝ → ℝ) (characteristic f₁ ⊤ + characteristic f₂ ⊤) (fun (x : ℝ) ↦ log 2) a
Tactic: filter_upwards [Filter.eventually_ge_atTop 1] with r hr
    using characteristic_add_top_le h₁f₁ h₁f₂ hr
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction (goal)
Goal:
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 ≠ ⊤
⊢ proximity (f₁ * f₂) 0 r + logCounting (f₁ * f₂) 0 r ≤
    proximity f₁ 0 r + logCounting f₁ 0 r + (proximity f₂ 0 r + logCounting f₂ 0 r)
have rw : proximity (f₁ * f₂) 0 r + logCounting (f₁ * f₂) 0 r ≤
  proximity f₁ 0 r + proximity f₂ 0 r + (logCounting f₁ 0 r + logCounting f₂ 0 r)
Tactic: rw [add_add_add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction (goal)
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : ℂ), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : ℂ), meromorphicOrderAt f₂ z ≠ ⊤
⊢ characteristic (f₁ * f₂) 0 ≤ᶠ[atTop] characteristic f₁ 0 + characteristic 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 : ℝ) ↦ characteristic (f₁ * f₂) 0 x ≤ (characteristic f₁ 0 + characteristic f₂ 0) x) x} x}
    a
Tactic: filter_upwards [Filter.eventually_ge_atTop 1]
    using fun _ hr ↦ characteristic_mul_zero_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction (goal)
Goal:
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 : ℝ) ↦ characteristic (f₁ * f₂) 0 x ≤ (characteristic f₁ 0 + characteristic f₂ 0) x) x} x}
      a
⊢ characteristic (f₁ * f₂) 0 ≤ᶠ[atTop] characteristic f₁ 0 + characteristic f₂ 0
have h₁ : ∀ (a : ℝ), 1 ≤ a → characteristic (f₁ * f₂) 0 a ≤ (characteristic f₁ 0 + characteristic f₂ 0) a
Tactic: filter_upwards [Filter.eventually_ge_atTop 1]
    using fun _ hr ↦ characteristic_mul_zero_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction (goal)
Goal:
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 ≠ ⊤
⊢ proximity (f₁ * f₂) ⊤ r + logCounting (f₁ * f₂) ⊤ r ≤
    proximity f₁ ⊤ r + logCounting f₁ ⊤ r + (proximity f₂ ⊤ r + logCounting f₂ ⊤ r)
have rw : proximity (f₁ * f₂) ⊤ r + logCounting (f₁ * f₂) ⊤ r ≤
  proximity f₁ ⊤ r + proximity f₂ ⊤ r + (logCounting f₁ ⊤ r + logCounting f₂ ⊤ r)
Tactic: rw [add_add_add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction (goal)
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : ℂ), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : ℂ), meromorphicOrderAt f₂ z ≠ ⊤
⊢ characteristic (f₁ * f₂) ⊤ ≤ᶠ[atTop] characteristic f₁ ⊤ + characteristic f₂ ⊤
have h : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ)
    {x : ℝ |
      Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 1 ≤ x) x} x →
        Membership.mem (γ := Set ℝ)
          {x : ℝ | (fun (x : ℝ) ↦ characteristic (f₁ * f₂) ⊤ x ≤ (characteristic f₁ ⊤ + characteristic f₂ ⊤) x) x} x}
    a
Tactic: filter_upwards [Filter.eventually_ge_atTop 1]
    using fun _ hr ↦ characteristic_mul_top_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction (goal)
Goal:
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 : ℝ) ↦ characteristic (f₁ * f₂) ⊤ x ≤ (characteristic f₁ ⊤ + characteristic f₂ ⊤) x) x} x}
      a
⊢ characteristic (f₁ * f₂) ⊤ ≤ᶠ[atTop] characteristic f₁ ⊤ + characteristic f₂ ⊤
have h₁ : ∀ (a : ℝ), 1 ≤ a → characteristic (f₁ * f₂) ⊤ a ≤ (characteristic f₁ ⊤ + characteristic f₂ ⊤) a
Tactic: filter_upwards [Filter.eventually_ge_atTop 1]
    using fun _ hr ↦ characteristic_mul_top_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem (goal)
Goal:
f : ℂ → ℂ
h : Meromorphic f
⊢ proximity f ⊤ - proximity f⁻¹ ⊤ - (logCounting f⁻¹ ⊤ - logCounting f ⊤) =
    circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 - (logCounting f⁻¹ ⊤ - logCounting f ⊤)
have rw : circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 - (logCounting f⁻¹ ⊤ - logCounting f ⊤) =
  circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 - (logCounting f⁻¹ ⊤ - logCounting f ⊤)
Tactic: rw [proximity_sub_proximity_inv_eq_circleAverage h]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem (goal)
Goal:
f : ℂ → ℂ
h : Meromorphic f
⊢ circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 - (logCounting f⁻¹ ⊤ - logCounting f ⊤) =
    circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 - (logCounting f 0 - logCounting f ⊤)
have rw : circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 - (logCounting f 0 - logCounting f ⊤) =
  circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 - (logCounting f 0 - logCounting f ⊤)
Tactic: rw [logCounting_inv]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem (goal)
Goal:
f : ℂ → ℂ
h : Meromorphic f
⊢ 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) :
        ℝ → ℝ)
have rw : HSub.hSub (α := (R : ℝ) → ℝ) (β := ℝ → ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0)
    ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) :
      ℝ → ℝ) =
  HSub.hSub (α := (R : ℝ) → ℝ) (β := ℝ → ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0)
    ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) :
      ℝ → ℝ)
Tactic: rw [← ValueDistribution.log_counting_zero_sub_logCounting_top]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem (goal)
Goal:
f : ℂ → ℂ
h : Meromorphic 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 : characteristic f ⊤ - characteristic f⁻¹ ⊤ = proximity f ⊤ - proximity f⁻¹ ⊤ - (logCounting f⁻¹ ⊤ - logCounting f ⊤)
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 : ℂ → ℂ
h : Meromorphic f
calc :
  characteristic f ⊤ - characteristic f⁻¹ ⊤ = proximity f ⊤ - proximity f⁻¹ ⊤ - (logCounting f⁻¹ ⊤ - 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₁ : proximity f ⊤ - proximity f⁻¹ ⊤ - (logCounting f⁻¹ ⊤ - logCounting f ⊤) =
  circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 - (logCounting f⁻¹ ⊤ - logCounting f ⊤)
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 : ℂ → ℂ
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 ⊤)
⊢ 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⁻¹ ⊤ - logCounting f ⊤) =
  circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 - (logCounting f 0 - logCounting f ⊤)
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]