I think the withNaryArg 2 delab can also be extracted to the assertNonCanonical function as the output.

Unfortunately, doing that means that we commit to failing if this particular instance is non-canonical -- I don't think we can use <|> anymore, so behavior changes from NAND (not both canonical, at least one is non-canonical) to NOR (neither is canonical, succeeds only if both are non-canonical).

Everything else looks reasonable, though, so I'll try and bundle up a next iteration with it, thanks!

EDIT: Hmmm... Actually, this can still work, we just have to return the result unconditionally and just flag whether or not it was canonical.

(Also, the resulting assertNonCanonical is no longer bound to TopologicalSpace and belongs somewhere more general; suggestions?)

Why not Mathlib.Topology.Defs.Basic?

I see, it's because of the bug right (might be worth explaining this in a comment too)

Yep. Though actually, now that I think about it... while most topologies are hard to implement without importing a bunch of Set lemmas, the discrete topology probably is doable.

Also, I could just fill in the proofs with sorries. Do you think that's better or worse than a bigger export?

I think in general you can do whatever you want in tests, even using axioms.

What bug are we talking about?

synthInstance and friends don't work properly in #check, #guard_target when used with opaque typeclass assumptions/variable definitions; we need an actual concrete type with an actual concrete canonical instance in order to make a linter that checks what we want, and it's actually kinda hard to make a TopologicalSpace instance without importing a whole bunch of the Set API anyway. At which point, we might as well just import Mathlib.Topology.Order, which among other things gives us the discrete topology on any type.