awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
f : locallyFinsupp E ℤ
r : ℝ
h : 0 ≤ f
hr : 1 ≤ r
h₃r : 0 < r
a : E
h₁a : ¬a = 0
h₂a : a ∉ closedBall 0 |r|
⊢ 0 ≤
    (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) f :
                locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
              (a : E) → ℤ)
            a) :
        ℝ) *
      log (r * ‖a‖⁻¹)

Tactic:
simp [apply_eq_zero_of_notMem ((toClosedBall r) _) h₂a]

Premises used: Function.locallyFinsuppWithin.apply_eq_zero_of_notMem, DFunLike.coe, Function.locallyFinsuppWithin.toClosedBall
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
f₁ f₂ : locallyFinsupp E ℤ
r : ℝ
h : f₁ ≤ f₂
hr : 1 ≤ r
rw :
  ∀ (h : 0 ≤ f₂ - f₁) (hr : 1 ≤ r),
    0 ≤
      HSub.hSub (α := ℝ) (β := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) f₂ r : ℝ)
        ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) f₁ r : ℝ)
⊢ LE.le (α := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) f₁ r : ℝ)
    ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) f₂ r : ℝ)

Tactic:
rw [← sub_nonneg] at h ⊢

Premises used: sub_nonneg
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
f₁ f₂ : locallyFinsupp E ℤ
r : ℝ
h : 0 ≤ f₂ - f₁
hr : 1 ≤ r
⊢ 0 ≤
    HSub.hSub (α := ℝ) (β := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) f₂ r : ℝ)
      ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) f₁ r : ℝ)

Tactic:
simpa using logCounting_nonneg h hr

Premises used: Function.locallyFinsuppWithin.logCounting_nonneg
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
f₁ f₂ : locallyFinsupp E ℤ
h : f₁ ≤ f₂
⊢ ∀ (a : ℝ),
    1 ≤ a →
      LE.le (α := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) f₁ a : ℝ)
        ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) f₂ a : ℝ)

Tactic:
fun _ hr ↦ logCounting_le h hr

Premises used: Function.locallyFinsuppWithin.logCounting_le
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
f₁ f₂ : locallyFinsupp E ℤ
h : f₁ ≤ f₂
h₁ :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 1 ≤ x) x} x →
          Membership.mem (γ := Set ℝ)
            {x : ℝ |
              (fun (x : ℝ) ↦
                  LE.le (α := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) f₁ x : ℝ)
                    ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) f₂ x : ℝ))
                x}
            x}
      a
h₂ :
  ∀ (a : ℝ),
    1 ≤ a →
      LE.le (α := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) f₁ a : ℝ)
        ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) f₂ a : ℝ)
⊢ EventuallyLE (α := ℝ) (β := ℝ) atTop ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) f₁)
    ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) f₂)

Tactic:
filter_upwards [eventually_ge_atTop 1] using fun _ hr ↦ logCounting_le h hr

Premises used: Filter.eventually_ge_atTop, Function.locallyFinsuppWithin.logCounting_le, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
a : WithTop E
a₀ : E
pos : (h : a = ⊤) → ℝ → ℝ
neg : (h : ¬a = ⊤) → ℝ → ℝ
⊢ ℝ → ℝ

Tactic:
by_cases h : a = ⊤
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
a : WithTop E
a₀ : E
h : a = ⊤
⊢ ℝ → ℝ

Tactic:
exact (divisor f univ)⁻.logCounting

Premises used: Set.univ, Function.locallyFinsuppWithin.logCounting, MeromorphicOn.divisor, DFunLike.coe, NegPart.negPart
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
U : Set 𝕜
f g : 𝕜 → E
a : WithTop E
a₀ : E
h : ¬a = ⊤
⊢ ℝ → ℝ

Tactic:
exact (divisor (f · - a.untop₀) univ)⁺.logCounting

Premises used: WithTop.untop₀, Set.univ, HSub.hSub, Function.locallyFinsuppWithin.logCounting, PosPart.posPart, MeromorphicOn.divisor, DFunLike.coe
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
f : ℂ → ℂ
⊢ (locallyFinsuppWithin.logCounting : (a : locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f univ) =
    logCounting f 0 - logCounting f ⊤

Tactic:
simp [logCounting, ← locallyFinsuppWithin.logCounting.map_sub]

Premises used: ValueDistribution.logCounting, Function.locallyFinsuppWithin.logCounting, AddMonoidHom.map_sub
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : 𝕜 → E
a₀ : E
⊢ logCounting f (↑a₀ : WithTop E) =
    (locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
      (divisor.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ f x - a₀) univ)⁺

Tactic:
simp [logCounting]

Premises used: ValueDistribution.logCounting
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : 𝕜 → E
a₀ : E
⊢ logCounting f (↑a₀ : WithTop E) = logCounting (f - fun (x : 𝕜) ↦ a₀) 0

Tactic:
simp [logCounting]

Premises used: ValueDistribution.logCounting
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : 𝕜 → E
⊢ logCounting f 0 = (locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ) (divisor f univ)⁺

Tactic:
simp [logCounting]

Premises used: ValueDistribution.logCounting
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : 𝕜 → E
⊢ logCounting f ⊤ = (locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ) (divisor f univ)⁻

Tactic:
simp [logCounting]

Premises used: ValueDistribution.logCounting
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : 𝕜 → E
a : WithTop E
pos : ∀ (h : a = ⊤), logCounting f a 0 = 0
neg : ∀ (h : ¬a = ⊤), logCounting f a 0 = 0
⊢ logCounting f a 0 = 0

Tactic:
by_cases h : a = ⊤
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : 𝕜 → E
a : WithTop E
h : a = ⊤
⊢ logCounting f a 0 = 0

Tactic:
simp [logCounting, h]

Premises used: ValueDistribution.logCounting
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : 𝕜 → E
a : WithTop E
h : ¬a = ⊤
⊢ logCounting f a 0 = 0

Tactic:
simp [logCounting, h]

Premises used: ValueDistribution.logCounting
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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)⁻ : ℝ → ℝ)
rw₃ 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)⁻ : ℝ → ℝ)
⊢ (locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ) (divisor f univ) =
    logCounting f 0 - logCounting f ⊤

