[Merged by Bors] - chore(CategoryTheory): make Under implicit_reducible#41998

YaelDillies wants to merge 1 commit into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

YaelDillies:under_implicit_reducibleYaelDillies/mathlib4:under_implicit_reducibleCopy head branch name to clipboard