awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
simpa [sub_eq_add_neg] using logCounting_add_const hf

Premises used: sub_eq_add_neg, ValueDistribution.logCounting_add_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₁ f₂ : 𝕜 → E
r : ℝ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
hr : 1 ≤ r
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 :
      ℝ)
⊢ (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

Tactic:
rw [← locallyFinsuppWithin.logCounting.map_add]

Premises used: Function.locallyFinsuppWithin.logCounting, AddMonoidHom.map_add
-- 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₁ f₂ : 𝕜 → E
r : ℝ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
hr : 1 ≤ r
⊢ 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:
locallyFinsuppWithin.logCounting_le
    (negPart_divisor_add_le_add h₁f₁.meromorphicOn h₁f₂.meromorphicOn) hr

Premises used: Meromorphic.meromorphicOn, Function.locallyFinsuppWithin.logCounting_le, MeromorphicOn.negPart_divisor_add_le_add
-- 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₁ f₂ : 𝕜 → E
r : ℝ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
hr : 1 ≤ r
⊢ 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:
exact locallyFinsuppWithin.logCounting_le
    (negPart_divisor_add_le_add h₁f₁.meromorphicOn h₁f₂.meromorphicOn) hr

Premises used: Meromorphic.meromorphicOn, Function.locallyFinsuppWithin.logCounting_le, MeromorphicOn.negPart_divisor_add_le_add
-- 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₁ f₂ : 𝕜 → E
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
⊢ ∀ (a : ℝ), 1 ≤ a → logCounting (f₁ + f₂) ⊤ a ≤ (logCounting f₁ ⊤ + logCounting f₂ ⊤) a

Tactic:
fun _ hr ↦ logCounting_add_top_le h₁f₁ h₁f₂ hr

Premises used: ValueDistribution.logCounting_add_top_le
-- 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₁ 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
h₁ : ∀ (a : ℝ), 1 ≤ a → logCounting (f₁ + f₂) ⊤ a ≤ (logCounting f₁ ⊤ + logCounting f₂ ⊤) a
⊢ logCounting (f₁ + f₂) ⊤ ≤ᶠ[atTop] logCounting f₁ ⊤ + logCounting f₂ ⊤

Tactic:
filter_upwards [eventually_ge_atTop 1] using fun _ hr ↦ logCounting_add_top_le h₁f₁ h₁f₂ hr

Premises used: ValueDistribution.logCounting_add_top_le, Filter.eventually_ge_atTop, 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
α : Type u_3
f : α → 𝕜 → E
r : ℝ
hr : 1 ≤ r
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:
simp
-- 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
α : 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.insert a s, Meromorphic (f a_1)
insert :
  logCounting (f a + ∑ x ∈ s, f x) ⊤ r ≤ HAdd.hAdd (β := ℝ → ℝ) (logCounting (f a) ⊤) (∑ x ∈ s, logCounting (f x) ⊤) r
⊢ logCounting.{u_1, u_2} (𝕜 := 𝕜) (E := E) (∑ a ∈ Insert.insert a s, f a) ⊤ r ≤
    (∑ a ∈ Insert.insert a s, logCounting (f a) ⊤) r

Tactic:
rw [Finset.sum_insert ha, Finset.sum_insert ha]

Premises used: Finset.sum_insert
-- 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
α : 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 (f a + ∑ x ∈ s, f x) ⊤ r ≤
    (logCounting (f a) ⊤ + logCounting.{u_1, u_2} (𝕜 := 𝕜) (E := E) (∑ x ∈ s, f x) ⊤) r

Tactic:
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

Premises used: Finset.mem_insert_self, ValueDistribution.logCounting_add_top_le, Finset.mem_insert_of_mem, Meromorphic.sum
-- 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
α : 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 (f a) ⊤ r ≤ logCounting (f a) ⊤ r

Tactic:
trivial
-- 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
α : 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 (f a + ∑ x ∈ s, f x) ⊤ r ≤ HAdd.hAdd (β := ℝ → ℝ) (logCounting (f a) ⊤) (∑ x ∈ s, logCounting (f x) ⊤) r

Tactic:
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)))

