simp [intervalIntegral.integral_comp_mul_left]
case hg
a : ℝ
ha : 0 < a
⊢ Tendsto (fun b => ↑↑b * ∫ (x : ℝ) in 0 ..a, DiracSeq 1 (↑↑b * x)) atTop (nhds 2⁻¹)
case hg
a : ℝ
ha : 0 < a
⊢ Tendsto (fun b => ∫ (x : ℝ) in 0 ..↑↑b * a, DiracSeq 1 x) atTop (nhds 2⁻¹)