awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
b : ℝ
obtain :
  ∀ (c : ℝ)
    (hc :
      ∀ b ≥ c,
        Norm.norm (E := ℝ) (1 b) ≤
          a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)),
    ∃ b_1 ≥ b, 1 < HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D b_1| : ℝ)
⊢ ∃ b_1 ≥ b, 1 < HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D b_1| : ℝ)

Tactic:
obtain ⟨c, hc⟩ := eventually_atTop.1
    (isLittleO_iff.1 (one_isLittleO_logCounting_single (e := e)) ha)

Premises used: Iff.mp, Asymptotics.isLittleO_iff, Function.locallyFinsuppWithin.one_isLittleO_logCounting_single, Filter.eventually_atTop
-- 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
b c : ℝ
hc :
  ∀ b ≥ c,
    Norm.norm (E := ℝ) (1 b) ≤
      a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
⊢ c ≤ ℓ

Tactic:
grind
-- 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
b c : ℝ
hc :
  ∀ b ≥ c,
    Norm.norm (E := ℝ) (1 b) ≤
      a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
⊢ c ≤ ℓ

Tactic:
have h₁ℓ : c ≤ ℓ := by grind
-- 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
b c : ℝ
hc :
  ∀ b ≥ c,
    Norm.norm (E := ℝ) (1 b) ≤
      a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
⊢ 1 ≤ ℓ

Tactic:
simp [ℓ]
-- 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
b c : ℝ
hc :
  ∀ b ≥ c,
    Norm.norm (E := ℝ) (1 b) ≤
      a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
⊢ 1 ≤ ℓ

Tactic:
have h₂ℓ : 1 ≤ ℓ := by simp [ℓ]
-- 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
b c : ℝ
hc :
  ∀ b ≥ c,
    Norm.norm (E := ℝ) (1 b) ≤
      a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
⊢ b ≤ 1 + ℓ

Tactic:
grind
-- 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
b c : ℝ
hc :
  ∀ b ≥ c,
    Norm.norm (E := ℝ) (1 b) ≤
      a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
right : 1 < HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D (1 + ℓ)| : ℝ)
⊢ ∃ b_1 ≥ b, 1 < HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D b_1| : ℝ)

Tactic:
use 1 + ℓ, (show b ≤ 1 + ℓ by grind)
-- 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
b c : ℝ
hc :
  ∀ b ≥ c,
    Norm.norm (E := ℝ) (1 b) ≤
      a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
⊢ 1 ≤ HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) ℓ| : ℝ)

Tactic:
simpa [h₁ℓ] using hc ℓ
-- 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
b c : ℝ
hc :
  ∀ b ≥ c,
    Norm.norm (E := ℝ) (1 b) ≤
      a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
hbc : LE.le (α := ℝ) (0 : ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) ℓ : ℝ)
hbc₁ :
  LE.le (α := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) ℓ : ℝ)
    ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D ℓ : ℝ)
⊢ HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) ℓ| : ℝ) ≤
    HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D ℓ| : ℝ)

Tactic:
gcongr
-- 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
b c : ℝ
hc :
  ∀ b ≥ c,
    Norm.norm (E := ℝ) (1 b) ≤
      a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
⊢ LE.le (α := ℝ) (0 : ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) ℓ : ℝ)

Tactic:
apply logCounting_nonneg (single_pos.2 Int.one_pos).le h₂ℓ

Premises used: Iff.mpr, Function.locallyFinsuppWithin.logCounting_nonneg, LT.lt.le, Function.locallyFinsuppWithin.single_pos, Int.one_pos
-- 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
b c : ℝ
hc :
  ∀ b ≥ c,
    Norm.norm (E := ℝ) (1 b) ≤
      a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
⊢ LE.le (α := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) ℓ : ℝ)
    ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D ℓ : ℝ)

Tactic:
apply logCounting_le he h₂ℓ

Premises used: Function.locallyFinsuppWithin.logCounting_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
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
b c : ℝ
hc :
  ∀ b ≥ c,
    Norm.norm (E := ℝ) (1 b) ≤
      a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
hbc :
  LT.lt (α := ℝ) (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D ℓ| : ℝ)
    (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D (1 + ℓ)| : ℝ)
⊢ HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D ℓ| : ℝ) <
    HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D (1 + ℓ)| : ℝ)

Tactic:
gcongr 2
-- 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
b c : ℝ
hc :
  ∀ b ≥ c,
    Norm.norm (E := ℝ) (1 b) ≤
      a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
