apply continuousOn_id.mul (continuousOn_id.log ?_) |>.sub continuousOn_id
case refine_1
𝕂 : 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
⊢ ContinuousOn f (Ici 1)
𝕂 : 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 ∈ Ici 1, id x ≠ 0