exact log_pos hx
case refine_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
f : ℝ → ℝ := fun x => x * x.log - x
x : ℝ
hx : 1 < x
⊢ 0 < x.log
no goals