awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁s :
  Set.Finite.{u_2} (α := E)
    (support (U := closedBall 0 |r|) (Y := ℤ)
        ((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₁) ∪
      support (U := closedBall 0 |r|) (Y := ℤ)
        ((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₂))
h h₁ :
  ∀ ⦃x : E⦄
    (hx :
      Membership.mem (γ := Set E)
        (Function.support (M := ℝ) fun (z : E) ↦
          (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₂ :
                      locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                    (a : E) → ℤ)
                  z) :
              ℝ) *
            log (r * ‖z‖⁻¹))
        x),
    x ∈
      (↑(h₁s.toFinset (s :=
            support (U := closedBall 0 |r|) (Y := ℤ)
                ((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₁) ∪
              support (U := closedBall 0 |r|) (Y := ℤ)
                ((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₂))) :
        Set E)
h₂ :
  ∀ ⦃x : E⦄
    (hx :
      Membership.mem (γ := Set E)
        (Function.support (M := ℝ) fun (z : E) ↦
          (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₂ :
                      locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                    (a : E) → ℤ)
                  z) :
              ℝ) *
            log (r * ‖z‖⁻¹))
        x)
    (this :
      x ∉
        (↑(h₁s.toFinset (s :=
              support (U := closedBall 0 |r|) (Y := ℤ)
                  ((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₁) ∪
                support (U := closedBall 0 |r|) (Y := ℤ)
                  ((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₂))) :
          Set E)),
    False
⊢ (Function.support (M := ℝ) fun (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₁s.toFinset (s :=
          support (U := closedBall 0 |r|) (Y := ℤ)
              ((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₁) ∪
            support (U := closedBall 0 |r|) (Y := ℤ)
              ((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₂))) :
      Set E)

Tactic:
repeat
        intro x hx
        by_contra
        simp_all
-- 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)
⊢ HAdd.hAdd (α := ℝ) (↑((D₁ : (a : E) → ℤ) 0) : ℝ) (↑((D₂ : (a : E) → ℤ) 0) : ℝ) * log r =
    (↑((D₁ : (a : E) → ℤ) 0) : ℝ) * log r + (↑((D₂ : (a : E) → ℤ) 0) : ℝ) * log r

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsupp E ℤ
⊢ Eq (α := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D 0 : ℝ) (0 : ℝ)

Tactic:
simp [logCounting]

Premises used: Function.locallyFinsuppWithin.logCounting
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : DecidableEq E
inst_2 : ProperSpace E
e : E
r : ℝ
n : ℤ
hr : ‖e‖ ≤ r
⊢ (Function.support (M := ℝ) fun (z : E) ↦
      (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) (single e n) :
                  locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                (a : E) → ℤ)
              z) :
          ℝ) *
        log (r * ‖z‖⁻¹)) ⊆
    (↑(⋯.toFinset (s := {e})) : Set E)

Tactic:
simp_all [toClosedBall, restrict_apply, single_apply]

Premises used: Function.locallyFinsuppWithin.restrict_apply, Function.locallyFinsuppWithin.single_apply, Function.locallyFinsuppWithin.toClosedBall
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : DecidableEq E
inst_2 : ProperSpace E
e : E
r : ℝ
n : ℤ
hr : ‖e‖ ≤ r
rw :
  ∑ i ∈ ⋯.toFinset (s := {e}),
        (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) (single e n) :
                    locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                  (a : E) → ℤ)
                i) :
            ℝ) *
          log (r * ‖i‖⁻¹) +
      (↑((single e n : (a : E) → ℤ) 0) : ℝ) * log r =
    (↑n : ℝ) * (log r - log ‖e‖)
⊢ ∑ᶠ (z : E),
        (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) (single e n) :
                    locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                  (a : E) → ℤ)
                z) :
            ℝ) *
          log (r * ‖z‖⁻¹) +
      (↑((single e n : (a : E) → ℤ) 0) : ℝ) * log r =
    (↑n : ℝ) * (log r - log ‖e‖)

Tactic:
rw [finsum_eq_sum_of_support_subset _ (s := (finite_singleton e).toFinset)
    (by simp_all [toClosedBall, restrict_apply, single_apply])]

Premises used: finsum_eq_sum_of_support_subset
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : DecidableEq E
inst_2 : ProperSpace E
e : E
r : ℝ
n : ℤ
hr : ‖e‖ ≤ r
simp :
  (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) (single e n) :
                  locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                (a : E) → ℤ)
              e) :
          ℝ) *
        log (r * ‖e‖⁻¹) +
      (↑((single e n : (a : E) → ℤ) 0) : ℝ) * log r =
    (↑n : ℝ) * (log r - log ‖e‖)
