conv => arg 1; intro b; arg 1; intro x; rw [DiracSeq.eq_comp_mul]
case hg
a : ℝ
ha : 0 < a
⊢ Tendsto (fun x => ∫ (x_1 : ℝ) in 0 ..a, DiracSeq (↑↑x) x_1) atTop (nhds (1 / 2))
case hg
a : ℝ
ha : 0 < a
⊢ Tendsto (fun b => ∫ (x : ℝ) in 0 ..a, ↑↑b * DiracSeq 1 (↑↑b * x)) atTop (nhds (1 / 2))