The usual analogy here is an infinite line of dominos: if you knock down the first domino (show the base case holds) and know that each domino will knock down the domino after it (show the inductive case holds), then you know that all dominos will be knocked down (the proposition will hold for all natural numbers). The Lean proof window will now show the following two goals, the base case and the inductive case: In case you lost track at some point, here is a link to the Lean web editor with the full proof (move your cursor to the end of each line to see the proof state at that position).