⊢ ∑ i ∈ ⋯.toFinset (s := {e}),
        (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) (single e n) :
                    locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                  (a : E) → ℤ)
                i) :
            ℝ) *
          log (r * ‖i‖⁻¹) +
      (↑((single e n : (a : E) → ℤ) 0) : ℝ) * log r =
    (↑n : ℝ) * (log r - log ‖e‖)

Tactic:
simp only [toFinite_toFinset, toFinset_singleton, Finset.sum_singleton]

Premises used: Set.toFinite_toFinset, Set.toFinset_singleton, Finset.sum_singleton
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : DecidableEq E
inst_2 : ProperSpace E
e : E
r : ℝ
n : ℤ
hr : ‖e‖ ≤ r
⊢ Membership.mem (γ := Set E) (closedBall 0 |r|) e

Tactic:
simpa [abs_of_nonneg ((norm_nonneg e).trans hr)]

Premises used: abs_of_nonneg, LE.le.trans, norm_nonneg
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : DecidableEq E
inst_2 : ProperSpace E
e : E
r : ℝ
n : ℤ
hr : ‖e‖ ≤ r
rw :
  (↑((single e n : (a : E) → ℤ) e) : ℝ) * log (r * ‖e‖⁻¹) + (↑((single e n : (a : E) → ℤ) 0) : ℝ) * log r =
    (↑n : ℝ) * (log r - log ‖e‖)
⊢ (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) (single e n) :
                  locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                (a : E) → ℤ)
              e) :
          ℝ) *
        log (r * ‖e‖⁻¹) +
      (↑((single e n : (a : E) → ℤ) 0) : ℝ) * log r =
    (↑n : ℝ) * (log r - log ‖e‖)

Tactic:
rw [toClosedBall_eval_within _ (by simpa [abs_of_nonneg ((norm_nonneg e).trans hr)])]

Premises used: Function.locallyFinsuppWithin.toClosedBall_eval_within
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : DecidableEq E
inst_2 : ProperSpace E
e : E
r : ℝ
n : ℤ
hr : ‖e‖ ≤ r
pos :
  ∀ (he : 0 = e),
    (↑((single e n : (a : E) → ℤ) e) : ℝ) * log (r * ‖e‖⁻¹) + (↑((single e n : (a : E) → ℤ) 0) : ℝ) * log r =
      (↑n : ℝ) * (log r - log ‖e‖)
neg :
  ∀ (he : ¬0 = e),
    (↑((single e n : (a : E) → ℤ) e) : ℝ) * log (r * ‖e‖⁻¹) + (↑((single e n : (a : E) → ℤ) 0) : ℝ) * log r =
      (↑n : ℝ) * (log r - log ‖e‖)
⊢ (↑((single e n : (a : E) → ℤ) e) : ℝ) * log (r * ‖e‖⁻¹) + (↑((single e n : (a : E) → ℤ) 0) : ℝ) * log r =
    (↑n : ℝ) * (log r - log ‖e‖)

Tactic:
by_cases he : 0 = e
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : DecidableEq E
inst_2 : ProperSpace E
e : E
r : ℝ
n : ℤ
hr : ‖e‖ ≤ r
he : 0 = e
⊢ (↑((single e n : (a : E) → ℤ) e) : ℝ) * log (r * ‖e‖⁻¹) + (↑((single e n : (a : E) → ℤ) 0) : ℝ) * log r =
    (↑n : ℝ) * (log r - log ‖e‖)

Tactic:
simp [← he, single_apply]

Premises used: Function.locallyFinsuppWithin.single_apply
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : DecidableEq E
inst_2 : ProperSpace E
e : E
r : ℝ
n : ℤ
hr : ‖e‖ ≤ r
he : ¬0 = e
neg : (↑n : ℝ) * (log r + -log ‖e‖) = (↑n : ℝ) * (log r - log ‖e‖)
⊢ (↑((single e n : (a : E) → ℤ) e) : ℝ) * log (r * ‖e‖⁻¹) + (↑((single e n : (a : E) → ℤ) 0) : ℝ) * log r =
    (↑n : ℝ) * (log r - log ‖e‖)

