mathlib

b790b27d - feat(slim_check): sampleable instance for generating functions and injective functions (#3967)

feat(slim_check): sampleable instance for generating functions and injective functions (#3967) This also adds `printable_prop` to trace why propositions hold or don't hold and `sampleable_ext` to allow the data structure generated and shrunken by `slim_check` to have a different type from the type we are looking for.