rw [(by simp [f] : -1 = f 1), (by simp : c * Real.log c - c = f c)]
𝕂 : 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
⊢ -1 < c * c.log - c
𝕂 : 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
⊢ f 1 < f c