have hI₁ {a} (ha : 0 < a) : Tendsto (fun (n : ℕ+) => ∫ x in Set.Iic (-a), (φ x - φ 0) * DiracSeq n x) atTop (nhds 0)
case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
case hI₁
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
a : ℝ
ha : 0 < a
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-a), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)

case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
hI₁ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-a), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)