no goals
α : Type u_1
β : Type ?u.850348
γ : Type ?u.850351
δ : Type ?u.850354
inst✝ : MeasurableSpace α
K : Type ?u.850360
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ (∑' (n : ℕ), ↑(↑(eapproxDiff f n) a)) = f a
simp_rw [ENNReal.tsum_eq_iSup_nat' (tendsto_add_atTop_nat 1), sum_eapproxDiff,
  iSup_eapprox_apply f hf a]