mathlib3

68d2d213 - feat(testing/slim_check): teach slim_check about `finsupp`s (#10916)

feat(testing/slim_check): teach slim_check about `finsupp`s (#10916) We add some instances so that `slim_check` can generate `finsupp`s and hence try to provide counterexamples for them. As the way the original slim_check for functions works is to generate a finite list of random values and pick a default for the rest of the values these `total_functions` are quite close to finsupps already, we just have to map the default value to zero, and prove various things about the support. There might be conceptually nicer ways of building this instance but this seems functional enough. Seeing as many finsupp defs are classical (and noncomputable) this isn't quite as useful for generating counterexamples as I originally hoped. See the test at `test/slim_check.lean` for a basic example of usage I wrote this while working on flt-regular but it is hopefully useful outside of that Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>