mathlib3

f8d8465c - chore(category_theory/preadditive/projective): split out two lemmas to reduce imports (#18688)

chore(category_theory/preadditive/projective): split out two lemmas to reduce imports (#18688) Motivated by all the unneeded imports visible in https://tqft.net/mathlib4/2023-03-29/category_theory.monoidal.tor.pdf Co-authored-by: Scott Morrison <scott.morrison@gmail.com>