CategoryTheory.Monoidal.Category

Stream: mathlib4

[Matej Penciak]

I started the port of this file (!4#2318) and it seems like MathPort had a hard time with notation that is introduced in the definition of a structure.

I'm fixing all these things by hand, but I was curious if there were any other workarounds?