linarith
𝕂 : 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 : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
a✝ : 2 ^ (-ε) ≤ x / y
⊢ 0 < y
no goals