Bad TopCat.Presheaf.pushforward notation

Stream: mathlib4

[Eric Wieser]

I'm sure I made this thread before, but now I can't find it. The following code works:

example : ∃ x, x = 2 * 3 := by
  exact ⟨_*_, rfl⟩

but with import Mathlib, it fails:

import Mathlib

example : ∃ x, x = 2 * 3 := by
  exact ⟨_*_, rfl⟩ -- bizarre error message

-- the notation parses as this now!
#check _ _* _

Can we make this notation scoped, or pick something different?

[Eric Wieser]

#17101