[Merged by Bors] - chore: classify deprecated porting notes#11230

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

pitmonticone/deprecatedleanprover-community/mathlib4:pitmonticone/deprecatedCopy head branch name to clipboard