Have you tried "Mathematics in Lean"? It's in the Books section here, along with a few other resources:

https://leanprover-community.github.io/learn.html

Yes I am aware of this one, it seems like a good intro.

I am just thinking more along the lines of - other than times where a computer is not available to us, why do we keep using traditional notion/pen and paper at all?

If everything is digitalized no one will have mark homework ever again.