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
f : 𝕜 → E
rw :
  (locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
      (HSub.hSub (α := locallyFinsuppWithin (X := 𝕜) univ ℤ) (divisor f univ)⁺ (divisor f univ)⁻) =
    logCounting f 0 - logCounting f ⊤
rw₁ :
  (locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
      (HSub.hSub (α := locallyFinsuppWithin (X := 𝕜) univ ℤ) (divisor f univ)⁺ (divisor f univ)⁻) =
    HSub.hSub (α := ℝ → ℝ)
      ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ) (divisor f univ)⁺ : ℝ → ℝ)
      (logCounting f ⊤)
⊢ (locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ) (divisor f univ) =
    logCounting f 0 - logCounting f ⊤
have rw₂ : (locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
    (HSub.hSub (α := locallyFinsuppWithin (X := 𝕜) univ ℤ) (divisor f univ)⁺ (divisor f univ)⁻) =
  HSub.hSub (α := ℝ → ℝ) (β := ℝ → ℝ)
    ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ) (divisor f univ)⁺ : ℝ → ℝ)
    ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ) (divisor f univ)⁻ : ℝ → ℝ)
Tactic: rw [← posPart_sub_negPart (divisor f univ), logCounting_zero, logCounting_top, map_sub]
-- 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
f : 𝕜 → E
rw :
  (locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
      (HSub.hSub (α := locallyFinsuppWithin (X := 𝕜) univ ℤ) (divisor f univ)⁺ (divisor f univ)⁻) =
    logCounting f 0 - logCounting f ⊤
rw₁ :
  (locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
      (HSub.hSub (α := locallyFinsuppWithin (X := 𝕜) univ ℤ) (divisor f univ)⁺ (divisor f univ)⁻) =
    HSub.hSub (α := ℝ → ℝ)
      ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ) (divisor f univ)⁺ : ℝ → ℝ)
      (logCounting f ⊤)
rw₂ :
  (locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
      (HSub.hSub (α := locallyFinsuppWithin (X := 𝕜) univ ℤ) (divisor f univ)⁺ (divisor f univ)⁻) =
    HSub.hSub (α := ℝ → ℝ) (β := ℝ → ℝ)
      ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ) (divisor f univ)⁺ : ℝ → ℝ)
      ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ) (divisor f univ)⁻ : ℝ → ℝ)
⊢ (locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ) (divisor f univ) =
    logCounting f 0 - logCounting f ⊤
have rw₃ : HSub.hSub (α := ℝ → ℝ) (β := ℝ → ℝ)
    ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ) (divisor f univ)⁺ : ℝ → ℝ)
    ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ) (divisor f univ)⁻ : ℝ → ℝ) =
  HSub.hSub (α := ℝ → ℝ) (β := ℝ → ℝ)
    ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ) (divisor f univ)⁺ : ℝ → ℝ)
    ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ) (divisor f univ)⁻ : ℝ → ℝ)
Tactic: rw [← posPart_sub_negPart (divisor f univ), logCounting_zero, logCounting_top, map_sub]
-- 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
f : 𝕜 → E
e : WithTop E
r : ℝ
⊢ logCounting f e (-r) = logCounting f e r
have pos : ∀ (h : e = ⊤), logCounting f e (-r) = logCounting f e r
Tactic: by_cases h : e = ⊤
-- 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
f : 𝕜 → E
e : WithTop E
r : ℝ
pos : ∀ (h : e = ⊤), logCounting f e (-r) = logCounting f e r
⊢ logCounting f e (-r) = logCounting f e r
have neg : ∀ (h : ¬e = ⊤), logCounting f e (-r) = logCounting f e r
Tactic: by_cases h : e = ⊤
-- 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
f : 𝕜 → E
e : WithTop E
⊢ MonotoneOn (logCounting f e) (Ioi 0)
have pos : ∀ (h : e = ⊤), MonotoneOn (logCounting f e) (Ioi 0)
Tactic: by_cases h : e = ⊤
-- 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
f : 𝕜 → E
e : WithTop E
pos : ∀ (h : e = ⊤), MonotoneOn (logCounting f e) (Ioi 0)
⊢ MonotoneOn (logCounting f e) (Ioi 0)
have neg : ∀ (h : ¬e = ⊤), MonotoneOn (logCounting f e) (Ioi 0)
Tactic: by_cases h : e = ⊤
-- 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
r : ℝ
f : 𝕜 → E
e : WithTop E
hr : 1 ≤ r
⊢ 0 ≤ logCounting f e r
have pos : ∀ (h : e = ⊤), 0 ≤ logCounting f e r
Tactic: by_cases h : e = ⊤
-- 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
r : ℝ
f : 𝕜 → E
e : WithTop E
hr : 1 ≤ r
pos : ∀ (h : e = ⊤), 0 ≤ logCounting f e r
⊢ 0 ≤ logCounting f e r
have neg : ∀ (h : ¬e = ⊤), 0 ≤ logCounting f e r
Tactic: by_cases h : e = ⊤
-- 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
f : 𝕜 → E
e : WithTop E
⊢ 0 ≤ᶠ[atTop] logCounting f e
have h : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ)
    {x : ℝ |
      Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 1 ≤ x) x} x →
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 0 x ≤ logCounting f e x) x} x}
    a
