import Mathlib

-- Theorem: For any natural number n, n + 0 = n.
theorem demo (n : ℕ) : n + 0 = n := by
  /- <feedback>
  -- proof state:
  n : ℕ
  ⊢ n + 0 = n
  </feedback> -/
  induction n with
  /- <feedback>
  -- proof state:
  case zero
  ⊢ 0 + 0 = 0
  </feedback> -/
  | zero => rfl
  /- <feedback>
  -- proof state:
  ih : n + 0 = n
  case succ
  ⊢ n + 1 + 0 = n + 1
  </feedback> -/
  | succ n ih => simp_all