[Merged by Bors] - chore: classify added to speed up elaboration porting notes#10695

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

pitmonticone/added-to-speedup-elableanprover-community/mathlib4:pitmonticone/added-to-speedup-elabCopy head branch name to clipboard