mathlib3

e42af8da - refactor(topology/category/Profinite): define Profinite as a subcategory of CompHaus (#8314)

refactor(topology/category/Profinite): define Profinite as a subcategory of CompHaus (#8314) This adjusts the definition of Profinite to explicitly be a subcategory of CompHaus rather than a subcategory of Top which embeds into CompHaus. Essentially this means it's easier to construct an element of Profinite from an element of CompHaus.