apply diffΨ.continuous.comp (g := Ψ) _ |>.div_const
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
diffΨ : ContDiff ℝ 1 Ψ
⊢ Continuous fun x => DeltaSpike Ψ ε x
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
diffΨ : ContDiff ℝ 1 Ψ
⊢ Continuous fun x => x ^ (1 / ε)