awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : DecidableEq E
inst_2 : ProperSpace E
e : E
r : ℝ
n : ℤ
hr : ‖e‖ ≤ r
⊢ (↑((single e n : (a : E) → ℤ) e) : ℝ) * log (r * ‖e‖⁻¹) + (↑((single e n : (a : E) → ℤ) 0) : ℝ) * log r =
    (↑n : ℝ) * (log r - log ‖e‖)
have 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‖)
Tactic: by_cases he : 0 = e
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
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‖)
⊢ (↑((single e n : (a : E) → ℤ) e) : ℝ) * log (r * ‖e‖⁻¹) + (↑((single e n : (a : E) → ℤ) 0) : ℝ) * log r =
    (↑n : ℝ) * (log r - log ‖e‖)
have 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‖)
Tactic: by_cases he : 0 = e
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
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‖)
have neg : (↑n : ℝ) * (log r + -log ‖e‖) = (↑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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : DecidableEq E
inst_2 : ProperSpace E
e : E
r : ℝ
n : ℤ
hr : ‖e‖ ≤ r
⊢ (logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e n) r = (↑n : ℝ) * (log r - log ‖e‖)
have 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‖)
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
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
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‖)
⊢ (logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e n) r = (↑n : ℝ) * (log r - log ‖e‖)
have simp₁ : ∑ i ∈ sorry.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: 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
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
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‖)
⊢ (logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e n) r = (↑n : ℝ) * (log r - log ‖e‖)
have 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‖)
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
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
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‖)
⊢ (logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e n) r = (↑n : ℝ) * (log r - log ‖e‖)
have simp₃ : (↑((single e n : (a : E) → ℤ) e) : ℝ) * log (r * ‖e‖⁻¹) + (↑((single e n : (a : E) → ℤ) 0) : ℝ) * log 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
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
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‖)
⊢ (logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e n) r = (↑n : ℝ) * (log r - log ‖e‖)
have 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‖)
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
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
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‖)
⊢ (logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) (single e n) r = (↑n : ℝ) * (log r - log ‖e‖)
have 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‖)
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
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (hypothesis)
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
⊢ LE.le (α := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D a : ℝ)
    ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D b : ℝ)
have ha₁ : 0 < a
Tactic: simp_all only [mem_Ioi, logCounting, AddMonoidHom.coe_mk, ZeroHom.coe_mk]
Cleared hypotheses: ha, hb, h
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (hypothesis)
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
⊢ LE.le (α := ℝ) ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D a : ℝ)
    ((logCounting : (a : locallyFinsupp E ℤ) → ℝ → ℝ) D b : ℝ)
have hb₁ : 0 < b
Tactic: simp_all only [mem_Ioi, logCounting, AddMonoidHom.coe_mk, ZeroHom.coe_mk]
Cleared hypotheses: ha, hb, h
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
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
⊢ ∑ᶠ (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
have 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‖⁻¹))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
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‖⁻¹))
⊢ ∑ᶠ (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
have h₂ : LE.le (α := ℝ) 0 (↑((D : (a : E) → ℤ) 0) : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (hypothesis)
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)
⊢ 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‖⁻¹))
have hs : s.Finite
Tactic: have hs : s.Finite := (toClosedBall b D).finiteSupport (isCompact_closedBall 0 |b|)
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
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
⊢ 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‖⁻¹))
have 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‖⁻¹))
Tactic: rw [finsum_eq_sum_of_support_subset (s := hs.toFinset)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
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‖⁻¹))
⊢ 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‖⁻¹))
have 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)
Tactic: rw [finsum_eq_sum_of_support_subset (s := hs.toFinset)]