[Merged by Bors] - chore: cleanup of adaptation notes#37922

kim-em wants to merge 3 commits intomasterleanprover-community/mathlib4:masterfrom

cleanup_adaptation_notesleanprover-community/mathlib4:cleanup_adaptation_notesCopy head branch name to clipboard