feat(data/part): Lemmas for get on binary function instances (#12194)
feat(data/part): Lemmas for get on binary function instances (#12194)


A variety of lemmas such as `mul_get_eq` for `part`.





leanprover-community/mathlib,leanprover-community/mathlib