. rw [eq_sub_iff_add_eq']
  simp [intervalIntegral.integral_of_le ha.le]
  rw [← integral_union]
  . simp [Set.Ioc_union_Ioi_eq_Ioi ha.le]
  . simp [disjoint_iff]
  . exact measurableSet_Ioi
  . apply Integrable.integrableOn
    exact DiracSeq.integrable (by simp)
  . apply Integrable.integrableOn
    exact DiracSeq.integrable (by simp)
case this
a : ℝ
ha : 0 < a
n : ℕ+
⊢ ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x =
    (∫ (x : ℝ) in Set.Ioi 0, DiracSeq (↑↑n) x) - ∫ (x : ℝ) in 0 ..a, DiracSeq (↑↑n) x

a : ℝ
ha : 0 < a
this :
  ∀ {n : ℕ+},
    ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x =
      (∫ (x : ℝ) in Set.Ioi 0, DiracSeq (↑↑n) x) - ∫ (x : ℝ) in 0 ..a, DiracSeq (↑↑n) x
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x) atTop (nhds 0)
a : ℝ
ha : 0 < a
this :
  ∀ {n : ℕ+},
    ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x =
      (∫ (x : ℝ) in Set.Ioi 0, DiracSeq (↑↑n) x) - ∫ (x : ℝ) in 0 ..a, DiracSeq (↑↑n) x
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x) atTop (nhds 0)