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

[yyyhz]

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?

[objecti0n]

https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAWQIYwBYBtgCMBQEwCmAdnAEoFLo45oHQEhzoVED6A7tANZYQResATADY4ACgAecAFxxAuIQBKcaimyADHAA8cCUtlSAtHACMcQKZEZCugB06CAHMdMgLxwsATxxw4RTESRQwGhwANp29qzMrADOAK5YrBBEBIkAZqyQ0XAqALpAA

I think you need open Real

[yyyhz]

Thank you very much for your answer, I can run it on the web version! But locally, using open real requires LeanDOJO, but after setting it up according to your README, it comes up with something like:[{'theorem': 'amc12a_2019_p21', 'success': False, 'failure_reason': 'DojoInitError'}] Error Reporting.