. conv => arg 1; intro n; rw [← sub_add_cancel (∫ x, _) (φ 0)]
  conv => arg 3; rw [← sub_add_cancel (φ 0) (φ 0)]
  refine Tendsto.add_const _ ?_
  simp
  refine Filter.Tendsto.congr ?_ h_tendsto
  intro n
  simp [sub_mul]
  rw [integral_sub]
  rotate_left
  . exact IsBump.integrable_mul_continuous hφ DiracSeq.continuous
  . refine Integrable.const_mul ?_ _
    exact DiracSeq.integrable (by simp)
  simp [integral_mul_left, DiracSeq.integral]
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto (fun n => ∫ (x : ℝ), φ x * DiracSeq (↑↑n) x) atTop (nhds (φ 0))

case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
⊢ Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
⊢ Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)