Commit 2026-05-20 07:15 0956725d

feat: add and use custom (d)elaborators for mvfderiv, add basic API lemmas (#39554) Add a custom elaborator (scoped to the Manifold namespace) shortening mvfderiv I f to d% f, and have a corresponding delaborator also. Their implementation is fully analogous to the existing elaborators. Also, rewrite Lie bracket lemmas to use mvfderiv instead of open-coding it. Part of #36036, i.e. from the path towards the Levi-Civita connection and Riemanian curvature. Related to fixing defeq abuses related to tangent space and scalar multiplication in mathlib.