[Merged by Bors] - feat(subtype): standardize

[fpvandoorn]

Add simp lemma from x.val to coe x
Use correct ext/ext_iff naming scheme
Use coe in more places in the library

---

[fpvandoorn]

There are some cases where it got better:

• there were some ext, rw subtype.ext, ext sequences that now become ext.
• there were some places where simp did more

There are some places where it got worse:

• On types defined as subtypes, the coercion doesn't work, but simp still simplifies val into the coercion. That is not ideal. That means I had to add [-subtype.val_eq_coe] to simp sometimes.

I changed subtype.val to coe in a lot of places, but of course only in places near an error, definitely not everywhere. I expect a bunch of linter failures of the form LHS is not in normal form.

[fpvandoorn]

There were only few linter errors.

@kappelmann: I had to remove some simp lemmas in continued fractions, because they went in the other direction (simplifying from coercion to subtype.val). I think they were unused, though.

[fpvandoorn]

Trying to rebase on this branch (which will probably need to go through a couple of iterations of fixes): https://github.com/leanprover-community/mathlib/compare/subtype_rebase

[fpvandoorn]

I think there are no more errors here. I would appreciate a quick merge, as this PR is likely to break quickly.

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Lint mathlib
• Build mathlib
• Run tests and docs