[Merged by Bors] - chore(CategoryTheory/Limits/Shapes/SequentialProduct): remove an erw#38519

yuanyi-350 wants to merge 1 commit intoleanprover-community:masterleanprover-community/mathlib4:masterfrom

yuanyi-350:E_13yuanyi-350/yuanyi_mathlib4:E_13Copy head branch name to clipboard