⊢ 1 ≤ 1 + ℓ

Tactic:
grind
-- 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
b c : ℝ
hc :
  ∀ b ≥ c,
    Norm.norm (E := ℝ) (1 b) ≤
      a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
hbc :
  LT.lt (α := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D ℓ : ℝ)
    ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D (1 + ℓ) : ℝ)
⊢ LT.lt (α := ℝ) (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D ℓ| : ℝ)
    (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D (1 + ℓ)| : ℝ)

Tactic:
rw [abs_of_nonneg (logCounting_nonneg h h₂ℓ),
        abs_of_nonneg (logCounting_nonneg h (by grind))]

Premises used: Function.locallyFinsuppWithin.logCounting_nonneg, abs_of_nonneg
-- 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
b c : ℝ
hc :
  ∀ b ≥ c,
    Norm.norm (E := ℝ) (1 b) ≤
      a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
hbc : ℓ ∈ Ioi ‖e‖
hbc₁ : 1 + ℓ ∈ Ioi ‖e‖
hbc₂ : ℓ < 1 + ℓ
⊢ LT.lt (α := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D ℓ : ℝ)
    ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D (1 + ℓ) : ℝ)

Tactic:
apply logCounting_strictMono he

Premises used: Function.locallyFinsuppWithin.logCounting_strictMono
-- 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
b c : ℝ
hc :
  ∀ b ≥ c,
    Norm.norm (E := ℝ) (1 b) ≤
      a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
⊢ ℓ ∈ Ioi ‖e‖

Tactic:
grind
-- 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
b c : ℝ
hc :
  ∀ b ≥ c,
    Norm.norm (E := ℝ) (1 b) ≤
      a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
⊢ 1 + ℓ ∈ Ioi ‖e‖

Tactic:
grind
-- 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
b c : ℝ
hc :
  ∀ b ≥ c,
    Norm.norm (E := ℝ) (1 b) ≤
      a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
⊢ ℓ < 1 + ℓ

Tactic:
grind
-- 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
b c : ℝ
hc :
  ∀ b ≥ c,
    Norm.norm (E := ℝ) (1 b) ≤
      a * Norm.norm (E := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) b : ℝ)
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
h₁ℓ : c ≤ ℓ
h₂ℓ : 1 ≤ ℓ
calc : 1 ≤ HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) ℓ| : ℝ)
calc₁ :
  HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e 1) ℓ| : ℝ) ≤
    HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D ℓ| : ℝ)
calc₂ :
  HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D ℓ| : ℝ) <
    HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D (1 + ℓ)| : ℝ)
⊢ 1 < HMul.hMul (β := ℝ) a (|(logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D (1 + ℓ)| : ℝ)

Tactic:
calc 1
    _ ≤ (a * |logCounting (single e 1) ℓ|) := by simpa [h₁ℓ] using hc ℓ
    _ ≤ (a * |logCounting D ℓ|) := by
      gcongr
      · apply logCounting_nonneg (single_pos.2 Int.one_pos).le h₂ℓ
      · apply logCounting_le he h₂ℓ
    _ < a * |logCounting D (1 + ℓ)| := by
      gcongr 2
      rw [abs_of_nonneg (logCounting_nonneg h h₂ℓ),
        abs_of_nonneg (logCounting_nonneg h (by grind))]
      apply logCounting_strictMono he <;> grind

Premises used: HMul.hMul, abs, Function.locallyFinsuppWithin.single, Function.locallyFinsuppWithin.logCounting, HAdd.hAdd, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : 𝕜 → E
h : Meromorphic f
rw :
  Eq (α := locallyFinsuppWithin (X := 𝕜) univ ℤ) (MeromorphicOn.divisor f univ)⁻ 0 ↔
    AnalyticOnNhd 𝕜 (toMeromorphicNFOn f univ) univ
rw₁ :
  LE.le (α := locallyFinsuppWithin (X := 𝕜) univ ℤ) 0 (MeromorphicOn.divisor f univ) ↔
    AnalyticOnNhd 𝕜 (toMeromorphicNFOn f univ) univ
rw₂ :
  LE.le (α := locallyFinsuppWithin (X := 𝕜) univ ℤ) 0 (MeromorphicOn.divisor (toMeromorphicNFOn f univ) univ) ↔
    AnalyticOnNhd 𝕜 (toMeromorphicNFOn f univ) univ
rw₃ rw₄ : AnalyticOnNhd 𝕜 (toMeromorphicNFOn f univ) univ ↔ AnalyticOnNhd 𝕜 (toMeromorphicNFOn f univ) univ
⊢ IsBigO (α := ℝ) (E := ℝ) (F := ℝ) atTop
      ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ) (MeromorphicOn.divisor f univ)⁻) 1 ↔
    AnalyticOnNhd 𝕜 (toMeromorphicNFOn f univ) univ