Tactic:
rw [← posPart_sub_negPart (divisor f univ), logCounting_zero, logCounting_top, map_sub]

Premises used: ValueDistribution.logCounting_zero, map_sub, ValueDistribution.logCounting_top, Set.univ, MeromorphicOn.divisor, posPart_sub_negPart
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
c : E
e : WithTop E
⊢ logCounting (fun (x : 𝕜) ↦ c) e = 0

Tactic:
simp [logCounting]

Premises used: ValueDistribution.logCounting
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
e : WithTop E
⊢ logCounting.{u_1, u_2} (𝕜 := 𝕜) 0 e = 0

Tactic:
logCounting_const

Premises used: ValueDistribution.logCounting_const
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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
neg : ∀ (h : ¬e = ⊤), logCounting f e (-r) = logCounting f e r
⊢ logCounting f e (-r) = logCounting f e r

Tactic:
by_cases h : e = ⊤
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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 : ℝ
h : e = ⊤
⊢ logCounting f e (-r) = logCounting f e r

Tactic:
simp [logCounting, h, locallyFinsuppWithin.logCounting_even _ r]

Premises used: ValueDistribution.logCounting, Function.locallyFinsuppWithin.logCounting_even
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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 : ℝ
h : ¬e = ⊤
⊢ logCounting f e (-r) = logCounting f e r

Tactic:
simp [logCounting, h, locallyFinsuppWithin.logCounting_even _ r]

Premises used: ValueDistribution.logCounting, Function.locallyFinsuppWithin.logCounting_even
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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)
neg : ∀ (h : ¬e = ⊤), MonotoneOn (logCounting f e) (Ioi 0)
⊢ MonotoneOn (logCounting f e) (Ioi 0)

Tactic:
by_cases h : e = ⊤
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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 : e = ⊤
⊢ LE.le (α := locallyFinsupp 𝕜 ℤ) 0 (divisor f univ)⁻

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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 : e = ⊤
⊢ MonotoneOn (logCounting f e) (Ioi 0)

Tactic:
simpa [logCounting, h] using locallyFinsuppWithin.logCounting_mono (by positivity)

Premises used: ValueDistribution.logCounting, Function.locallyFinsuppWithin.logCounting_mono
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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 : ¬e = ⊤
⊢ LE.le.{u_1} (α := locallyFinsupp 𝕜 ℤ) 0 (divisor.{u_1, u_2} (E := E) (fun (x : 𝕜) ↦ f x - e.untop₀) univ)⁺

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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 : ¬e = ⊤
⊢ MonotoneOn (logCounting f e) (Ioi 0)

Tactic:
simpa [logCounting, h] using locallyFinsuppWithin.logCounting_mono (by positivity)

Premises used: ValueDistribution.logCounting, Function.locallyFinsuppWithin.logCounting_mono
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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
neg : ∀ (h : ¬e = ⊤), 0 ≤ logCounting f e r
⊢ 0 ≤ logCounting f e r

Tactic:
by_cases h : e = ⊤
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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
h : e = ⊤
⊢ 0 ≤ logCounting f e r

Tactic:
simp [logCounting, h, locallyFinsuppWithin.logCounting_nonneg
      (negPart_nonneg (divisor f univ)) hr]

Premises used: Function.locallyFinsuppWithin.logCounting_nonneg, ValueDistribution.logCounting, Set.univ, MeromorphicOn.divisor, negPart_nonneg
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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
h : ¬e = ⊤
⊢ 0 ≤ logCounting f e r

Tactic:
simp [logCounting, h, locallyFinsuppWithin.logCounting_nonneg
      (posPart_nonneg (divisor (f · - e.untop₀) univ)) hr]

Premises used: WithTop.untop₀, Function.locallyFinsuppWithin.logCounting_nonneg, ValueDistribution.logCounting, Set.univ, posPart_nonneg, HSub.hSub, MeromorphicOn.divisor
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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
x : ℝ
hr : 1 ≤ x
⊢ 0 x ≤ logCounting f e x

