Commit 2025-11-20 07:16 56c98a55

chore: remove unused Decidable* instances in theorem types (#31831) 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 in order to put the ones that do require DecidableRel in a section.
• [lean4#5565](https://github.com/leanprover/lean4/issues/5595) forces us to change two instances to @[instance] theorem because of a failure in omit. We preserve the autogenerated name here.