[Merged by Bors] - chore: golf proofs of mdifferentiableAt_atlas{_symm}#42011

grunweg wants to merge 1 commit into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

grunweg:golf-mdiff-atlas-symmgrunweg/mathlib4:golf-mdiff-atlas-symmCopy head branch name to clipboard