`lean.inductionWithNoAlts`

Induction pattern with nontactic in natural-number-game-style `with` clause.

Severity: ErrorSince: 4.26.0

Tactic-based proofs using induction in Lean need to use a pattern-matching-like notation to describe individual cases of the proof. However, the induction' tactic in Mathlib and the specialized induction tactic for natural numbers used in the Natural Number Game follows a different pattern.

Examples

Adding Explicit Cases to an Induction Proof

theorem zero_mul (m : Nat) : 0 * m = 0 := by
  induction m Invalid syntax for induction tactic: The `with` keyword must followed by a tactic or by an alternative (e.g. `| zero =>`), but here it is followed by the identifier `n`.with n n_ih
  rw [Nat.mul_zero]
  rw [Nat.mul_succ]
  rw [Nat.add_zero]
  rw [n_ih]

unknown tactic

theorem zero_mul (m : Nat) : 0 * m = 0 := by
  induction m with
  | zero =>
    rw [Nat.mul_zero]
  | succ n n_ih =>
    rw [Nat.mul_succ]
    rw [Nat.add_zero]
    rw [n_ih]

The broken example has the structure of a correct proof in the Natural Numbers Game, and this proof will work if you import Mathlib and replace induction with induction'. Induction tactics in basic Lean expect the with keyword to be followed by a series of cases, and the names for the inductive case are provided in the succ case rather than being provided up-front.