rw [inv_eq_one_div, ← DiracSeq.integral_Ioi zero_lt_one]
case hg
a : ℝ
ha : 0 < a
⊢ Tendsto (fun b => ∫ (x : ℝ) in 0 ..↑↑b * a, DiracSeq 1 x) atTop (nhds 2⁻¹)
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))