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 : 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 (α := ℝ)
    (∑ 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‖⁻¹))
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‖⁻¹))
  (∑ 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‖⁻¹))
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‖⁻¹))
    (∑ 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‖⁻¹))
⊢ 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‖⁻¹))
have 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)
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
⊢ 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‖⁻¹))
  (∑ 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‖⁻¹))
Tactic: repeat 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‖⁻¹))
    (∑ 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‖⁻¹))
⊢ 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 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)
Tactic: repeat 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‖⁻¹))
    (∑ 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 (α := ℝ)
    (∑ᶠ (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: repeat 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
⊢ 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‖⁻¹))
have h₁ : ∀ (z : E) (hz : z ∈ hs.toFinset (s := s)),
  (↑((((toClosedBall a : (a_1 : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |a|) ℤ) D :
                locallyFinsuppWithin (X := E) (closedBall 0 |a|) ℤ) :
              (a : E) → ℤ)
            z) :
        ℝ) *
      log (a * ‖z‖⁻¹) ≤
    (↑((((toClosedBall b : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |b|) ℤ) D :
                locallyFinsuppWithin (X := E) (closedBall 0 |b|) ℤ) :
              (a : E) → ℤ)
            z) :
        ℝ) *
      log (b * ‖z‖⁻¹)
Tactic: gcongr 1 with z hz
-- 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
z : E
hz : z ∈ hs.toFinset (s := s)
⊢ (↑((((toClosedBall a : (a_1 : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |a|) ℤ) D :
                locallyFinsuppWithin (X := E) (closedBall 0 |a|) ℤ) :
              (a : E) → ℤ)
            z) :
        ℝ) *
      log (a * ‖z‖⁻¹) ≤
    (↑((((toClosedBall b : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |b|) ℤ) D :
                locallyFinsuppWithin (X := E) (closedBall 0 |b|) ℤ) :
              (a : E) → ℤ)
            z) :
        ℝ) *
      log (b * ‖z‖⁻¹)
have pos : ∀ (h₂z : z = 0),
  (↑((((toClosedBall a : (a_1 : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |a|) ℤ) D :
                locallyFinsuppWithin (X := E) (closedBall 0 |a|) ℤ) :
              (a : E) → ℤ)
            z) :
        ℝ) *
      log (a * ‖z‖⁻¹) ≤
    (↑((((toClosedBall b : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |b|) ℤ) D :
                locallyFinsuppWithin (X := E) (closedBall 0 |b|) ℤ) :
              (a : E) → ℤ)
            z) :
        ℝ) *
      log (b * ‖z‖⁻¹)
Tactic: by_cases h₂z : z = 0
-- 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
z : E
hz : z ∈ hs.toFinset (s := s)
pos :
  ∀ (h₂z : z = 0),
    (↑((((toClosedBall a : (a_1 : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |a|) ℤ) D :
                  locallyFinsuppWithin (X := E) (closedBall 0 |a|) ℤ) :
                (a : E) → ℤ)
              z) :
          ℝ) *
        log (a * ‖z‖⁻¹) ≤
      (↑((((toClosedBall b : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |b|) ℤ) D :
                  locallyFinsuppWithin (X := E) (closedBall 0 |b|) ℤ) :
                (a : E) → ℤ)
              z) :
          ℝ) *
        log (b * ‖z‖⁻¹)
⊢ (↑((((toClosedBall a : (a_1 : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |a|) ℤ) D :
                locallyFinsuppWithin (X := E) (closedBall 0 |a|) ℤ) :
              (a : E) → ℤ)
            z) :
        ℝ) *
      log (a * ‖z‖⁻¹) ≤
    (↑((((toClosedBall b : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |b|) ℤ) D :
                locallyFinsuppWithin (X := E) (closedBall 0 |b|) ℤ) :
              (a : E) → ℤ)
            z) :
        ℝ) *
      log (b * ‖z‖⁻¹)
have neg : ∀ (h₂z : ¬z = 0),
  (↑((((toClosedBall a : (a_1 : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |a|) ℤ) D :
                locallyFinsuppWithin (X := E) (closedBall 0 |a|) ℤ) :
              (a : E) → ℤ)
            z) :
        ℝ) *
      log (a * ‖z‖⁻¹) ≤
    (↑((((toClosedBall b : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |b|) ℤ) D :
                locallyFinsuppWithin (X := E) (closedBall 0 |b|) ℤ) :
              (a : E) → ℤ)
            z) :
        ℝ) *
      log (b * ‖z‖⁻¹)
Tactic: by_cases h₂z : z = 0
-- 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)
hs : s.Finite
z : E
hz : z ∈ hs.toFinset (s := s)
h₂z : ¬z = 0
⊢ (↑((((toClosedBall a : (a_1 : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |a|) ℤ) D :
                locallyFinsuppWithin (X := E) (closedBall 0 |a|) ℤ) :
              (a : E) → ℤ)
            z) :
        ℝ) *
      log (a * ‖z‖⁻¹) ≤
    (↑((((toClosedBall b : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |b|) ℤ) D :
                locallyFinsuppWithin (X := E) (closedBall 0 |b|) ℤ) :
              (a : E) → ℤ)
            z) :
        ℝ) *
      log (b * ‖z‖⁻¹)
