simp [intervalIntegral.integral_of_le ha.le]
case this
a : ℝ
ha : 0 < a
n : ℕ+
⊢ (∫ (x : ℝ) in 0 ..a, DiracSeq (↑↑n) x) + ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x =
    ∫ (x : ℝ) in Set.Ioi 0, DiracSeq (↑↑n) x
case this
a : ℝ
ha : 0 < a
n : ℕ+
⊢ ∫ (x : ℝ) in Set.Ioc 0 a, DiracSeq (↑↑n) x ∂volume + ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x =
    ∫ (x : ℝ) in Set.Ioi 0, DiracSeq (↑↑n) x