scope of local notations

Stream: mathlib4

[Joël Riou]

In !4#5224 AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf there is a notation which should be local, but which just does not work at all when I write local notation....

[Matthew Ballard]

Explained clearly here https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/no.20macro.20or.20.60.5Bquot_precheck.5D.60.20instance.20for.20syntax.20kind/near/373071387

[Kyle Miller]

@Joël Riou @Matthew Ballard #5758 fixes the notation so it pretty prints.

The notation command can't handle local variable variables, but notation3 can handle them (with the same limitation as notation of not being able to handle dot notation).