Tactic:
simp [logCounting_nonneg hr]

Premises used: ValueDistribution.logCounting_nonneg
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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
h₁ : ∀ (a : ℝ), 1 ≤ a → 0 a ≤ logCounting f e a
⊢ 0 ≤ᶠ[atTop] logCounting f e

Tactic:
filter_upwards [eventually_ge_atTop 1] using fun _ hr ↦ by simp [logCounting_nonneg hr]

Premises used: Filter.eventually_ge_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : ℂ → E
hfg : f =ᶠ[codiscrete ℂ] g
h : ∀ (a : WithTop E), logCounting f a = logCounting g a
⊢ logCounting f = logCounting g

Tactic:
ext a : 1
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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
neg : ∀ (h : ¬a = ⊤), logCounting f a = logCounting g a
⊢ logCounting f a = logCounting g a

Tactic:
by_cases h : a = ⊤
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : ℂ → E
hfg : f =ᶠ[codiscrete ℂ] g
a : WithTop E
h : a = ⊤
pos :
  Eq (α := ℝ → ℝ) ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f univ)⁻ : ℝ → ℝ)
    ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor g univ)⁻ : ℝ → ℝ)
⊢ logCounting f a = logCounting g a

Tactic:
simp only [logCounting, h, ↓reduceDIte]

Premises used: ValueDistribution.logCounting, reduceDIte
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : ℂ → E
hfg : f =ᶠ[codiscrete ℂ] g
a : WithTop E
h : a = ⊤
pos : Eq (α := locallyFinsupp ℂ ℤ) (divisor f univ) (divisor g univ)
⊢ Eq (α := ℝ → ℝ) ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f univ)⁻ : ℝ → ℝ)
    ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor g univ)⁻ : ℝ → ℝ)

Tactic:
congr 2
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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 f univ) (divisor g univ)

Tactic:
divisor_congr_codiscreteWithin hfg isOpen_univ

Premises used: isOpen_univ, MeromorphicOn.divisor_congr_codiscreteWithin
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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 f univ) (divisor g univ)

Tactic:
exact divisor_congr_codiscreteWithin hfg isOpen_univ

Premises used: isOpen_univ, MeromorphicOn.divisor_congr_codiscreteWithin
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : ℂ → E
hfg : f =ᶠ[codiscrete ℂ] g
a : WithTop E
h : ¬a = ⊤
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)⁺ :
      ℝ → ℝ)
⊢ logCounting f a = logCounting g a

Tactic:
simp only [logCounting, h, ↓reduceDIte]

Premises used: ValueDistribution.logCounting, reduceDIte
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : ℂ → E
hfg : f =ᶠ[codiscrete ℂ] g
a : WithTop E
h : ¬a = ⊤
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)
⊢ 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:
congr 2
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : ℂ → E
hfg : f =ᶠ[codiscrete ℂ] g
a : WithTop E
h : ¬a = ⊤
apply :
  EventuallyEq.{0, u_2} (β := E) (codiscreteWithin univ) (fun (x : ℂ) ↦ f x - a.untop₀) fun (x : ℂ) ↦ g x - a.untop₀
⊢ 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:
apply divisor_congr_codiscreteWithin _ isOpen_univ

Premises used: isOpen_univ, MeromorphicOn.divisor_congr_codiscreteWithin
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : ℂ → E
hfg : f =ᶠ[codiscrete ℂ] g
a : WithTop E
h : ¬a = ⊤
⊢ ∀ (a_1 : ℂ), f a_1 = g a_1 → f a_1 - a.untop₀ = g a_1 - a.untop₀

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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
h₂ : ∀ (a_1 : ℂ), f a_1 = g a_1 → f a_1 - a.untop₀ = g a_1 - a.untop₀
⊢ EventuallyEq.{0, u_2} (β := E) (codiscreteWithin univ) (fun (x : ℂ) ↦ f x - a.untop₀) fun (x : ℂ) ↦ g x - a.untop₀

Tactic:
filter_upwards [hfg] using by simp
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
f : 𝕜 → 𝕜
⊢ logCounting f⁻¹ ⊤ = logCounting f 0

Tactic:
simp [logCounting_zero, logCounting_top]

Premises used: ValueDistribution.logCounting_zero, ValueDistribution.logCounting_top
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
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
rw rw₁ :
  Eq (α := ℝ → ℝ) ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ) (divisor f univ)⁻ : ℝ → ℝ)
    ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ) (divisor f univ)⁻ : ℝ → ℝ)
⊢ Eq (α := ℝ → ℝ)
    ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ) (divisor (f + g) 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)]

Premises used: MeromorphicOn.negPart_divisor_add_of_analyticNhdOn_right, Meromorphic.meromorphicOn, isOpen_univ, IsOpen.analyticOn_iff_analyticOnNhd, Iff.mp
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : 𝕜 → E
a₀ : E
hf : Meromorphic f
⊢ logCounting (f + fun (x : 𝕜) ↦ a₀) ⊤ = logCounting f ⊤

Tactic:
apply logCounting_add_analyticOn hf analyticOn_const

Premises used: ValueDistribution.logCounting_add_analyticOn, analyticOn_const