exact log_pos (by norm_num)
case h.left
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
⊢ 0 < c

case h.right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
⊢ ∀ (x : ℝ), 0 < x → x ≤ 1 - c * ε → Smooth1 Ψ ε x = 1
case h.right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
⊢ ∀ (x : ℝ), 0 < x → x ≤ 1 - c * ε → Smooth1 Ψ ε x = 1