convert MellinOfDeltaSpike Ψ εpos 1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
⊢ 𝓜 (fun x => ↑(DeltaSpike Ψ ε x)) 1 = 𝓜 (fun x => ↑(Ψ x)) ↑ε
case h.e'_3.h.e'_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
⊢ ↑ε = ↑ε * 1