Tactic:
rw [← locallyFinsuppWithin.zero_iff_logCounting_bounded (negPart_nonneg _), negPart_eq_zero,
    ← h.meromorphicOn.divisor_of_toMeromorphicNFOn,
    (meromorphicNFOn_toMeromorphicNFOn _ _).divisor_nonneg_iff_analyticOnNhd]

Premises used: Function.locallyFinsuppWithin.zero_iff_logCounting_bounded, Meromorphic.meromorphicOn, meromorphicNFOn_toMeromorphicNFOn, MeromorphicOn.divisor_of_toMeromorphicNFOn, MeromorphicNFOn.divisor_nonneg_iff_analyticOnNhd, negPart_nonneg, negPart_eq_zero
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
r : ℝ
h : Subset.{u_1} (α := Set E) (closedBall 0 |r|) univ
⊢ locallyFinsupp E ℤ →+ locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ

Tactic:
apply restrictMonoidHom

Premises used: Function.locallyFinsuppWithin.restrictMonoidHom
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
r : ℝ
h h₁ h₂ h₃ h₄ h₅ h₆ h₇ :
  ∀ ⦃a : E⦄, Membership.mem (γ := Set E) (closedBall 0 |r|) a → Membership.mem (γ := Set E) univ a
⊢ Subset.{u_1} (α := Set E) (closedBall 0 |r|) univ

Tactic:
tauto
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
r : ℝ
z : E
f : locallyFinsupp E ℤ
ha : Membership.mem (γ := Set E) (closedBall 0 |r|) z
⊢ Eq (α := ℤ)
    ((((restrictMonoidHom (U := univ) (V := closedBall 0 |r|) ⋯ :
                (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ)
              f :
            locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
          (a : E) → ℤ)
        z :
      ℤ)
    ((f : (a : E) → ℤ) z : ℤ)

Tactic:
simp_all [restrict_apply]

Premises used: Function.locallyFinsuppWithin.restrict_apply
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
r : ℝ
f : ℂ → ℂ
h : Meromorphic f
⊢ Eq (α := locallyFinsuppWithin (X := ℂ) (closedBall 0 |r|) ℤ) (divisor f (closedBall 0 |r|))
    ((toClosedBall r : (a : locallyFinsupp ℂ ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) (divisor f univ))

Tactic:
simp_all [locallyFinsuppWithin.toClosedBall]

Premises used: Function.locallyFinsuppWithin.toClosedBall
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
r : ℝ
f : locallyFinsupp E ℤ
⊢ Subset.{u_2} (α := Set E)
    (support (U := closedBall 0 |r|) (Y := ℤ)
      ((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) f))
    (closedBall 0 |r|)

Tactic:
simp_all [toClosedBall, restrict_apply]

Premises used: Function.locallyFinsuppWithin.restrict_apply, Function.locallyFinsuppWithin.toClosedBall
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : ProperSpace E
⊢ Eq (α := ℝ → ℝ)
    (fun (r : ℝ) ↦
      ∑ᶠ (z : E),
          (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) 0 :
                      locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                    (a : E) → ℤ)
                  z) :
              ℝ) *
            log (r * ‖z‖⁻¹) +
        (↑((0 : (a : E) → ℤ) 0) : ℝ) * log r)
    0

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
simp :
  (fun (r : ℝ) ↦
      ∑ᶠ (z : E),
          HAdd.hAdd (α := ℝ)
              (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₁ :
                        locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                      (a : E) → ℤ)
                    z) :
                ℝ)
              (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₂ :
                        locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                      (a : E) → ℤ)
                    z) :
                ℝ) *
            log (r * ‖z‖⁻¹) +
        HAdd.hAdd (α := ℝ) (↑((D₁ : (a : E) → ℤ) 0) : ℝ) (↑((D₂ : (a : E) → ℤ) 0) : ℝ) * log r) =
    HAdd.hAdd (α := ℝ → ℝ)
      (fun (r : ℝ) ↦
        ∑ᶠ (z : E),
            (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₁ :
                        locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                      (a : E) → ℤ)
                    z) :
                ℝ) *
              log (r * ‖z‖⁻¹) +
          (↑((D₁ : (a : E) → ℤ) 0) : ℝ) * log r)
      fun (r : ℝ) ↦
      ∑ᶠ (z : E),
          (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₂ :
                      locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                    (a : E) → ℤ)
                  z) :
              ℝ) *
            log (r * ‖z‖⁻¹) +
        (↑((D₂ : (a : E) → ℤ) 0) : ℝ) * log r