Tactic:
simp only [single_apply, he, reduceIte, Int.cast_zero, zero_mul, add_zero,
      log_mul (ne_of_lt (lt_of_lt_of_le (norm_pos_iff.mpr (he ·.symm)) hr)).symm
      (inv_ne_zero (norm_ne_zero_iff.mpr (he ·.symm))), log_inv]

Premises used: Iff.mpr, norm_pos_iff, Int.cast_zero, MulZeroClass.zero_mul, Function.locallyFinsuppWithin.single_apply, Ne.symm, norm_ne_zero_iff, reduceIte, inv_ne_zero, Real.log_inv, add_zero, Eq.symm, ne_of_lt, Real.log_mul, lt_of_lt_of_le
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : DecidableEq E
inst_2 : ProperSpace E
e : E
r : ℝ
n : ℤ
hr : ‖e‖ ≤ r
he : ¬0 = e
⊢ (↑n : ℝ) * (log r + -log ‖e‖) = (↑n : ℝ) * (log r - log ‖e‖)

Tactic:
grind
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : DecidableEq E
inst_2 : ProperSpace E
e : E
r : ℝ
n : ℤ
hr : ‖e‖ ≤ r
simp :
  ∑ᶠ (z : E),
        (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) (single e n) :
                    locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                  (a : E) → ℤ)
                z) :
            ℝ) *
          log (r * ‖z‖⁻¹) +
      (↑((single e n : (a : E) → ℤ) 0) : ℝ) * log r =
    (↑n : ℝ) * (log r - log ‖e‖)
simp₁ :
  ∑ i ∈ ⋯.toFinset (s := {e}),
        (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) (single e n) :
                    locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                  (a : E) → ℤ)
                i) :
            ℝ) *
          log (r * ‖i‖⁻¹) +
      (↑((single e n : (a : E) → ℤ) 0) : ℝ) * log r =
    (↑n : ℝ) * (log r - log ‖e‖)
simp₂ :
  (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) (single e n) :
                  locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                (a : E) → ℤ)
              e) :
          ℝ) *
        log (r * ‖e‖⁻¹) +
      (↑((single e n : (a : E) → ℤ) 0) : ℝ) * log r =
    (↑n : ℝ) * (log r - log ‖e‖)
simp₃ :
  (↑((single e n : (a : E) → ℤ) e) : ℝ) * log (r * ‖e‖⁻¹) + (↑((single e n : (a : E) → ℤ) 0) : ℝ) * log r =
    (↑n : ℝ) * (log r - log ‖e‖)
pos :
  ∀ (he : 0 = e),
    (↑((single e n : (a : E) → ℤ) e) : ℝ) * log (r * ‖e‖⁻¹) + (↑((single e n : (a : E) → ℤ) 0) : ℝ) * log r =
      (↑n : ℝ) * (log r - log ‖e‖)
neg neg₁ :
  ∀ (he : ¬0 = e),
    (↑((single e n : (a : E) → ℤ) e) : ℝ) * log (r * ‖e‖⁻¹) + (↑((single e n : (a : E) → ℤ) 0) : ℝ) * log r =
      (↑n : ℝ) * (log r - log ‖e‖)
⊢ (logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e n) r = (↑n : ℝ) * (log r - log ‖e‖)

Tactic:
classical
  simp only [logCounting, AddMonoidHom.coe_mk, ZeroHom.coe_mk]
  rw [finsum_eq_sum_of_support_subset _ (s := (finite_singleton e).toFinset)
    (by simp_all [toClosedBall, restrict_apply, single_apply])]
  simp only [toFinite_toFinset, toFinset_singleton, Finset.sum_singleton]
  rw [toClosedBall_eval_within _ (by simpa [abs_of_nonneg ((norm_nonneg e).trans hr)])]
  by_cases he : 0 = e
  · simp [← he, single_apply]
  · simp only [single_apply, he, reduceIte, Int.cast_zero, zero_mul, add_zero,
      log_mul (ne_of_lt (lt_of_lt_of_le (norm_pos_iff.mpr (he ·.symm)) hr)).symm
      (inv_ne_zero (norm_ne_zero_iff.mpr (he ·.symm))), log_inv]
    grind

Premises used: AddMonoidHom.coe_mk, Int.cast_zero, MulZeroClass.zero_mul, Function.locallyFinsuppWithin.logCounting, Set.toFinite_toFinset, Function.locallyFinsuppWithin.single_apply, Set.toFinset_singleton, Finset.sum_singleton, ZeroHom.coe_mk, finsum_eq_sum_of_support_subset, reduceIte, Real.log_inv, add_zero, Function.locallyFinsuppWithin.toClosedBall_eval_within
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsupp E ℤ
r : ℝ
⊢ Eq (α := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D (-r) : ℝ)
    ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D r : ℝ)

