-- 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 :
  ∑ᶠ (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 (α := ℝ) (↑((D₁ : (a : E) → ℤ) 0) : ℝ) (↑((D₂ : (a : E) → ℤ) 0) : ℝ) * log r =
    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‖⁻¹)) +
      ((↑((D₁ : (a : E) → ℤ) 0) : ℝ) * log r + (↑((D₂ : (a : E) → ℤ) 0) : ℝ) * log r)
⊢ ∑ᶠ (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 (α := ℝ) (↑((D₁ : (a : E) → ℤ) 0) : ℝ) (↑((D₂ : (a : E) → ℤ) 0) : ℝ) * log r =
    HAdd.hAdd (α := ℝ → ℝ) (β := ℝ → ℝ)
      (fun (r : ℝ) ↦
        ∑ᶠ (z : E),
            (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₁ :
                        locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                      (a : E) → ℤ)
                    z) :
                ℝ) *
              log (r * ‖z‖⁻¹) +
          (↑((D₁ : (a : E) → ℤ) 0) : ℝ) * log r)
      (fun (r : ℝ) ↦
        ∑ᶠ (z : E),
            (↑((((toClosedBall r : (a : locallyFinsupp E ℤ) → locallyFinsuppWithin (closedBall 0 |r|) ℤ) D₂ :
                        locallyFinsuppWithin (X := E) (closedBall 0 |r|) ℤ) :
                      (a : E) → ℤ)
                    z) :
                ℝ) *
              log (r * ‖z‖⁻¹) +
          (↑((D₂ : (a : E) → ℤ) 0) : ℝ) * log r)
      r

Tactic:
rw [Pi.add_apply, this]

Premises used: Pi.add_apply