Tactic: filter_upwards [eventually_ge_atTop 1] using fun _ hr ↦ by simp [logCounting_nonneg hr]
-- 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
f : 𝕜 → E
e : WithTop E
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 1 ≤ x) x} x →
          Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 0 x ≤ logCounting f e x) x} x}
      a
⊢ 0 ≤ᶠ[atTop] logCounting f e
have h₁ : ∀ (a : ℝ), 1 ≤ a → 0 a ≤ logCounting f e a
Tactic: filter_upwards [eventually_ge_atTop 1] using fun _ hr ↦ by simp [logCounting_nonneg hr]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : ℂ → E
hfg : f =ᶠ[codiscrete ℂ] g
⊢ logCounting f = logCounting g
have h : ∀ (a : WithTop E), logCounting f a = logCounting g a
Tactic: ext a : 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : ℂ → E
hfg : f =ᶠ[codiscrete ℂ] g
a : WithTop E
⊢ logCounting f a = logCounting g a
have pos : ∀ (h : a = ⊤), logCounting f a = logCounting g a
Tactic: by_cases h : a = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : ℂ → E
hfg : f =ᶠ[codiscrete ℂ] g
a : WithTop E
pos : ∀ (h : a = ⊤), logCounting f a = logCounting g a
⊢ logCounting f a = logCounting g a
have neg : ∀ (h : ¬a = ⊤), logCounting f a = logCounting g a
Tactic: by_cases h : a = ⊤
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : ℂ → E
hfg : f =ᶠ[codiscrete ℂ] g
a : WithTop E
h : a = ⊤
⊢ logCounting f a = logCounting g a
have pos : Eq (α := ℝ → ℝ) ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f univ)⁻ : ℝ → ℝ)
  ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor g univ)⁻ : ℝ → ℝ)
Tactic: simp only [logCounting, h, ↓reduceDIte]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : ℂ → E
hfg : f =ᶠ[codiscrete ℂ] g
a : WithTop E
h : a = ⊤
⊢ Eq (α := ℝ → ℝ) ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f univ)⁻ : ℝ → ℝ)
    ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor g univ)⁻ : ℝ → ℝ)
have pos : Eq (α := locallyFinsupp ℂ ℤ) (divisor f univ) (divisor g univ)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : ℂ → E
hfg : f =ᶠ[codiscrete ℂ] g
a : WithTop E
h : ¬a = ⊤
⊢ logCounting f a = logCounting g a
have neg : Eq (α := ℝ → ℝ)
  ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp ℂ ℤ) → ℝ → ℝ)
      (divisor.{0, u_2} (E := E) (fun (x : ℂ) ↦ f x - a.untop₀) univ)⁺ :
    ℝ → ℝ)
  ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp ℂ ℤ) → ℝ → ℝ)
      (divisor.{0, u_2} (E := E) (fun (x : ℂ) ↦ g x - a.untop₀) univ)⁺ :
    ℝ → ℝ)
Tactic: simp only [logCounting, h, ↓reduceDIte]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : ℂ → E
hfg : f =ᶠ[codiscrete ℂ] g
a : WithTop E
h : ¬a = ⊤
⊢ Eq (α := ℝ → ℝ)
    ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp ℂ ℤ) → ℝ → ℝ)
        (divisor.{0, u_2} (E := E) (fun (x : ℂ) ↦ f x - a.untop₀) univ)⁺ :
      ℝ → ℝ)
    ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp ℂ ℤ) → ℝ → ℝ)
        (divisor.{0, u_2} (E := E) (fun (x : ℂ) ↦ g x - a.untop₀) univ)⁺ :
      ℝ → ℝ)
