refactor(data/finsupp): add decidable_eq (#6333)
... when the statement (not the proof) of the theorem depends on a
decidability assumption. This prevents instance mismatch issues in
downstream theorems.
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
