have h_integrable {n : ℕ+} := @integrable_bump_sub_const_mul_diracSeq _ hφ (φ 0) n (by simp)
case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
⊢ Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
⊢ Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)