mathlib

0fe91d0d - feat(data/part): Instance lemmas (#12001)

feat(data/part): Instance lemmas (#12001) Lemmas about `part` instances, proved by `tidy` Co-authored-by: Eric Wieser <wieser.eric@gmail.com>