!4#3872 Topology.Category.Compactum

Stream: mathlib4

[Moritz Firsching]

Here, there was

def forget : Compactum ⥤ Type _ :=
  Monad.forget _ deriving CreatesLimits, Faithful
#align Compactum.forget Compactum.forget

and the deriving failed, so I added:

instance : Faithful forget :=
show Faithful <| Monad.forget _ from inferInstance

instance : CreatesLimits forget :=
show CreatesLimits <| Monad.forget _ from inferInstance

which worked fine for Faithful but for Creates limits it only worked after adding `noncomputable. Is it ok to have noncomputable here?

Another problem:
In some places it failes to synthesize instance TopologicalSpace X.A for a Compactum X, and I haven't been able fix that. What is the best way to get this instance?