mathlib in emacs

Stream: new members

[Bob Bass]

Hello, everyone!
My first post.
While I have not yet started working with Lean in earnest, I appear to have Lean 3 working on emacs 27.1 with lean-mode and I would prefer not to use vscode.
Would you please help me get mathlib set up so that I can work through the book?
I'm using Lubuntu 22.04 on a PC laptop.
Thanks in advance.

[Johan Commelin]

@Bob Bass How did you install everything? Because the installation instructions on leanprover-community.github.io should give you working projects out of the box. Do you have leanproject installed? Also: which book are you talking about?

[Bob Bass]

@Johan Commelin Hi, Johan!
Sorry I didn't stick around long enough to catch your reply.
I've reformulated my question here: post