Add delaborator checking canonicity of instances

Following a Zulip discussion
https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Topological.20.28scoped.29.20notation.20in.20doc-gen/near/565193294
I'm suggesting that we introduce some fix to (topological) scoped notation not showing up in the doc-gen.

More concretely, observe that on this file one finds the definition of open/closed/etc... with respect to non-standard topologies, so that one can write IsOpen[T] (U : Set X), for instance, to mean that a set U is open wrt to the topology T rather than wrt any other topology that might be synthesized on X. This I find very convenient, but it does not show up in the doc-gen so that, for example, while reading docs#LinearMap.mem_span_iff_continuous_of_finite online one has no clue of the topology on E with respect to which φ would be continuous — whereas in the source this is very clear.

Compare the scoped notation definitions in Mathlib/Topology/Defs/Basic.lean with the generated documentation for LinearMap.mem_span_iff_continuous_of_finite, using the linked source in Mathlib/Analysis/LocallyConvex/WeakDual.lean as the reference. Start by tracing doc-gen's delaboration of these declarations; done means the generated docs make the relevant topology or instance context clear.