have neg : Eq (α := locallyFinsupp ℂ ℤ) (divisor.{0, u_2} (E := E) (fun (x : ℂ) ↦ f x - a.untop₀) univ)
  (divisor.{0, u_2} (E := E) (fun (x : ℂ) ↦ g x - a.untop₀) univ)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : ℂ → E
hfg : f =ᶠ[codiscrete ℂ] g
a : WithTop E
h : ¬a = ⊤
⊢ Eq (α := locallyFinsupp ℂ ℤ) (divisor.{0, u_2} (E := E) (fun (x : ℂ) ↦ f x - a.untop₀) univ)
    (divisor.{0, u_2} (E := E) (fun (x : ℂ) ↦ g x - a.untop₀) univ)
have apply : EventuallyEq.{0, u_2} (β := E) (codiscreteWithin univ) (fun (x : ℂ) ↦ f x - a.untop₀) fun (x : ℂ) ↦ g x - a.untop₀
Tactic: apply divisor_congr_codiscreteWithin _ isOpen_univ
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : ℂ → E
hfg : f =ᶠ[codiscrete ℂ] g
a : WithTop E
h : ¬a = ⊤
⊢ EventuallyEq.{0, u_2} (β := E) (codiscreteWithin univ) (fun (x : ℂ) ↦ f x - a.untop₀) fun (x : ℂ) ↦ 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.{u_2 + 1} (α := E) ((fun (x : ℂ) ↦ f x - a.untop₀) x) ((fun (x : ℂ) ↦ g x - a.untop₀) x))
              x}
          x}
    a_1
Tactic: filter_upwards [hfg] using by simp
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : ℂ → E
hfg : f =ᶠ[codiscrete ℂ] g
a : WithTop E
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.{u_2 + 1} (α := E) ((fun (x : ℂ) ↦ f x - a.untop₀) x) ((fun (x : ℂ) ↦ g x - a.untop₀) x))
                x}
            x}
      a_1
⊢ EventuallyEq.{0, u_2} (β := E) (codiscreteWithin univ) (fun (x : ℂ) ↦ f x - a.untop₀) fun (x : ℂ) ↦ g x - a.untop₀
have h₂ : ∀ (a_1 : ℂ), f a_1 = g a_1 → f a_1 - a.untop₀ = g a_1 - a.untop₀
Tactic: filter_upwards [hfg] using by simp
-- 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
f g : 𝕜 → E
hf : Meromorphic f
hg : AnalyticOn 𝕜 g univ
⊢ Eq (α := ℝ → ℝ)
    ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ) (divisor (f + g) univ)⁻ : ℝ → ℝ)
    ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ) (divisor f univ)⁻ : ℝ → ℝ)
have rw : Eq (α := ℝ → ℝ) ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ) (divisor f univ)⁻ : ℝ → ℝ)
  ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ) (divisor f univ)⁻ : ℝ → ℝ)
Tactic: rw [hf.meromorphicOn.negPart_divisor_add_of_analyticNhdOn_right
    (isOpen_univ.analyticOn_iff_analyticOnNhd.1 hg)]
-- 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
f₁ f₂ : 𝕜 → E
r : ℝ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
hr : 1 ≤ r
⊢ (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 𝕜 ℤ) → ℝ → ℝ) (divisor (f₁ + f₂) univ)⁻ r : ℝ)
  ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
      (HAdd.hAdd (α := locallyFinsupp 𝕜 ℤ) (divisor f₁ univ)⁻ (divisor f₂ univ)⁻) r :
    ℝ)
Tactic: rw [← 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 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f₁ f₂ : 𝕜 → E
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ 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_add_top_le h₁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 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : 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 : ℝ) ↦ 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_add_top_le h₁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 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
α : Type u_3
f : α → 𝕜 → E
r : ℝ
hr : 1 ≤ r
a : α
s : Finset α
ha : a ∉ s
hs :
  ∀ (h₁f : ∀ a ∈ s, Meromorphic (f a)),
    logCounting.{u_1, u_2} (𝕜 := 𝕜) (E := E) (∑ a ∈ s, f a) ⊤ r ≤ (∑ a ∈ s, logCounting (f a) ⊤) r
