exact mono (by rw [mem_Ici]) (mem_Ici.mpr <| le_of_lt hc) hc
𝕂 : 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
mono : StrictMonoOn f (Ici 1)
⊢ f 1 < f c
no goals