⊢ (fun (r : ℝ) ↦
      ∑ᶠ (z : E),
          (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) (D₁ + D₂) :
                      locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                    (a : E) → ℤ)
                  z) :
              ℝ) *
            log (r * ‖z‖⁻¹) +
        (↑((D₁ + D₂ : (a : E) → ℤ) 0) : ℝ) * log r) =
    HAdd.hAdd (α := ℝ → ℝ)
      (fun (r : ℝ) ↦
        ∑ᶠ (z : E),
            (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₁ :
                        locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                      (a : E) → ℤ)
                    z) :
                ℝ) *
              log (r * ‖z‖⁻¹) +
          (↑((D₁ : (a : E) → ℤ) 0) : ℝ) * log r)
      fun (r : ℝ) ↦
      ∑ᶠ (z : E),
          (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₂ :
                      locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                    (a : E) → ℤ)
                  z) :
              ℝ) *
            log (r * ‖z‖⁻¹) +
        (↑((D₂ : (a : E) → ℤ) 0) : ℝ) * log r

Tactic:
simp only [map_add, coe_add, Pi.add_apply, Int.cast_add]

Premises used: Int.cast_add, map_add, Pi.add_apply, Function.locallyFinsuppWithin.coe_add
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r A B C D : ℝ
⊢ A + B + (C + D) = A + C + (B + D)

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
⊢ ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)

Tactic:
have {A B C D : ℝ} : A + B + (C + D) = A + C + (B + D) := by ring
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h :
  ∑ᶠ (z : E),
      HAdd.hAdd (α := ℝ)
          (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₁ :
                    locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                  (a : E) → ℤ)
                z) :
            ℝ)
          (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₂ :
                    locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                  (a : E) → ℤ)
                z) :
            ℝ) *
        log (r * ‖z‖⁻¹) =
    HAdd.hAdd (α := ℝ)
      (∑ᶠ (z : E),
        (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₁ :
                    locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                  (a : E) → ℤ)
                z) :
            ℝ) *
          log (r * ‖z‖⁻¹))
      (∑ᶠ (z : E),
        (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₂ :
                    locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                  (a : E) → ℤ)
                z) :
            ℝ) *
          log (r * ‖z‖⁻¹))
h₁ :
  HAdd.hAdd (α := ℝ) (↑((D₁ : (a : E) → ℤ) 0) : ℝ) (↑((D₂ : (a : E) → ℤ) 0) : ℝ) * log r =
    (↑((D₁ : (a : E) → ℤ) 0) : ℝ) * log r + (↑((D₂ : (a : E) → ℤ) 0) : ℝ) * log r
⊢ ∑ᶠ (z : E),
        HAdd.hAdd (α := ℝ)
            (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₁ :
                      locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                    (a : E) → ℤ)
                  z) :
              ℝ)
            (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₂ :
                      locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                    (a : E) → ℤ)
                  z) :
              ℝ) *
          log (r * ‖z‖⁻¹) +
      HAdd.hAdd (α := ℝ) (↑((D₁ : (a : E) → ℤ) 0) : ℝ) (↑((D₂ : (a : E) → ℤ) 0) : ℝ) * log r =
    HAdd.hAdd (α := ℝ)
        (∑ᶠ (z : E),
          (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₁ :
                      locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                    (a : E) → ℤ)
                  z) :
              ℝ) *
            log (r * ‖z‖⁻¹))
        (∑ᶠ (z : E),
          (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₂ :
                      locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                    (a : E) → ℤ)
                  z) :
              ℝ) *
            log (r * ‖z‖⁻¹)) +
      ((↑((D₁ : (a : E) → ℤ) 0) : ℝ) * log r + (↑((D₂ : (a : E) → ℤ) 0) : ℝ) * log r)

Tactic:
congr 1