h₁f : ∀ a_1 ∈ insert a s, Meromorphic (f a_1)
⊢ logCounting.{u_1, u_2} (𝕜 := 𝕜) (E := E) (∑ a ∈ insert a s, f a) ⊤ r ≤ (∑ a ∈ insert a s, logCounting (f a) ⊤) r
have insert : logCounting (f a + ∑ x ∈ s, f x) ⊤ r ≤ HAdd.hAdd (β := ℝ → ℝ) (logCounting (f a) ⊤) (∑ x ∈ s, logCounting (f x) ⊤) r
Tactic: rw [Finset.sum_insert ha, Finset.sum_insert ha]
-- 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
r : ℝ
h₁f : ∀ a ∈ s, Meromorphic (f a)
hr : 1 ≤ r
⊢ logCounting.{u_1, u_2} (𝕜 := 𝕜) (E := E) (∑ a ∈ s, f a) ⊤ r ≤ (∑ a ∈ s, logCounting (f a) ⊤) r
have empty : ∀ (h₁f : ∀ (a : α), Membership.mem (γ := Finset α) ∅ a → Meromorphic (f a)),
  logCounting.{u_1, u_2} (𝕜 := 𝕜) (E := E) (∑ a ∈ ∅, f a) ⊤ r ≤ (∑ a ∈ ∅, logCounting (f a) ⊤) r
Tactic: induction s using Finset.induction with
  | empty =>
    simp
  | insert a s ha hs =>
    rw [Finset.sum_insert ha, Finset.sum_insert ha]
    calc logCounting (f a + ∑ x ∈ s, f x) ⊤ r
      _ ≤ (logCounting (f a) ⊤ + logCounting (∑ x ∈ s, f x) ⊤) r :=
        logCounting_add_top_le (h₁f a (Finset.mem_insert_self a s))
          (Meromorphic.sum (fun σ hσ ↦ h₁f σ (Finset.mem_insert_of_mem hσ))) hr
      _ ≤ (logCounting (f a) ⊤ + ∑ x ∈ s, logCounting (f x) ⊤) r :=
        add_le_add (by trivial) (hs (fun a ha ↦ h₁f a (Finset.mem_insert_of_mem ha)))
Cleared hypotheses: s, h₁f
-- 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
r : ℝ
h₁f : ∀ a ∈ s, Meromorphic (f a)
hr : 1 ≤ r
empty :
  ∀ (h₁f : ∀ (a : α), Membership.mem (γ := Finset α) ∅ a → Meromorphic (f a)),
    logCounting.{u_1, u_2} (𝕜 := 𝕜) (E := E) (∑ a ∈ ∅, f a) ⊤ r ≤ (∑ a ∈ ∅, logCounting (f a) ⊤) r
⊢ logCounting.{u_1, u_2} (𝕜 := 𝕜) (E := E) (∑ a ∈ s, f a) ⊤ r ≤ (∑ a ∈ s, logCounting (f a) ⊤) r
have insert : ∀ (a : α) (s : Finset α) (ha : a ∉ s)
  (hs :
    ∀ (h₁f : ∀ a ∈ s, Meromorphic (f a)),
      logCounting.{u_1, u_2} (𝕜 := 𝕜) (E := E) (∑ a ∈ s, f a) ⊤ r ≤ (∑ a ∈ s, logCounting (f a) ⊤) r)
  (h₁f : ∀ a_1 ∈ insert a s, Meromorphic (f a_1)),
  logCounting.{u_1, u_2} (𝕜 := 𝕜) (E := E) (∑ a ∈ insert a s, f a) ⊤ r ≤ (∑ a ∈ insert a s, logCounting (f a) ⊤) r
Tactic: induction s using Finset.induction with
  | empty =>
    simp
  | insert a s ha hs =>
    rw [Finset.sum_insert ha, Finset.sum_insert ha]
    calc logCounting (f a + ∑ x ∈ s, f x) ⊤ r
      _ ≤ (logCounting (f a) ⊤ + logCounting (∑ x ∈ s, f x) ⊤) r :=
        logCounting_add_top_le (h₁f a (Finset.mem_insert_self a s))
          (Meromorphic.sum (fun σ hσ ↦ h₁f σ (Finset.mem_insert_of_mem hσ))) hr
      _ ≤ (logCounting (f a) ⊤ + ∑ x ∈ s, logCounting (f x) ⊤) r :=
        add_le_add (by trivial) (hs (fun a ha ↦ h₁f a (Finset.mem_insert_of_mem ha)))
