Why is lean 4 behaving differently on my machine vs in the natural number game?

Question

In the lean 4 version of the natural number game at https://adam.math.hhu.de/#/g/leanprover-community/NNG4/ , I can use tactics like apply x at h and induction b with d hd.

In my local copy of lean, which I believe is v4.4.0-rc1, these things cause errors. For example, induction fails when given a with d hd suffix:

theorem lt_implies_le (a b : Nat)
  (h: a < b)
  : a <= b
  := by
    induction b with d hd  -- "unknown tactic"

and apply fails when given an at h suffix:

theorem lt_implies_le (a b : Nat)
  (h: a < b)
  : a <= b
  := by
    induction b
    trivial
    induction a
    simp
    apply Nat.succ_le_succ
    apply Nat.succ_le_succ at h  -- unexpected token 'at'; expected command

What is going on? Why is it behaving differently?

Answer 1

You need to install Mathlib and then import it with import Mathlib.

Also you need to use induction' instead of induction to get the equivalent behavior to the natural number game.

With Mathlib installed, this example from the game works with an import:

import Mathlib

example
  (x y : ℕ)
  (h1 : x = 37)
  (h2 : x = 37 → y = 42)
  : y = 42 := by
  apply h2 at h1
  exact h1

and it doesn't work without the import:

example
  (x y : ℕ)
  (h1 : x = 37)          -- failed to synthesize instance
  (h2 : x = 37 → y = 42) -- failed to synthesize instance
  : y = 42 := by         -- failed to synthesize instance
  apply h2 at h1         -- unexpected token 'at'
  exact h1