-- Lean 4 proof step from Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic (goal)
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 ℤ
⊢ (fun (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
have h : ∀ (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: ext r