mathlib4 refactor(Topology/Category): refactor CompHaus.Basic

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).

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

Jun 17 '24 20:06 dagurtomas

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

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

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>

Jun 17 '24 20:06 github-actions[bot]

This PR/issue depends on:

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

Jul 04 '24 14:07 leanprover-community-mathlib4-bot

Thanks!

bors d+

Jul 16 '24 11:07 riccardobrasca

:v: 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.