Make typeclass synthesis try harder

Stream: mathlib4

[Andrew Yang]

In #21904, there's a new lemma (finite type artinian algebra over field is (module) finite) that ideally should be instances, but couldn't be because of performance reasons. There are other occasions of this occurring in mathlib, e.g. docs#Module.finitePresentation_of_finite, docs#Module.finitePresentation_of_projective, and (one direction of) docs#posMulStrictMono_iff_mulPosStrictMono etc.
I wonder if it makes sense to throw them all into a scoped[TryHarder] for discoverability, where the user is intended to find the right instance and attribute [local instance] it. And possibly a linter against opening it in mathlib.
We might even be able to lump all the "not instance due to diamond" things in it as well.

[Kyle Miller]

I kind of like the idea. What if there is an ExpensiveInstances sub-namespace that theories can populate, so maybe you'd do open scoped Module.ExpensiveInstances? If you already have Module open, it would just be open scoped ExpensiveInstances, and I think the way open works is that this will do open scoped on all ExpensiveInstances namespaces that are currently accessible.