awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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:
repeat 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₁ :
  ∀ (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‖⁻¹)
⊢ 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:
gcongr 1 with z hz
-- 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
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‖⁻¹)
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‖⁻¹)
⊢ (↑((((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
-- 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
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‖⁻¹)

Tactic:
simp [h₂z]
-- 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
z : E
hz : z ∈ hs.toFinset (s := s)
h₂z : ¬z = 0
⊢ Membership.mem (γ := Set E) (closedBall 0 |b|) z

Tactic:
have := (toClosedBall_support_subset_closedBall D (hs.mem_toFinset.1 hz))
-- 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
z : E
hz : z ∈ hs.toFinset (s := s)
h₂z : ¬z = 0
this : Membership.mem (γ := Set E) (closedBall 0 |b|) z
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‖⁻¹)
⊢ (↑((((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:
rw [toClosedBall_eval_within _ this]

Premises used: 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 ℤ
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‖⁻¹)
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‖⁻¹)
⊢ (↑((((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|

Premises used: abs, Metric.closedBall, OfNat.ofNat
-- 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
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
pos : (↑((D : (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‖⁻¹)

Tactic:
rw [toClosedBall_eval_within _ h₃z]

Premises used: 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 ℤ
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
pos : LE.le (α := ℝ) 0 (↑((D : (a : E) → ℤ) z) : ℝ)
⊢ (↑((D : (a : E) → ℤ) z) : ℝ) * log (a * ‖z‖⁻¹) ≤ (↑((D : (a : E) → ℤ) z) : ℝ) * log (b * ‖z‖⁻¹)

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)
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
⊢ LE.le (α := ℝ) 0 (↑((D : (a : E) → ℤ) z) : ℝ)

Tactic:
Int.cast_nonneg (hD z)

Premises used: Int.cast_nonneg
-- 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
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
⊢ LE.le (α := ℝ) 0 (↑((D : (a : E) → ℤ) z) : ℝ)

Tactic:
exact Int.cast_nonneg (hD z)

Premises used: Int.cast_nonneg
-- 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
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|
neg : 0 ≤ (↑((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‖⁻¹)

Tactic:
simp only [h₃z, not_false_eq_true, apply_eq_zero_of_notMem, Int.cast_zero, zero_mul,
            ge_iff_le]

Premises used: Int.cast_zero, ge_iff_le, Function.locallyFinsuppWithin.apply_eq_zero_of_notMem, MulZeroClass.zero_mul, not_false_eq_true
-- 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
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|
apply : 1 ≤ b * ‖z‖⁻¹
⊢ 0 ≤ (↑((D : (a : E) → ℤ) z) : ℝ) * log (b * ‖z‖⁻¹)

Tactic:
apply mul_nonneg (Int.cast_nonneg (hD z)) (log_nonneg _)

Premises used: mul_nonneg, Real.log_nonneg
-- 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
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|
apply : 1 * ‖z‖ ≤ b
⊢ 1 ≤ b * ‖z‖⁻¹

Tactic:
apply (le_mul_inv_iff₀ (norm_pos_iff.mpr h₂z)).2

Premises used: Iff.mpr, norm_pos_iff, le_mul_inv_iff₀
-- 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
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 * ‖z‖ ≤ b

Tactic:
simp_all [abs_of_pos hb]

Premises used: abs_of_pos
-- 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
z : E
⊢ Membership.mem (γ := Set E)
      (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‖⁻¹))
      z →
    z ∈ (↑(hs.toFinset (s := s)) : Set E)

Tactic:
aesop
-- 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
z : E
h₁ :
  ¬Eq (α := ℤ)
        ((((toClosedBall a : (a_1 : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |a|) ℤ) D :
                locallyFinsuppWithin (X := E) (closedBall 0 |a|) ℤ) :
              (a : E) → ℤ)
            z :
          ℤ)
        (0 : ℤ) →
    ¬a = 0 →
      ¬z = 0 →
        ¬a * ‖z‖⁻¹ = 1 →
          ¬a * ‖z‖⁻¹ = -1 →
            ¬Eq (α := ℤ)
                ((((toClosedBall b : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |b|) ℤ) D :
                        locallyFinsuppWithin (X := E) (closedBall 0 |b|) ℤ) :
                      (a : E) → ℤ)
                    z :
                  ℤ)
                (0 : ℤ)
⊢ Membership.mem (γ := Set E)
      (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‖⁻¹))
      z →
    z ∈ (↑(hs.toFinset (s := s)) : Set E)

Tactic:
simp only [support_mul, mem_inter_iff, mem_support, ne_eq, Int.cast_eq_zero, log_eq_zero,
        mul_eq_zero, inv_eq_zero, norm_eq_zero, not_or, Finite.coe_toFinset, and_imp, s]

Premises used: norm_eq_zero, inv_eq_zero, and_imp, Set.mem_inter_iff, Set.Finite.coe_toFinset, Real.log_eq_zero, mul_eq_zero, ne_eq, not_or, Function.mem_support, Int.cast_eq_zero, Function.support_mul
-- 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
z : E
h₁ :
  ¬Eq (α := ℤ)
      ((((toClosedBall a : (a_1 : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |a|) ℤ) D :
              locallyFinsuppWithin (X := E) (closedBall 0 |a|) ℤ) :
            (a : E) → ℤ)
          z :
        ℤ)
      (0 : ℤ)
h₂ :
  ¬a = 0 →
    ¬z = 0 →
      ¬a * ‖z‖⁻¹ = 1 →
        ¬a * ‖z‖⁻¹ = -1 →
          ¬Eq (α := ℤ)
              ((((toClosedBall b : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |b|) ℤ) D :
                      locallyFinsuppWithin (X := E) (closedBall 0 |b|) ℤ) :
                    (a : E) → ℤ)
                  z :
                ℤ)
              (0 : ℤ)
⊢ ¬a = 0 →
    ¬z = 0 →
      ¬a * ‖z‖⁻¹ = 1 →
        ¬a * ‖z‖⁻¹ = -1 →
          ¬Eq (α := ℤ)
              ((((toClosedBall b : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |b|) ℤ) D :
                      locallyFinsuppWithin (X := E) (closedBall 0 |b|) ℤ) :
                    (a : E) → ℤ)
                  z :
                ℤ)
              (0 : ℤ)

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 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
h₁ :
  ¬Eq (α := ℤ)
      ((((toClosedBall a : (a_1 : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |a|) ℤ) D :
              locallyFinsuppWithin (X := E) (closedBall 0 |a|) ℤ) :
            (a : E) → ℤ)
          z :
        ℤ)
      (0 : ℤ)
h_1 : ¬a = 0
h₂ :
  ¬z = 0 →
    ¬a * ‖z‖⁻¹ = 1 →
      ¬a * ‖z‖⁻¹ = -1 →
        ¬Eq (α := ℤ)
            ((((toClosedBall b : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |b|) ℤ) D :
                    locallyFinsuppWithin (X := E) (closedBall 0 |b|) ℤ) :
                  (a : E) → ℤ)
                z :
              ℤ)
            (0 : ℤ)
⊢ ¬z = 0 →
    ¬a * ‖z‖⁻¹ = 1 →
      ¬a * ‖z‖⁻¹ = -1 →
        ¬Eq (α := ℤ)
            ((((toClosedBall b : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |b|) ℤ) D :
                    locallyFinsuppWithin (X := E) (closedBall 0 |b|) ℤ) :
                  (a : E) → ℤ)
                z :
              ℤ)
            (0 : ℤ)

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 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
h₁ :
  ¬Eq (α := ℤ)
      ((((toClosedBall a : (a_1 : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |a|) ℤ) D :
              locallyFinsuppWithin (X := E) (closedBall 0 |a|) ℤ) :
            (a : E) → ℤ)
          z :
        ℤ)
      (0 : ℤ)
h_1 : ¬a = 0
h_2 : ¬z = 0
h₂ :
  ¬a * ‖z‖⁻¹ = 1 →
    ¬a * ‖z‖⁻¹ = -1 →
      ¬Eq (α := ℤ)
          ((((toClosedBall b : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |b|) ℤ) D :
                  locallyFinsuppWithin (X := E) (closedBall 0 |b|) ℤ) :
                (a : E) → ℤ)
              z :
            ℤ)
          (0 : ℤ)
⊢ ¬a * ‖z‖⁻¹ = 1 →
    ¬a * ‖z‖⁻¹ = -1 →
      ¬Eq (α := ℤ)
          ((((toClosedBall b : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |b|) ℤ) D :
                  locallyFinsuppWithin (X := E) (closedBall 0 |b|) ℤ) :
                (a : E) → ℤ)
              z :
            ℤ)
          (0 : ℤ)

Tactic:
_