have this : Membership.mem (γ := Set E) (closedBall 0 |b|) z
Tactic: have := (toClosedBall_support_subset_closedBall D (hs.mem_toFinset.1 hz))
-- 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
z : E
hz : z ∈ hs.toFinset (s := s)
h₂z : ¬z = 0
this : Membership.mem (γ := Set E) (closedBall 0 |b|) z
⊢ (↑((((toClosedBall a : (a_1 : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |a|) ℤ) D :
                locallyFinsuppWithin (X := E) (closedBall 0 |a|) ℤ) :
              (a : E) → ℤ)
            z) :
        ℝ) *
      log (a * ‖z‖⁻¹) ≤
    (↑((((toClosedBall b : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |b|) ℤ) D :
                locallyFinsuppWithin (X := E) (closedBall 0 |b|) ℤ) :
              (a : E) → ℤ)
            z) :
        ℝ) *
      log (b * ‖z‖⁻¹)
have neg : (↑((((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) → ℤ) z) : ℝ) * log (b * ‖z‖⁻¹)
Tactic: rw [toClosedBall_eval_within _ this]
-- 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
z : E
hz : z ∈ hs.toFinset (s := s)
h₂z : ¬z = 0
this : Membership.mem (γ := Set E) (closedBall 0 |b|) z
⊢ (↑((((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) → ℤ) z) : ℝ) * log (b * ‖z‖⁻¹)
have pos : ∀ (h₃z : Membership.mem (γ := Set E) (closedBall 0 |a|) z),
  (↑((((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) → ℤ) z) : ℝ) * log (b * ‖z‖⁻¹)
Tactic: by_cases h₃z : z ∈ closedBall 0 |a|
-- 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
z : E
hz : z ∈ hs.toFinset (s := s)
h₂z : ¬z = 0
this : Membership.mem (γ := Set E) (closedBall 0 |b|) z
pos :
  ∀ (h₃z : Membership.mem (γ := Set E) (closedBall 0 |a|) z),
    (↑((((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) → ℤ) z) : ℝ) * log (b * ‖z‖⁻¹)
⊢ (↑((((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) → ℤ) z) : ℝ) * log (b * ‖z‖⁻¹)
have neg : ∀ (h₃z : z ∉ closedBall 0 |a|),
  (↑((((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) → ℤ) z) : ℝ) * log (b * ‖z‖⁻¹)
Tactic: by_cases h₃z : z ∈ closedBall 0 |a|
-- 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
z : E
hz : z ∈ hs.toFinset (s := s)
h₂z : ¬z = 0
this : Membership.mem (γ := Set E) (closedBall 0 |b|) z
h₃z : Membership.mem (γ := Set E) (closedBall 0 |a|) z
⊢ (↑((((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) → ℤ) z) : ℝ) * log (b * ‖z‖⁻¹)
have pos : (↑((D : (a : E) → ℤ) z) : ℝ) * log (a * ‖z‖⁻¹) ≤ (↑((D : (a : E) → ℤ) z) : ℝ) * log (b * ‖z‖⁻¹)
Tactic: rw [toClosedBall_eval_within _ h₃z]
-- 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
z : E
hz : z ∈ hs.toFinset (s := s)
h₂z : ¬z = 0
this : Membership.mem (γ := Set E) (closedBall 0 |b|) z
h₃z : Membership.mem (γ := Set E) (closedBall 0 |a|) z
⊢ (↑((D : (a : E) → ℤ) z) : ℝ) * log (a * ‖z‖⁻¹) ≤ (↑((D : (a : E) → ℤ) z) : ℝ) * log (b * ‖z‖⁻¹)
have pos : LE.le (α := ℝ) 0 (↑((D : (a : E) → ℤ) 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
s : Set E :=
  support (U := closedBall 0 |b|) (Y := ℤ)
    ((toClosedBall b : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |b|) ℤ) D)
hs : s.Finite
z : E
hz : z ∈ hs.toFinset (s := s)
h₂z : ¬z = 0
this : Membership.mem (γ := Set E) (closedBall 0 |b|) z
h₃z : z ∉ closedBall 0 |a|
⊢ (↑((((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) → ℤ) z) : ℝ) * log (b * ‖z‖⁻¹)
have neg : 0 ≤ (↑((D : (a : E) → ℤ) z) : ℝ) * log (b * ‖z‖⁻¹)
Tactic: simp only [h₃z, not_false_eq_true, apply_eq_zero_of_notMem, Int.cast_zero, zero_mul,
            ge_iff_le]
-- 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
z : E
hz : z ∈ hs.toFinset (s := s)
h₂z : ¬z = 0
this : Membership.mem (γ := Set E) (closedBall 0 |b|) z
h₃z : z ∉ closedBall 0 |a|
⊢ 0 ≤ (↑((D : (a : E) → ℤ) z) : ℝ) * log (b * ‖z‖⁻¹)
have apply : 1 ≤ b * ‖z‖⁻¹
Tactic: apply mul_nonneg (Int.cast_nonneg (hD z)) (log_nonneg _)
-- 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
z : E
hz : z ∈ hs.toFinset (s := s)
h₂z : ¬z = 0
this : Membership.mem (γ := Set E) (closedBall 0 |b|) z
h₃z : z ∉ closedBall 0 |a|
⊢ 1 ≤ b * ‖z‖⁻¹
have apply : 1 * ‖z‖ ≤ b
Tactic: apply (le_mul_inv_iff₀ (norm_pos_iff.mpr h₂z)).2