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

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