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

case this.hst
a : ℝ
ha : 0 < a
n : ℕ+
⊢ Disjoint (Set.Ioc 0 a) (Set.Ioi a)

case this.ht
a : ℝ
ha : 0 < a
n : ℕ+
⊢ MeasurableSet (Set.Ioi a)

case this.hfs
a : ℝ
ha : 0 < a
n : ℕ+
⊢ IntegrableOn (fun x => DiracSeq (↑↑n) x) (Set.Ioc 0 a)

case this.hft
a : ℝ
ha : 0 < a
n : ℕ+
⊢ IntegrableOn (fun x => DiracSeq (↑↑n) x) (Set.Ioi a)
case this.hst
a : ℝ
ha : 0 < a
n : ℕ+
⊢ Disjoint (Set.Ioc 0 a) (Set.Ioi a)

case this.ht
a : ℝ
ha : 0 < a
n : ℕ+
⊢ MeasurableSet (Set.Ioi a)

case this.hfs
a : ℝ
ha : 0 < a
n : ℕ+
⊢ IntegrableOn (fun x => DiracSeq (↑↑n) x) (Set.Ioc 0 a)

case this.hft
a : ℝ
ha : 0 < a
n : ℕ+
⊢ IntegrableOn (fun x => DiracSeq (↑↑n) x) (Set.Ioi a)