Is the proof included in the Lean-workbook ensured to be correct?

I used the header you provided and integrated the formal_statement and proof. Only to find that some cases pass lean server and some don't.
For example:
theorem lean_workbook_26 (x : ℝ) (hx : 0 < x) : x - 1 ≥ Real.log x := by
nlinarith [log_le_sub_one_of_pos hx]
will display error：unknown identifier 'log_le_sub_one_of_pos'
Do you know how to fix it?