[Merged by Bors] - fix(deprecated/*): remove instances

[jcommelin]

Remove all instances constructing structures from is_* predicates, like for example:

instance subset.ring {S : set R} [is_subring S] : ring S :=
...

Co-Authored-By: Gabriel Ebner gebner@gebner.org

---

[gebner]

I think lowering the instance priority for whole files is the wrong way to fix this issue. We should only lower the priority of a single instance, and understand what caused this issue in the first place. Ideally there'd also be a linter.

Do you have an MWE?

[jcommelin]

Re MWE, see the test file.
Note that the problem goes away if you remove any of the following three ingredients:

• change unit -> R to a module like M
• change L.subtype to some hom f
• remove the tensor_product.map L.subtype, and just ask for injectivity of L.subtype.

[jcommelin]

We deprecated these files because we realised that these things shouldn't use the typeclass system. So I think it makes sense to actually lower the priority for the entire file.

[gebner]

Ok, didn't look too closely at the file names. I'm still a bit uneasy, because we'll probably still have timeouts in type-class searches that should fail (lowering the priority typically doesn't help here).

If we're going to remove the files soon anyhow, then I won't bother debugging this.

[jcommelin]

I don't think these files will go away... 😢
What should happen, is that someone refactors these files so that they are all about semibundled structures, instead of classes. But that refactor is very painful. I tried it and failed.

[urkud]

LGTM

[ChrisHughes24]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests