[Merged by Bors] - chore: classify @[simp] removed porting notes#11121

pitmonticone wants to merge 1 commit intomasterleanprover-community/mathlib4:masterfrom

pitmonticone/@-simp]-removedleanprover-community/mathlib4:pitmonticone/@-simp]-removedCopy head branch name to clipboard