The complete typechecked Lean 4 proof is:

```lean4
import Mathlib


theorem demo (n : ℕ) : n + 0 = n := by 
  
  induction n with
  
  | zero => rfl
  
  | succ n ih => simp_all
```