[Merged by Bors] - chore: classify rfl required porting notes#11442

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

pitmonticone/rfl-requiredleanprover-community/mathlib4:pitmonticone/rfl-requiredCopy head branch name to clipboard