-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s :
  Set.Finite.{u_2} (α := E)
    (support (U := closedBall 0 |r|) (Y := ℤ)
        ((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₁) ∪
      support (U := closedBall 0 |r|) (Y := ℤ)
        ((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₂))
h :
  (Function.support (M := ℝ) fun (z : E) ↦
      (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₂ :
                  locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                (a : E) → ℤ)
              z) :
          ℝ) *
        log (r * ‖z‖⁻¹)) ⊆
    (↑(h₁s.toFinset (s :=
          support (U := closedBall 0 |r|) (Y := ℤ)
              ((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₁) ∪
            support (U := closedBall 0 |r|) (Y := ℤ)
              ((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₂))) :
      Set E)
h₁ :
  (Function.support (M := ℝ) fun (z : E) ↦
      (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₁ :
                  locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                (a : E) → ℤ)
              z) :
          ℝ) *
        log (r * ‖z‖⁻¹)) ⊆
    (↑(h₁s.toFinset (s :=
          support (U := closedBall 0 |r|) (Y := ℤ)
              ((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₁) ∪
            support (U := closedBall 0 |r|) (Y := ℤ)
              ((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₂))) :
      Set E)
h₂ :
  (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)
⊢ ∑ᶠ (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‖⁻¹) =
    HAdd.hAdd (α := ℝ)
      (∑ᶠ (z : E),
        (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₁ :
                    locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                  (a : E) → ℤ)
                z) :
            ℝ) *
          log (r * ‖z‖⁻¹))
      (∑ᶠ (z : E),
        (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₂ :
                    locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                  (a : E) → ℤ)
                z) :
            ℝ) *
          log (r * ‖z‖⁻¹))

Tactic:
repeat
        rw [finsum_eq_sum_of_support_subset (s := h₁s.toFinset)]
        try simp_rw [← Finset.sum_add_distrib, ← add_mul]

Premises used: add_mul, Finset.sum_add_distrib, finsum_eq_sum_of_support_subset