Theorem: MellinOfDeltaSpikeAt1 (PrimeNumberTheoremAnd/MellinCalculus.lean)

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

State before:
case h.e'_3.h.e'_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
⊢ ↑ε = ↑ε * 1
Tactic:
simp [mul_one]
State after:
no goals