refine Integrable.const_mul ?_ _
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
case hg
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ Integrable fun x => DiracSeq (↑↑n) x