Very few proofs in actual professional mathematics are written in a formal proof structure where what you suggest is actually possible. You definitely need to u

Very few proofs in actual professional mathematics are written in a formal proof structure where what you suggest is actually possible. You definitely need to understand the underlying ideas to follow along. "rewrite in lean when" isn't really practical (at least yet).