Premises used: Finset.mem_insert_self, ValueDistribution.logCounting_add_top_le, ValueDistribution.logCounting, add_le_add, Finset.mem_insert_of_mem, HAdd.hAdd, Meromorphic.sum, Top.top, Finset.sum
-- 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
α : 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
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.insert a s, Meromorphic (f a_1)),
    logCounting.{u_1, u_2} (𝕜 := 𝕜) (E := E) (∑ a ∈ Insert.insert a s, f a) ⊤ r ≤
      (∑ a ∈ Insert.insert a s, logCounting (f a) ⊤) r
⊢ logCounting.{u_1, u_2} (𝕜 := 𝕜) (E := E) (∑ a ∈ s, f a) ⊤ r ≤ (∑ 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)))

Premises used: Insert.insert
-- 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
α : 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
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.insert a s, Meromorphic (f a_1)),
    logCounting.{u_1, u_2} (𝕜 := 𝕜) (E := E) (∑ a ∈ Insert.insert a s, f a) ⊤ r ≤
      (∑ a ∈ Insert.insert a s, logCounting (f a) ⊤) r
⊢ logCounting.{u_1, u_2} (𝕜 := 𝕜) (E := E) (∑ a ∈ s, f a) ⊤ r ≤ (∑ 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)))

Premises used: Insert.insert
-- 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
α : Type u_3
s : Finset α
f : α → 𝕜 → E
h₁f : ∀ a ∈ s, Meromorphic (f a)
⊢ ∀ (a : ℝ), 1 ≤ a → logCounting.{u_1, u_2} (𝕜 := 𝕜) (E := E) (∑ a ∈ s, f a) ⊤ a ≤ (∑ a ∈ s, logCounting (f a) ⊤) a

Tactic:
fun _ hr ↦ logCounting_sum_top_le s f h₁f hr

Premises used: ValueDistribution.logCounting_sum_top_le
-- 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
α : Type u_3
s : Finset α
f : α → 𝕜 → E
h₁f : ∀ 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 : ℝ) ↦
                  logCounting.{u_1, u_2} (𝕜 := 𝕜) (E := E) (∑ a ∈ s, f a) ⊤ x ≤ (∑ a ∈ s, logCounting (f a) ⊤) x)
                x}
            x}
      a
h₁ : ∀ (a : ℝ), 1 ≤ a → logCounting.{u_1, u_2} (𝕜 := 𝕜) (E := E) (∑ a ∈ s, f a) ⊤ a ≤ (∑ a ∈ s, logCounting (f a) ⊤) a
⊢ logCounting.{u_1, u_2} (𝕜 := 𝕜) (E := E) (∑ a ∈ s, f a) ⊤ ≤ᶠ[atTop] ∑ a ∈ s, logCounting (f a) ⊤

Tactic:
filter_upwards [eventually_ge_atTop 1] using fun _ hr ↦ logCounting_sum_top_le s f h₁f hr

Premises used: ValueDistribution.logCounting_sum_top_le, Filter.eventually_ge_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
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 ≠ ⊤
simp :
  (locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
      (divisor (E := 𝕜) (fun (x : 𝕜) ↦ (f₁ * f₂) x) univ)⁺ r ≤
    HAdd.hAdd (α := ℝ → ℝ) (β := ℝ → ℝ)
      ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
          (divisor (E := 𝕜) (fun (x : 𝕜) ↦ f₁ x) univ)⁺ :
        ℝ → ℝ)
      ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
          (divisor (E := 𝕜) (fun (x : 𝕜) ↦ f₂ x) univ)⁺ :
        ℝ → ℝ)
      r
⊢ logCounting (f₁ * f₂) 0 r ≤ (logCounting f₁ 0 + logCounting f₂ 0) r

Tactic:
simp only [logCounting, WithTop.zero_ne_top, reduceDIte, WithTop.untop₀_zero, sub_zero]

Premises used: WithTop.untop₀_zero, sub_zero, ValueDistribution.logCounting, reduceDIte, WithTop.zero_ne_top
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
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 ≠ ⊤
rw :
  LE.le (α := ℝ)
    ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
        (HAdd.hAdd (α := locallyFinsuppWithin (X := 𝕜) univ ℤ) (divisor f₁ univ) (divisor f₂ univ))⁺ r :
      ℝ)
    ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
        (HAdd.hAdd (α := locallyFinsupp 𝕜 ℤ) (divisor (E := 𝕜) (fun (x : 𝕜) ↦ f₁ x) univ)⁺
          (divisor (E := 𝕜) (fun (x : 𝕜) ↦ f₂ x) univ)⁺)
        r :
      ℝ)
