-- 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 ℤ
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
⊢ (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

Tactic:
ext r