!4#3487 last minute split?

Stream: mathlib4

[Scott Morrison]

In Porting goals for Copenhagen @Adam Topaz says he needs both

• topology.category.CompHaus.projective
• topology.category.Profinite.as_limit

ported to prepare for the Copenhagen workshop.

Both of these files are waiting on !4#3487, porting Topology.Category.Top.Limits. This PR has many errors, and after doing a quick pass many don't look easy.

However I realised, and checked in mathlib3, that Adam's two files actually only depend on the very first part of this file, and in fact as of today we have cleared the errors in that section.

Thus, I propose we do a later-than-last-minute split of topology.category.Top.limits into smaller pieces (this was overdue in any case, the file is too big, and why did the topological König lemma not get its own file in the first place?).

We will then mostly throw out the parts of !4#3487 that port past that point, and restart them as needed.

This will immediately unblock progress on the requirements for the Copenhagen workshop.

[Scott Morrison]

I haven't actually done the mathlib3 split, just checked that if you comment things out Adam's two files still compile. However I think I'll go do that now, so if anyone thinks this is a terrible idea they should please tell me soon. :-)

[Johan Commelin]

Sounds good to me

[Johan Commelin]

@Scott Morrison If you have a PR with the ml3 split, please ping me

[Scott Morrison]

@Johan Commelin https://github.com/leanprover-community/mathlib/pull/18871

[Scott Morrison]

Okay, I have now chopped down https://github.com/leanprover-community/mathlib4/pull/3487 to match.