[Merged by Bors] - feat: custom elaborators for differential geometry#27021

grunweg wants to merge 108 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

grunweg:diffgeo-custom-elaboratorsgrunweg/mathlib4:diffgeo-custom-elaboratorsCopy head branch name to clipboard