mathlib3

efdce094 - refactor(topology/constructions): turn `cofinite_topology` into a type synonym (#11967)

refactor(topology/constructions): turn `cofinite_topology` into a type synonym (#11967) Instead of `cofinite_topology α : topological_space α`, define `cofinite_topology α := α` with an instance `topological_space (cofinite_topology α) := (old definition)`. This way we can talk about cofinite topology without using `@` all over the place. Also move `homeo_of_equiv_compact_to_t2.t1_counterexample` to `topology.alexandroff` and prove it for `alexandroff ℕ` and `cofinite_topology (alexandroff ℕ)`.