suffices (n : ℕ+) : |∫ x in Set.Ioi a, (φ x - y) * DiracSeq n x| ≤ M * ∫ x in Set.Ioi a, DiracSeq n x
case intro
a : ℝ
ha : 0 < a
φ : ℝ → ℝ
hφ : IsBump φ
y M : ℝ
hM : ∀ (x : ℝ), ‖φ x - y‖ ≤ M
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - y) * DiracSeq (↑↑n) x) atTop (nhds 0)
case intro
a : ℝ
ha : 0 < a
φ : ℝ → ℝ
hφ : IsBump φ
y M : ℝ
hM : ∀ (x : ℝ), ‖φ x - y‖ ≤ M
this : ∀ (n : ℕ+), |∫ (x : ℝ) in Set.Ioi a, (φ x - y) * DiracSeq (↑↑n) x| ≤ M * ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - y) * DiracSeq (↑↑n) x) atTop (nhds 0)

case this
a : ℝ
ha : 0 < a
φ : ℝ → ℝ
hφ : IsBump φ
y M : ℝ
hM : ∀ (x : ℝ), ‖φ x - y‖ ≤ M
n : ℕ+
⊢ |∫ (x : ℝ) in Set.Ioi a, (φ x - y) * DiracSeq (↑↑n) x| ≤ M * ∫ (x : ℝ) in Set.Ioi a, DiracSeq (↑↑n) x