mathlib3

feat(category_theory/bifunctor): simp lemmas

#867

Merged