rw [Asymptotics.isBigO_iff] at h ⊢
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
h : (fun ε => 𝓜 (fun x => ↑(Ψ x)) ↑ε - 1) =O[𝓝[>] 0] id
⊢ (fun ε => 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) 1 - 1) =O[𝓝[>] 0] id
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
h : ∃ c, ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖𝓜 (fun x => ↑(Ψ x)) ↑x - 1‖ ≤ c * ‖id x‖
⊢ ∃ c, ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖𝓜 (fun x_1 => ↑(Smooth1 Ψ x x_1)) 1 - 1‖ ≤ c * ‖id x‖