refactor: add TC cycles

[urkud]

In Lean 3, many lemmas are not instances to avoid loops. I think that we should not turn them into instances while porting. Instead, we should turn them into instances all at once after the port is done and see how does it affect build time. For now, we should create a list of these lemmas.

• normalOfCompactT2;
• T3Space.mk (any T₀ regular space is a T₃ space);
• normalSpaceOfT3SecondCountable;
• compact_t2_tot_disc_iff_tot_sep (the Iff.mp implication);
• loc_compact_t2_tot_disc_iff_tot_sep;
• UniformSpace.secondCountable_of_separable

[alexjbest]

One thing to note here is that loops which have data in are still potentially dangerous I believe.

It doesn't look like this affects Yury's examples, but for example one might want the instance that a finite integral domain is a field, as this instance presumably will construct the inv field out of some nontrivial mathematics.
This can cause issues when we have an existing finite field which has a well defined inverse but we now have two ways of getting the inverse, the original one and the one constructed by the mathematical theorem that a finite integral domain is a field.
Maybe priorities are enough to fix this? I'm not sure

[alreadydone]

Related: #6646

There are still mysterious issues impairing performance even for Prop-valued classes. (See also Zulip)

[urkud]

@alexjbest Indeed, I'm talking about Prop-valued classes only.