apply intervalIntegral_tendsto_integral_Ioi
case hg
a : ℝ
ha : 0 < a
⊢ Tendsto (fun b => ∫ (x : ℝ) in 0 ..↑↑b * a, DiracSeq 1 x) atTop (nhds (∫ (x : ℝ) in Set.Ioi 0, DiracSeq 1 x))
case hg.hfi
a : ℝ
ha : 0 < a
⊢ IntegrableOn (fun x => DiracSeq 1 x) (Set.Ioi 0)

case hg.hb
a : ℝ
ha : 0 < a
⊢ Tendsto (fun i => ↑↑i * a) atTop atTop