[Merged by Bors] - refactor(Topology/Category): refactor CompHaus.Basic

[dagurtomas]

This PR refactors the file CompHaus.Basic in terms of the new CompHausLike API. Other files are touched only to fix errors created by this refactor, they will be refactored later (in particular, the API for explicit limits will be mostly removed in favour of the general API for explicit limits in CompHausLike, see #12930).

---

• depends on: [Merged by Bors] - refactor(Topology/Category): add CompHausLike.Basic #13904
• depends on: [Merged by Bors] - refactor(Topology/Category): add CompHausLike.Limits #13905
• depends on: [Merged by Bors] - refactor(Topology/Category): add CompHausLike.EffectiveEpi #13907

[github-actions]

PR summary 77b5a55be6

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Topology.Category.CompHaus.Basic	1288	1287	-1 (-0.08%)
Mathlib.Topology.Category.Profinite.Basic	1296	1295	-1 (-0.08%)
Mathlib.Topology.Category.Compactum	1301	1300	-1 (-0.08%)
Mathlib.Topology.Category.Stonean.Basic	1315	1314	-1 (-0.08%)

Import changes for all files

Files	Import difference
13 files Mathlib.Topology.Category.Stonean.Adjunctions Mathlib.Topology.Category.Profinite.CofilteredLimit Mathlib.Topology.Category.Profinite.AsLimit Mathlib.Topology.Category.CompHaus.Basic Mathlib.Topology.Category.CompHaus.Projective Mathlib.Topology.Category.Profinite.Projective Mathlib.Topology.Category.Profinite.Basic Mathlib.Topology.Category.Compactum Mathlib.Topology.Category.Stonean.Basic Mathlib.Topology.Category.Locale Mathlib.Order.Category.Frm Mathlib.Topology.Category.Profinite.Product Mathlib.Topology.Order.Category.FrameAdjunction	-1
5 files Mathlib.Condensed.Light.Explicit Mathlib.Condensed.Light.TopComparison Mathlib.Condensed.Light.Module Mathlib.Condensed.Light.Discrete Mathlib.Condensed.Epi	1

---

Declarations diff

+ instance : HasProp (fun _ ↦ True) X := ⟨trivial⟩
- CompHaus
- CompHaus.forget_reflectsIsomorphisms
- category
- coe_of
- coe_toTop
- compHausToTop
- concreteCategory
- instance (X : CompHaus) : CompactSpace (compHausToTop.obj X)
- instance (X : CompHaus) : T2Space (compHausToTop.obj X)
- instance (X : CompHaus.{u}) : CompactSpace ((forget CompHaus).obj X)
- instance (X : CompHaus.{u}) : T2Space ((forget CompHaus).obj X)
- instance (X : CompHaus.{u}) : TopologicalSpace ((forget CompHaus).obj X)
- instance : compHausToTop.Faithful
- instance : compHausToTop.Full
- isClosedMap
- isIso_of_bijective
- isoEquivHomeo
- isoOfBijective
- isoOfHomeo
- mono_iff_injective
- of
--++--+ homeoOfIso

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:

• [Merged by Bors] - refactor(Topology/Category): add CompHausLike.Basic #13904
• [Merged by Bors] - refactor(Topology/Category): add CompHausLike.Limits #13905
• [Merged by Bors] - refactor(Topology/Category): add CompHausLike.EffectiveEpi #13907
  By Dependent Issues (🤖). Happy coding!

[riccardobrasca]

Thanks!

bors d+

[mathlib-bors]

✌️ dagurtomas can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[dagurtomas]

bors merge

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Build failed:

• Build

[dagurtomas]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style