Cleared hypotheses: s, h₁f
-- 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
r : ℝ
h₁f : ∀ a ∈ s, Meromorphic (f a)
hr : 1 ≤ r
⊢ logCounting.{u_1, u_2} (𝕜 := 𝕜) (E := E) (∑ a ∈ s, f a) ⊤ r ≤ (∑ a ∈ s, logCounting (f a) ⊤) r
have empty : ∀ (h₁f : ∀ (a : α), Membership.mem (γ := Finset α) ∅ a → Meromorphic (f a)),
  logCounting.{u_1, u_2} (𝕜 := 𝕜) (E := E) (∑ a ∈ ∅, f a) ⊤ r ≤ (∑ a ∈ ∅, logCounting (f a) ⊤) r
Tactic: classical
  induction s using Finset.induction with
  | empty =>
    simp
  | insert a s ha hs =>
    rw [Finset.sum_insert ha, Finset.sum_insert ha]
    calc logCounting (f a + ∑ x ∈ s, f x) ⊤ r
      _ ≤ (logCounting (f a) ⊤ + logCounting (∑ x ∈ s, f x) ⊤) r :=
        logCounting_add_top_le (h₁f a (Finset.mem_insert_self a s))
          (Meromorphic.sum (fun σ hσ ↦ h₁f σ (Finset.mem_insert_of_mem hσ))) hr
      _ ≤ (logCounting (f a) ⊤ + ∑ x ∈ s, logCounting (f x) ⊤) r :=
        add_le_add (by trivial) (hs (fun a ha ↦ h₁f a (Finset.mem_insert_of_mem ha)))
Cleared hypotheses: s, h₁f
-- 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
r : ℝ
h₁f : ∀ a ∈ s, Meromorphic (f a)
hr : 1 ≤ r
empty :
  ∀ (h₁f : ∀ (a : α), Membership.mem (γ := Finset α) ∅ a → Meromorphic (f a)),
    logCounting.{u_1, u_2} (𝕜 := 𝕜) (E := E) (∑ a ∈ ∅, f a) ⊤ r ≤ (∑ a ∈ ∅, logCounting (f a) ⊤) r
⊢ logCounting.{u_1, u_2} (𝕜 := 𝕜) (E := E) (∑ a ∈ s, f a) ⊤ r ≤ (∑ a ∈ s, logCounting (f a) ⊤) r
have insert : ∀ (a : α) (s : Finset α) (ha : a ∉ s)
  (hs :
    ∀ (h₁f : ∀ a ∈ s, Meromorphic (f a)),
      logCounting.{u_1, u_2} (𝕜 := 𝕜) (E := E) (∑ a ∈ s, f a) ⊤ r ≤ (∑ a ∈ s, logCounting (f a) ⊤) r)
  (h₁f : ∀ a_1 ∈ insert a s, Meromorphic (f a_1)),
  logCounting.{u_1, u_2} (𝕜 := 𝕜) (E := E) (∑ a ∈ insert a s, f a) ⊤ r ≤ (∑ a ∈ insert a s, logCounting (f a) ⊤) r
Tactic: classical
  induction s using Finset.induction with
  | empty =>
    simp
  | insert a s ha hs =>
    rw [Finset.sum_insert ha, Finset.sum_insert ha]
    calc logCounting (f a + ∑ x ∈ s, f x) ⊤ r
      _ ≤ (logCounting (f a) ⊤ + logCounting (∑ x ∈ s, f x) ⊤) r :=
        logCounting_add_top_le (h₁f a (Finset.mem_insert_self a s))
          (Meromorphic.sum (fun σ hσ ↦ h₁f σ (Finset.mem_insert_of_mem hσ))) hr
      _ ≤ (logCounting (f a) ⊤ + ∑ x ∈ s, logCounting (f x) ⊤) r :=
        add_le_add (by trivial) (hs (fun a ha ↦ h₁f a (Finset.mem_insert_of_mem ha)))
Cleared hypotheses: s, h₁f
-- 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)
⊢ logCounting.{u_1, u_2} (𝕜 := 𝕜) (E := E) (∑ a ∈ s, f a) ⊤ ≤ᶠ[atTop] ∑ a ∈ s, logCounting (f a) ⊤
have 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
Tactic: filter_upwards [eventually_ge_atTop 1] using fun _ hr ↦ logCounting_sum_top_le s f h₁f hr