pushforwardObj claims unexpected notation

Stream: mathlib4

[Eric Wieser]

This is pretty surprising behavior:

import Mathlib.Tactic

example : 1 * 2 = 2 * 1 := by
  show _*_ = _*_ -- works
  norm_num

import Mathlib

example : 1 * 2 = 2 * 1 := by
  show _*_ = _*_ -- fails
  norm_num

Can we change docs#TopCat.Presheaf.pushforwardObj to use less intrusive notation?

[Kyle Miller]

It ought to be scoped at least!

[Eric Wieser]

Also, was there a better way for me to track this down than pruning imports until it worked?

[Eric Wieser]

Can I get Lean to tell me what it thinks the tokens are?

[Damiano Testa]

Eric, is this the list of tokens?

import Lean.Elab.Command

open Lean Parser in
run_cmd
  logInfo m!"{(getTokenTable (← getEnv)).values}"