why lean-repl can't identify "norm_num" tactic?

Stream: general

[Zihao Zhang]

Screenshot from 2024-12-19 14-26-16.png

[Kim Morrison]

@Zihao Zhang, is it just that you didn't specify the "env" field of your second command, so you're working in a fresh environment without the import Mathlib?