Tactic:
simp [logCounting, toClosedBall, restrict_apply]

Premises used: Function.locallyFinsuppWithin.restrict_apply, Function.locallyFinsuppWithin.logCounting, Function.locallyFinsuppWithin.toClosedBall
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsupp E ℤ
hD : 0 ≤ D
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioi 0) a
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Ioi 0) b
_ :
  a ≤ b →
    LE.le (α := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D a : ℝ)
      ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D b : ℝ)
⊢ a ≤ b →
    LE.le (α := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D a : ℝ)
      ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D b : ℝ)

Tactic:
_
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsupp E ℤ
hD : 0 ≤ D
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioi 0) a
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Ioi 0) b
h : a ≤ b
⊢ 0 < a

Tactic:
simp_all only [mem_Ioi, logCounting, AddMonoidHom.coe_mk, ZeroHom.coe_mk]

Premises used: AddMonoidHom.coe_mk, Function.locallyFinsuppWithin.logCounting, Set.mem_Ioi, ZeroHom.coe_mk
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsupp E ℤ
hD : 0 ≤ D
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioi 0) a
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Ioi 0) b
h : a ≤ b
ha₁ : 0 < a
⊢ 0 < b

Tactic:
simp_all only [mem_Ioi, logCounting, AddMonoidHom.coe_mk, ZeroHom.coe_mk]

Premises used: AddMonoidHom.coe_mk, Function.locallyFinsuppWithin.logCounting, Set.mem_Ioi, ZeroHom.coe_mk
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsupp E ℤ
hD : 0 ≤ D
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioi 0) a
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Ioi 0) b
h : a ≤ b
ha₁ : 0 < a
hb₁ : 0 < b
⊢ a ≤ b

Tactic:
simp_all only [mem_Ioi, logCounting, AddMonoidHom.coe_mk, ZeroHom.coe_mk]

Premises used: AddMonoidHom.coe_mk, Function.locallyFinsuppWithin.logCounting, Set.mem_Ioi, ZeroHom.coe_mk
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsupp E ℤ
hD : 0 ≤ D
a b : ℝ
ha : 0 < a
hb : 0 < b
h : a ≤ b
h₁ :
  LE.le (α := ℝ)
    (∑ᶠ (z : E),
      (↑((((toClosedBall a : (a_1 : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |a|) ℤ) D :
                  locallyFinsuppWithin (X := E) (closedBall 0 |a|) ℤ) :
                (a : E) → ℤ)
              z) :
          ℝ) *
        log (a * ‖z‖⁻¹))
    (∑ᶠ (z : E),
      (↑((((toClosedBall b : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |b|) ℤ) D :
                  locallyFinsuppWithin (X := E) (closedBall 0 |b|) ℤ) :
                (a : E) → ℤ)
              z) :
          ℝ) *
        log (b * ‖z‖⁻¹))
h₂ : LE.le (α := ℝ) 0 (↑((D : (a : E) → ℤ) 0) : ℝ)
⊢ ∑ᶠ (z : E),
        (↑((((toClosedBall a : (a_1 : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |a|) ℤ) D :
                    locallyFinsuppWithin (X := E) (closedBall 0 |a|) ℤ) :
                  (a : E) → ℤ)
                z) :
            ℝ) *
          log (a * ‖z‖⁻¹) +
      (↑((D : (a : E) → ℤ) 0) : ℝ) * log a ≤
    ∑ᶠ (z : E),
        (↑((((toClosedBall b : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |b|) ℤ) D :
                    locallyFinsuppWithin (X := E) (closedBall 0 |b|) ℤ) :
                  (a : E) → ℤ)
                z) :
            ℝ) *
          log (b * ‖z‖⁻¹) +
      (↑((D : (a : E) → ℤ) 0) : ℝ) * log b

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsupp E ℤ
hD : 0 ≤ D
a b : ℝ
ha : 0 < a
hb : 0 < b
h : a ≤ b
s : Set E :=
  support (U := closedBall 0 |b|) (Y := ℤ)
    ((toClosedBall b : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |b|) ℤ) D)
⊢ s.Finite

Tactic:
have hs : s.Finite := (toClosedBall b D).finiteSupport (isCompact_closedBall 0 |b|)
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsupp E ℤ
hD : 0 ≤ D
a b : ℝ
ha : 0 < a
hb : 0 < b
h : a ≤ b
s : Set E :=
  support (U := closedBall 0 |b|) (Y := ℤ)
    ((toClosedBall b : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |b|) ℤ) D)
