(1) I always tell my students that if they don't understand why things are done a certain way, that they should try to do it in the way most natural to them and then iterate to improve it. Eventually they will settle on something very similar to most common practice.

(2) Higher-level proofs are using so many ideas simultaneously that doing this would be tantamount to writing Lean code from scratch: painful.