apply Tendsto.sub
a : ℝ
ha : 0 < a
⊢ Tendsto (fun n => (∫ (x : ℝ) in Set.Ioi 0, DiracSeq (↑↑n) x) - ∫ (x : ℝ) in 0 ..a, DiracSeq (↑↑n) x) atTop
    (nhds (1 / 2 - 1 / 2))
case hf
a : ℝ
ha : 0 < a
⊢ Tendsto (fun x => ∫ (x_1 : ℝ) in Set.Ioi 0, DiracSeq (↑↑x) x_1) atTop (nhds (1 / 2))

case hg
a : ℝ
ha : 0 < a
⊢ Tendsto (fun x => ∫ (x_1 : ℝ) in 0 ..a, DiracSeq (↑↑x) x_1) atTop (nhds (1 / 2))