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)
apply :
  Set.Finite.{u_2} (α := E)
      (support (U := closedBall 0 |r|) (Y := ℤ)
        ((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₁)) ∧
    Set.Finite.{u_2} (α := E)
      (support (U := closedBall 0 |r|) (Y := ℤ)
        ((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₂))
⊢ 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₂))

Tactic:
apply Set.finite_union.2

Premises used: Iff.mpr, Set.finite_union
-- 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)
left :
  Set.Finite.{u_2} (α := E)
    (support (U := closedBall 0 |r|) (Y := ℤ)
      ((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₁))
right :
  Set.Finite.{u_2} (α := E)
    (support (U := closedBall 0 |r|) (Y := ℤ)
      ((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₂))
⊢ Set.Finite.{u_2} (α := E)
      (support (U := closedBall 0 |r|) (Y := ℤ)
        ((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₁)) ∧
    Set.Finite.{u_2} (α := E)
      (support (U := closedBall 0 |r|) (Y := ℤ)
        ((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₂))

Tactic:
constructor
-- 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)
⊢ Set.Finite.{u_2} (α := E)
    (support (U := closedBall 0 |r|) (Y := ℤ)
      ((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₁))

Tactic:
apply finiteSupport _ (isCompact_closedBall 0 |r|)

Premises used: abs, Function.locallyFinsuppWithin.finiteSupport, ProperSpace.isCompact_closedBall, OfNat.ofNat
-- 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)
⊢ Set.Finite.{u_2} (α := E)
    (support (U := closedBall 0 |r|) (Y := ℤ)
      ((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₂))

Tactic:
apply finiteSupport _ (isCompact_closedBall 0 |r|)

Premises used: abs, Function.locallyFinsuppWithin.finiteSupport, ProperSpace.isCompact_closedBall, OfNat.ofNat
-- 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)
⊢ 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₂))

Tactic:
have h₁s : ((D₁.toClosedBall r).support ∪ (D₂.toClosedBall r).support).Finite := by
        apply Set.finite_union.2
        constructor
        <;> apply finiteSupport _ (isCompact_closedBall 0 |r|)
-- 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₂))
⊢ (Function.support (M := ℝ) fun (z : E) ↦
      HAdd.hAdd (α := ℝ)
          (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₁ :
                    locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                  (a : E) → ℤ)
                z) :
            ℝ)
          (↑((((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:
simp_rw [← Finset.sum_add_distrib, ← add_mul]

Premises used: add_mul, Finset.sum_add_distrib
-- 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₂))
⊢ ∑
      i ∈
        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₂)),
      HAdd.hAdd (α := ℝ)
          (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₁ :
                    locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                  (a : E) → ℤ)
                i) :
            ℝ)
          (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₂ :
                    locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                  (a : E) → ℤ)
                i) :
            ℝ) *
        log (r * ‖i‖⁻¹) =
    HAdd.hAdd (α := ℝ)
      (∑
        i ∈
          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₂)),
        (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₁ :
                    locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                  (a : E) → ℤ)
                i) :
            ℝ) *
          log (r * ‖i‖⁻¹))
      (∑
        i ∈
          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₂)),
        (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₂ :
                    locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                  (a : E) → ℤ)
                i) :
            ℝ) *
          log (r * ‖i‖⁻¹))

Tactic:
simp_rw [← Finset.sum_add_distrib, ← add_mul]

Premises used: add_mul, Finset.sum_add_distrib
-- 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₂))
⊢ ∑
      i ∈
        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₂)),
      HAdd.hAdd (α := ℝ)
          (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₁ :
                    locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                  (a : E) → ℤ)
                i) :
            ℝ)
          (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₂ :
                    locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                  (a : E) → ℤ)
                i) :
            ℝ) *
        log (r * ‖i‖⁻¹) =
    HAdd.hAdd (α := ℝ)
      (∑
        i ∈
          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₂)),
        (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₁ :
                    locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                  (a : E) → ℤ)
                i) :
            ℝ) *
          log (r * ‖i‖⁻¹))
      (∑
        i ∈
          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₂)),
        (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₂ :
                    locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                  (a : E) → ℤ)
                i) :
            ℝ) *
          log (r * ‖i‖⁻¹))

Tactic:
try simp_rw [← Finset.sum_add_distrib, ← add_mul]

Premises used: add_mul, Finset.sum_add_distrib
-- 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₂))
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
h :
  ∀
    (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
⊢ 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)

Tactic:
by_contra
-- 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_1 : ∀ {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₂))
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

Tactic:
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)
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₂))
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
h :
  ∀
    (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
⊢ 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)

Tactic:
by_contra
-- 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_1 : ∀ {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₂))
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

Tactic:
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)
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₂))
x : E
hx :
  Membership.mem (γ := Set E)
    (Function.support (M := ℝ) fun (z : E) ↦
      HAdd.hAdd (α := ℝ)
          (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₁ :
                    locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                  (a : E) → ℤ)
                z) :
            ℝ)
          (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₂ :
                    locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                  (a : E) → ℤ)
                z) :
            ℝ) *
        log (r * ‖z‖⁻¹))
    x
h :
  ∀
    (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
⊢ 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)

Tactic:
by_contra
-- 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_1 : ∀ {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₂))
x : E
hx :
  Membership.mem (γ := Set E)
    (Function.support (M := ℝ) fun (z : E) ↦
      HAdd.hAdd (α := ℝ)
          (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₁ :
                    locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                  (a : E) → ℤ)
                z) :
            ℝ)
          (↑((((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

Tactic:
simp_all