refactor(Topology/Category): refactor Profinite.Basic

[dagurtomas]

This is the second part of the refactor of CompHaus and friends (refactoring the definition of Profinite in terms of CompHausLike, see #12930 for the end result)

---

• [x] depends on: #13904
• [x] depends on: #13905
• [x] depends on: #13907
• [ ] depends on: #13908

[github-actions[bot]]

PR summary 9308991747

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Topology.Category.Profinite.Basic	1295	1293	-2 (-0.15%)
Mathlib.Topology.Category.Profinite.Product	1296	1294	-2 (-0.15%)
Mathlib.Topology.Category.Profinite.AsLimit	1299	1297	-2 (-0.15%)
Mathlib.Topology.Category.Profinite.CofilteredLimit	1305	1303	-2 (-0.15%)
Mathlib.Topology.Category.LightProfinite.Basic	1326	1324	-2 (-0.15%)
Mathlib.Topology.Category.Profinite.Limits	1338	1337	-1 (-0.07%)

Import changes for all files

Files	Import difference
7 files Mathlib.Topology.Category.Profinite.CofilteredLimit Mathlib.Topology.Category.Profinite.AsLimit Mathlib.Topology.Category.Profinite.Basic Mathlib.Topology.Category.Compactum Mathlib.Topology.Category.LightProfinite.Basic Mathlib.Topology.Category.LightProfinite.Sequence Mathlib.Topology.Category.Profinite.Product	-2
Mathlib.Topology.Category.LightProfinite.Limits Mathlib.Topology.Category.Profinite.Limits	-1

---

Declarations diff

+ FintypeCat.toProfiniteFullyFaithful + instance (X : Type*) [TopologicalSpace X] + instance : FintypeCat.toProfinite.Faithful := FintypeCat.toProfiniteFullyFaithful.faithful + instance : FintypeCat.toProfinite.Full := FintypeCat.toProfiniteFullyFaithful.full - Profinite - Profinite.toTopCat - Profinite.to_compHausToTopCat - category - coe_comp - coe_id - concreteCategory - forget_ContinuousMap_mk - forget_reflectsIsomorphisms - hasForget₂ - homeoOfIso - instance : CoeSort Profinite Type* - instance : FintypeCat.toProfinite.Faithful - instance : FintypeCat.toProfinite.Full - instance : Profinite.toTopCat.Faithful - instance : Profinite.toTopCat.Full - instance : profiniteToCompHaus.Faithful - instance : profiniteToCompHaus.Full - instance {X : Profinite} : CompactSpace ((forget Profinite).obj X) := by - instance {X : Profinite} : T2Space ((forget Profinite).obj X) := by - instance {X : Profinite} : TopologicalSpace ((forget Profinite).obj X) := by - instance {X Y : Profinite} (f : X ⟶ Y) [@Epi CompHaus _ _ _ f] : Epi f := by - instance {X Y : Profinite} (f : X ⟶ Y) [Epi f] : @Epi CompHaus _ _ _ f := by - isClosedMap - isIso_of_bijective - isoEquivHomeo - isoOfBijective - isoOfHomeo - mono_iff_injective - of - profiniteToCompHaus

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#13904~~
• ~~leanprover-community/mathlib4#13905~~
• ~~leanprover-community/mathlib4#13907~~
• ~~leanprover-community/mathlib4#13908~~ By Dependent Issues (🤖). Happy coding!

[kim-em]

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style