⊢ (locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
      (divisor (E := 𝕜) (fun (x : 𝕜) ↦ (f₁ * f₂) x) univ)⁺ r ≤
    HAdd.hAdd (α := ℝ → ℝ) (β := ℝ → ℝ)
      ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
          (divisor (E := 𝕜) (fun (x : 𝕜) ↦ f₁ x) univ)⁺ :
        ℝ → ℝ)
      ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
          (divisor (E := 𝕜) (fun (x : 𝕜) ↦ f₂ x) univ)⁺ :
        ℝ → ℝ)
      r

Tactic:
rw [divisor_mul h₁f₁.meromorphicOn h₁f₂.meromorphicOn (fun z _ ↦ h₂f₁ z) (fun z _ ↦ h₂f₂ z),
    ← locallyFinsuppWithin.logCounting.map_add]

Premises used: Function.locallyFinsuppWithin.logCounting, Meromorphic.meromorphicOn, AddMonoidHom.map_add, MeromorphicOn.divisor_mul
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
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 ≠ ⊤
apply :
  (HAdd.hAdd (α := locallyFinsuppWithin (X := 𝕜) univ ℤ) (divisor f₁ univ) (divisor f₂ univ))⁺ ≤
    HAdd.hAdd (α := locallyFinsupp 𝕜 ℤ) (divisor (E := 𝕜) (fun (x : 𝕜) ↦ f₁ x) univ)⁺
      (divisor (E := 𝕜) (fun (x : 𝕜) ↦ f₂ x) univ)⁺
⊢ LE.le (α := ℝ)
    ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
        (HAdd.hAdd (α := locallyFinsuppWithin (X := 𝕜) univ ℤ) (divisor f₁ univ) (divisor f₂ univ))⁺ r :
      ℝ)
    ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
        (HAdd.hAdd (α := locallyFinsupp 𝕜 ℤ) (divisor (E := 𝕜) (fun (x : 𝕜) ↦ f₁ x) univ)⁺
          (divisor (E := 𝕜) (fun (x : 𝕜) ↦ f₂ x) univ)⁺)
        r :
      ℝ)

Tactic:
apply locallyFinsuppWithin.logCounting_le _ hr

Premises used: Function.locallyFinsuppWithin.logCounting_le
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
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 ≠ ⊤
⊢ (HAdd.hAdd (α := locallyFinsuppWithin (X := 𝕜) univ ℤ) (divisor f₁ univ) (divisor f₂ univ))⁺ ≤
    HAdd.hAdd (α := locallyFinsupp 𝕜 ℤ) (divisor (E := 𝕜) (fun (x : 𝕜) ↦ f₁ x) univ)⁺
      (divisor (E := 𝕜) (fun (x : 𝕜) ↦ f₂ x) univ)⁺

Tactic:
apply locallyFinsuppWithin.posPart_add

Premises used: Function.locallyFinsuppWithin.posPart_add
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
f₁ f₂ : 𝕜 → 𝕜
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤
⊢ ∀ (a : ℝ), 1 ≤ a → logCounting (f₁ * f₂) 0 a ≤ (logCounting f₁ 0 + logCounting f₂ 0) a

Tactic:
fun _ hr ↦ logCounting_mul_zero_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂

Premises used: ValueDistribution.logCounting_mul_zero_le
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
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 : ℝ) ↦ logCounting (f₁ * f₂) 0 x ≤ (logCounting f₁ 0 + logCounting f₂ 0) x) x} x}
      a
h₁ : ∀ (a : ℝ), 1 ≤ a → logCounting (f₁ * f₂) 0 a ≤ (logCounting f₁ 0 + logCounting f₂ 0) a
⊢ logCounting (f₁ * f₂) 0 ≤ᶠ[atTop] logCounting f₁ 0 + logCounting f₂ 0

Tactic:
filter_upwards [eventually_ge_atTop 1] using
    fun _ hr ↦ logCounting_mul_zero_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂

Premises used: Filter.eventually_ge_atTop, OfNat.ofNat, ValueDistribution.logCounting_mul_zero_le
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
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 ≠ ⊤
rw :
  LE.le (α := ℝ)
    ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
        (HAdd.hAdd (α := locallyFinsuppWithin (X := 𝕜) univ ℤ) (divisor f₁ univ) (divisor f₂ univ))⁻ r :
      ℝ)
    ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
        (HAdd.hAdd (α := locallyFinsupp 𝕜 ℤ) (divisor f₁ univ)⁻ (divisor f₂ univ)⁻) 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

