Commit 2026-05-31 10:14 919544d4

feat: add mvfderivWithin with (d)elaborators and basic API (#39513) Add mvfderivWithin (a version of mvfderiv within a set) and add analogues of all mvfderiv lemmas. We also add analogous custom elaborators and delaborators. To prove our set-up works, we re-phrase two lemmas in VectorField/LieBracket.lean to use this definition, instead of open-coding it. In passing, we also note a few areas in differential geometry that rely on similar defeq abuse, and should be cleaned up to use mvfderiv (this will be addressed in future PRs). Part of https://github.com/leanprover-community/mathlib4/pull/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.