Lean is more complex to develop in than most programming languages since it relies heavily on interactive programming, i.e. the context pane. The "easy way" is with a plugin.
If you're interested in learning more about Lean for writing proofs, I would recommend The Mechanics of Proof [0]. It strips out a lot of the convenience tactics in Mathlib to focus on the more primitive mechanisms Mathlib builds on.