This PR removes `Decidable*` instances that are not used by the remainder of a theorem's type and so can be replaced by `classical` in the proof (found by the  #31142). This allows us to turn on the `unusedDecidableInType` linter, which is done in #31747.

Notes:

- We rearrange the order of theorems slightly in [Mathlib/Combinatorics/SimpleGraph/Bipartite.lean](https://github.com/leanprover-community/mathlib4/pull/31747/files#diff-8acbd485d15b1e94a2afaf205ebedba12259361421342c715188192f1b0045f8) in order to put the ones that do require `DecidableRel` in a section.
- [lean4#5565](leanprover/lean4#5595) forces us to change two `instance`s to `@[instance] theorem` because of a failure in `omit`. We preserve the autogenerated name here.

Co-authored-by: thorimur <thomasmurrills@gmail.com>

This PR removes `Decidable*` instances that are not used by the remainder of a theorem's type and so can be replaced by `classical` in the proof (found by the  #31142). This allows us to turn on the `unusedDecidableInType` linter, which is done in #31747.

Notes:

- We rearrange the order of theorems slightly in [Mathlib/Combinatorics/SimpleGraph/Bipartite.lean](https://github.com/leanprover-community/mathlib4/pull/31747/files#diff-8acbd485d15b1e94a2afaf205ebedba12259361421342c715188192f1b0045f8) in order to put the ones that do require `DecidableRel` in a section.
- [lean4#5565](leanprover/lean4#5595) forces us to change two `instance`s to `@[instance] theorem` because of a failure in `omit`. We preserve the autogenerated name here.

Co-authored-by: thorimur <thomasmurrills@gmail.com>

This PR turns on the `unusedDecidableInType` syntax linter (#31142) after fixing the remaining violations in #31831, #31934, and #32153.

This also imports the linter into Mathlib.Init and adds the linter to the Mathlib standard set. Given that classicality is embedded in Lean, this is probably the behavior downstream repos who use the mathlib standard set want; if they are specifically constructive repos, the linter can always be turned off in the lakefile.

We exempt the entirety of [Mathlib/Data/Fintype/Quotient.lean](https://github.com/leanprover-community/mathlib4/pull/31747/files#diff-9591d2f3828bee189ea954bc33586ce451536bf00792362f7cdca4f5a8551207), [Mathlib/Order/Heyting/Regular.lean](https://github.com/leanprover-community/mathlib4/pull/31747/files#diff-af85d99e5d2f5561fe837f662f179c58f1ebe2a4ed0432a15260199883850c50), [Mathlib/Logic/Encodable/Basic.lean](https://github.com/leanprover-community/mathlib4/pull/31747/files#diff-db01c9a2d4726fe7ca0e6eb18a7cd485b5a9c6b26ba422dfbe501dcebef3cf77) and a declaration in [Mathlib/Computability/Halting.lean](https://github.com/leanprover-community/mathlib4/pull/31747/files#diff-d47323ee8b4b2321052b4be93715f8b2f3f840f76ec441d8bf75c834b8665b32) since constructivity is desired there. We also exempt `dec_em'`, which is a variant of `Decidable.em` but with the disjuncts reversed.

Many prior violations have already been fixed through the use of #10235, hence the small number of violations picked up by the syntax linter.

Co-authored-by: thorimur <thomasmurrills@gmail.com>
Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>