[Merged by Bors] - chore: classify used to be dsimp porting notes#10935

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

pitmonticone/used-to-be-dsimpleanprover-community/mathlib4:pitmonticone/used-to-be-dsimpCopy head branch name to clipboard