Tactic:
rw [divisor_mul h₁f₁.meromorphicOn h₁f₂.meromorphicOn (fun z _ ↦ h₂f₁ z) (fun z _ ↦ h₂f₂ z),
    ← locallyFinsuppWithin.logCounting.map_add]

Premises used: Function.locallyFinsuppWithin.logCounting, Meromorphic.meromorphicOn, AddMonoidHom.map_add, MeromorphicOn.divisor_mul
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
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 ≠ ⊤
apply :
  (HAdd.hAdd (α := locallyFinsuppWithin (X := 𝕜) univ ℤ) (divisor f₁ univ) (divisor f₂ univ))⁻ ≤
    HAdd.hAdd (α := locallyFinsupp 𝕜 ℤ) (divisor f₁ univ)⁻ (divisor f₂ univ)⁻
⊢ LE.le (α := ℝ)
    ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
        (HAdd.hAdd (α := locallyFinsuppWithin (X := 𝕜) univ ℤ) (divisor f₁ univ) (divisor f₂ univ))⁻ r :
      ℝ)
    ((locallyFinsuppWithin.logCounting : (a : locallyFinsupp 𝕜 ℤ) → ℝ → ℝ)
        (HAdd.hAdd (α := locallyFinsupp 𝕜 ℤ) (divisor f₁ univ)⁻ (divisor f₂ univ)⁻) r :
      ℝ)

Tactic:
apply locallyFinsuppWithin.logCounting_le _ hr

Premises used: Function.locallyFinsuppWithin.logCounting_le
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
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 ≠ ⊤
⊢ (HAdd.hAdd (α := locallyFinsuppWithin (X := 𝕜) univ ℤ) (divisor f₁ univ) (divisor f₂ univ))⁻ ≤
    HAdd.hAdd (α := locallyFinsupp 𝕜 ℤ) (divisor f₁ univ)⁻ (divisor f₂ univ)⁻

Tactic:
apply locallyFinsuppWithin.negPart_add

Premises used: Function.locallyFinsuppWithin.negPart_add
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
f₁ f₂ : 𝕜 → 𝕜
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : 𝕜), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : 𝕜), meromorphicOrderAt f₂ z ≠ ⊤
⊢ ∀ (a : ℝ), 1 ≤ a → logCounting (f₁ * f₂) ⊤ a ≤ (logCounting f₁ ⊤ + logCounting f₂ ⊤) a

Tactic:
fun _ hr ↦ logCounting_mul_top_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂

Premises used: ValueDistribution.logCounting_mul_top_le
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
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 : ℝ) ↦ logCounting (f₁ * f₂) ⊤ x ≤ (logCounting f₁ ⊤ + logCounting f₂ ⊤) x) x} x}
      a
h₁ : ∀ (a : ℝ), 1 ≤ a → logCounting (f₁ * f₂) ⊤ a ≤ (logCounting f₁ ⊤ + logCounting f₂ ⊤) a
⊢ logCounting (f₁ * f₂) ⊤ ≤ᶠ[atTop] logCounting f₁ ⊤ + logCounting f₂ ⊤

Tactic:
filter_upwards [eventually_ge_atTop 1] using
    fun _ hr ↦ logCounting_mul_top_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂

Premises used: ValueDistribution.logCounting_mul_top_le, Filter.eventually_ge_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
f : 𝕜 → 𝕜
n : ℕ
hf : Meromorphic f
⊢ logCounting (f ^ n) 0 = n • logCounting f 0

Tactic:
simp [logCounting, divisor_fun_pow hf.meromorphicOn n]

Premises used: ValueDistribution.logCounting, MeromorphicOn.divisor_fun_pow, Meromorphic.meromorphicOn
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
f : 𝕜 → 𝕜
n : ℕ
hf : Meromorphic f
⊢ logCounting (f ^ n) ⊤ = n • logCounting f ⊤

Tactic:
simp [logCounting, divisor_pow hf.meromorphicOn n]

Premises used: MeromorphicOn.divisor_pow, ValueDistribution.logCounting, Meromorphic.meromorphicOn