refine mul_le_mul_of_nonneg_right (hM x) (DiracSeq.nonneg_nat x)
case this.refine_2
a : ℝ
ha : 0 < a
φ : ℝ → ℝ
hφ : IsBump φ
y M : ℝ
hM : ∀ (x : ℝ), ‖φ x - y‖ ≤ M
n : ℕ+
x : ℝ
⊢ |φ x - y| * DiracSeq (↑↑n) x ≤ M * DiracSeq (↑↑n) x
no goals