rw [integral_sub]
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ ∫ (x : ℝ), φ x * DiracSeq (↑↑n) x - φ 0 * DiracSeq (↑↑n) x = (∫ (x : ℝ), φ x * DiracSeq (↑↑n) x) - φ 0
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ (∫ (a : ℝ), φ a * DiracSeq (↑↑n) a) - ∫ (a : ℝ), φ 0 * DiracSeq (↑↑n) a = (∫ (x : ℝ), φ x * DiracSeq (↑↑n) x) - φ 0

case hf
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ Integrable fun x => φ x * DiracSeq (↑↑n) x

case hg
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ Integrable fun x => φ 0 * DiracSeq (↑↑n) x