Junyan Xu

There's [one place](https://github.com/leanprover-community/mathlib/pull/16046/files/18de6dfa7934eddbe01e965617e10ef88d5931d8..99168dda843fa7f4e1c3d986a88f62102d4553cc) where an earlier `convert` proof breaks due to an added subsingleton instance, which I consider as a bug of `convert`, because the goal it created can simply...

Sorry, the last comment (deleted) is meant for the other PR.

No problem; it's fun to think about these proofs!

With your `exists_compact_superset'` you can now remove [exists_compact_between](https://leanprover-community.github.io/mathlib_docs/topology/separation.html#exists_compact_between) which has the extraneous t3_space assumption. The same assumption could be removed from `exists_open_between_and_is_compact_closure` as well, but this lemma seems not used...

Oh sorry, I now realize t3_space can't be totally removed from `exists_open_between_and_is_compact_closure`, but it can be replaced by `t2_space` given your lemma; as soon as you want the closure of...

I've been able to [adapt the proof](https://github.com/leanprover-community/mathlib/commit/fab824b466fa41b53eb0283ca49045b3ad48a487#diff-22c682b7d3ddbda2c1e6e6def47aa08b91b4ebe038ff016e4d2894939047b561R1039) of `exists_compact_superset` to more easily prove `exists_compact_between`, and then `exists_compact_superset` becomes a trivial consequence. Feel free to merge! (Update: I've also golfed `continuous_prod`...

I've basically done all the things I mentioned above in that branch, so you can just merge it and then I think this PR is good to go. If you...

This link is the diff between the branches but I agree the diff is a bit large, mainly because some lemmas are moved; but you can also check individual commits...

Yes, it appears to be a squash merge. Thanks!

It's interesting that you opened another PR on github and merged it to a nonmaster branch, instead of doing it locally. I never tried it and it's nice to know...