> Whatever style of proof you're used to, you can write in that style with mathlib.

Yes, you can do that, and it'll be a frustrating experience.

Knowing the theoretical foundations of your tool is a great way to be happy and productive.

Without it you have issues similar to people trying to implement parsers with regex. :)