hs : s.Finite
h₁ :
  LE.le (α := ℝ)
    (∑ i ∈ hs.toFinset (s := s),
      (↑((((toClosedBall a : (a_1 : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |a|) ℤ) D :
                  locallyFinsuppWithin (X := E) (closedBall 0 |a|) ℤ) :
                (a : E) → ℤ)
              i) :
          ℝ) *
        log (a * ‖i‖⁻¹))
    (∑ᶠ (z : E),
      (↑((((toClosedBall b : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |b|) ℤ) D :
                  locallyFinsuppWithin (X := E) (closedBall 0 |b|) ℤ) :
                (a : E) → ℤ)
              z) :
          ℝ) *
        log (b * ‖z‖⁻¹))
h₂ :
  (Function.support (M := ℝ) fun (z : E) ↦
      (↑((((toClosedBall a : (a_1 : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |a|) ℤ) D :
                  locallyFinsuppWithin (X := E) (closedBall 0 |a|) ℤ) :
                (a : E) → ℤ)
              z) :
          ℝ) *
        log (a * ‖z‖⁻¹)) ⊆
    (↑(hs.toFinset (s := s)) : Set E)
⊢ LE.le (α := ℝ)
    (∑ᶠ (z : E),
      (↑((((toClosedBall a : (a_1 : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |a|) ℤ) D :
                  locallyFinsuppWithin (X := E) (closedBall 0 |a|) ℤ) :
                (a : E) → ℤ)
              z) :
          ℝ) *
        log (a * ‖z‖⁻¹))
    (∑ᶠ (z : E),
      (↑((((toClosedBall b : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |b|) ℤ) D :
                  locallyFinsuppWithin (X := E) (closedBall 0 |b|) ℤ) :
                (a : E) → ℤ)
              z) :
          ℝ) *
        log (b * ‖z‖⁻¹))

Tactic:
rw [finsum_eq_sum_of_support_subset (s := hs.toFinset)]

Premises used: finsum_eq_sum_of_support_subset
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : ProperSpace E
D : locallyFinsupp E ℤ
hD : 0 ≤ D
a b : ℝ
ha : 0 < a
hb : 0 < b
h : a ≤ b
s : Set E :=
  support (U := closedBall 0 |b|) (Y := ℤ)
    ((toClosedBall b : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |b|) ℤ) D)
hs : s.Finite
h₁ :
  LE.le (α := ℝ)
    (∑ i ∈ hs.toFinset (s := s),
      (↑((((toClosedBall a : (a_1 : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |a|) ℤ) D :
                  locallyFinsuppWithin (X := E) (closedBall 0 |a|) ℤ) :
                (a : E) → ℤ)
              i) :
          ℝ) *
        log (a * ‖i‖⁻¹))
    (∑ i ∈ hs.toFinset (s := s),
      (↑((((toClosedBall b : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |b|) ℤ) D :
                  locallyFinsuppWithin (X := E) (closedBall 0 |b|) ℤ) :
                (a : E) → ℤ)
              i) :
          ℝ) *
        log (b * ‖i‖⁻¹))
h₂ :
  (Function.support (M := ℝ) fun (z : E) ↦
      (↑((((toClosedBall b : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |b|) ℤ) D :
                  locallyFinsuppWithin (X := E) (closedBall 0 |b|) ℤ) :
                (a : E) → ℤ)
              z) :
          ℝ) *
        log (b * ‖z‖⁻¹)) ⊆
    (↑(hs.toFinset (s := s)) : Set E)
⊢ LE.le (α := ℝ)
    (∑ i ∈ hs.toFinset (s := s),
      (↑((((toClosedBall a : (a_1 : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |a|) ℤ) D :
                  locallyFinsuppWithin (X := E) (closedBall 0 |a|) ℤ) :
                (a : E) → ℤ)
              i) :
          ℝ) *
        log (a * ‖i‖⁻¹))
    (∑ᶠ (z : E),
      (↑((((toClosedBall b : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |b|) ℤ) D :
                  locallyFinsuppWithin (X := E) (closedBall 0 |b|) ℤ) :
                (a : E) → ℤ)
              z) :
          ℝ) *
        log (b * ‖z‖⁻¹))

Tactic:
rw [finsum_eq_sum_of_support_subset (s := hs.toFinset)]

Premises used: finsum_eq_sum_of_support_subset