You're crazy. Don't bother to try to understand lean's internal models unless you want to work on lean itself. 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. :)