[Merged by Bors] - chore: classify lemma was not necessary porting notes (category theory)#10674

pitmonticone wants to merge 6 commits intomasterleanprover-community/mathlib4:masterfrom

pitmonticone/lemma-was-not-necessaryleanprover-community/mathlib4:pitmonticone/lemma-was-not-necessaryCopy head branch name to clipboard