It is one thing to "prove by induction that this loop will end" and another completely to write a specification for the compiler to find a proof for you.

Lean is an interactive proof assistant, not an ATP. If you're actively using Lean (or for that matter any other proof assistant), you're definitely "learning how to make proofs". Induction-based proofs, specifically, are notoriously hard to automate.