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

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?

• Perhaps you need to import Mathlib? Dec 5, 2023 at 1:12
• @FrançoisG.Dorais Why would importing Mathlib change the availability of syntax like an "at" clause on apply? Dec 5, 2023 at 1:17
• Because it's defined in Mathlib. Lean's syntax is extendible. Dec 5, 2023 at 1:18
• @FrançoisG.Dorais This does seem to be the problem. Definitely very confusing. Especially because the natural number game doesn't include the import in its example code. Dec 5, 2023 at 1:20
• I think NNG automatically includes Mathlib in the background. Dec 5, 2023 at 1:22

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