What do I need to import from MathLib to make `induction a with d hd` work?

Question

I know that I need to import Mathlib to make rewrite [x] at h work. But induction a with d hd still doesn't work with just import Mathlib. This syntax does work in the natural number game, so I know it's possible to make it work.

What do I need to import to make this example work?

import Mathlib

theorem zero_add (n : ℕ) : 0 + n = n := by
induction n with d hd  -- ERROR: unknown tactic
rw [add_zero]
rfl
rw [add_succ]
rw [hd]
rfl

In fact, what are all the imports used by the natural number game?

(Note: this is a follow-up to Why is lean 4 behaving differently on my machine vs in the natural number game?). It would also be acceptable to edit the answer there to include all the imports needed.

Answer 1

I think currently in Mathlib that version is called induction' not induction. So the full command is induction' n with d hd. You can import it with import Mathlib.Tactic or just import Mathlib.

I think the reason there is a separate induction' tactic is because Lean 4 changed the syntax of induction. To be able to still use the old syntax, Mathlib added induction'. This made it easier to translate the old Lean 3 proofs. (And maybe the users like the induction' syntax better. I don't know.) If you want to use the new induction tactic, you can write:

theorem zero_add (n : Nat) : 0 + n = n := by
induction n with
| zero => 
  rw [Nat.add_zero]
| succ d hd =>
  rw [Nat.add_succ]
  rw [hd]

This is arguably more general and easier to work with arbitrarily complicated inductive structures.

(As for why it is different in the Natural Number Game, I think the Natural Number Game is a slight approximation of Lean + Mathlib, or at least it was for the Lean 3 version. They probably thought it was less confusing to rename induction' back to induction. Also, note how the Natural Number Game's rw is closer to rewrite. In Lean 4, rw automatically tries rfl at the end, but rewrite doesn't.)