[Merged by Bors] - chore: classify avoid simpNF linter error porting notes#10760

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

pitmonticone/avoid-linter-errorleanprover-community/mathlib4:pitmonticone/avoid-linter-errorCopy head branch name to clipboard