Aaron Liu

feat: fix some issues with `equals t => tac`

2

This PR fixed some issues with the `conv` tactic `equals t => tac`: - It gives bad error messages when `t` has the wrong type. For example, ``` type mismatch...

Theorem Suggestion: A characterization of Finite T0 spaces

1

## Theorem Suggestion If a space is: - **sober** [P73](https://topology.pi-base.org/properties/P000073) - **alexandrov** [P90](https://topology.pi-base.org/properties/P000090) - **noetherian** [P208](https://topology.pi-base.org/properties/P000208) then it is **finite** [P78](https://topology.pi-base.org/properties/P000078). ## Rationale This theorem would give a characterization of...

Complete S195 "Join of cofinite and left-ray topologies on ω1​"

3

I have many proofs to write down. Currently trying to fill out the properties for [S195](https://topology.pi-base.org/spaces/S000195)

feat(Topology): Completely Regular Space iff Uniformizable

8

This PR continues the work from #24096. Original PR: https://github.com/leanprover-community/mathlib4/pull/24096 --------- - [x] depends on: #32140