You can but that ruins the fun and also misses the point. How do you know your "trivial" theorem is actually trivial? Proofs are mechanized to increase our trust into them, and it defeats the point if you have to still manually review a myriad of helper lemmas.
Yeah I guess it's more a question of methodology for me. You have several parts of a proof, and your intuition guides you that certain parts are more likely to be risky than others. Better to get those straight first since you've a higher chance of failure (potentially rendering much of the work you have already done pointless). Then you can come back to flesh out the hopefully more straightforward parts. This is as opposed to taking a purely bottom-up approach. At least that's how I often tackle a complex coding problem - I am no mathematician!
