feat: add and use custom (d)elaborators for mvfderiv, add basic API lemmas (leanprover-community#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 leanprover-community#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.

Co-authored-by: Heather Macbeth [25316162+hrmacbeth@users.noreply.github.com](mailto:25316162+hrmacbeth@users.noreply.github.com)
Co-authored-by: Patrick Massot [patrickmassot@free.fr](mailto:patrickmassot@free.fr)

Author: grunweg

Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean

@@ -18,7 +18,10 @@ differentiability.
 
 In addition to the above, this file provides
 * results about the differentiability of scalar multiplication (`mfderiv_smul` and friends), and
-* `mvfderiv`: the exterior derivative of a scalar function, as a section of the cotangent bundle
+* `mvfderiv`: the exterior derivative of a vector-valued function, as a section of the
+  cotangent bundle; adds notation `d% f` for `mvfderiv I f` via a custom elaborator scoped to the
+  `Manifold` namespace, with a corresponding delaborator, and
+  adds basic lemmas about `mvfderiv` (such as addition, subtraction, multiplication and constants).
 
 -/
 
@@ -404,26 +407,98 @@ as a section of the cotangent bundle.
 
 Future: this could be generalised to functions into additive torsors over abelian Lie groups.
 -/
-noncomputable abbrev mvfderiv (g : M → F) :
+@[expose]
+noncomputable def mvfderiv (g : M → F) :
     Π x : M, TangentSpace I x →L[𝕜] F :=
   fun x ↦ (NormedSpace.fromTangentSpace <| g x).toContinuousLinearMap ∘L (mfderiv% g x)
-
 @[deprecated (since := "2026-05-17")] alias extDerivFun := mvfderiv
 
-@[simp]
+namespace Manifold
+open scoped Bundle Manifold ContDiff
+
+open Lean Meta Elab Tactic
+
+/-- `d% f x` (scoped to the `Manifold` namespace) elaborates to `mvfderiv I J f x`,
+trying to determine `I` and `J` from the local context. -/
+scoped elab:max "d%" ppSpace t:term:arg : term => do
+  let e ← ensureIsFunction <| ← Term.elabTerm t none
+  let (srcI, _tgtI) ← findModels e none
+  mkAppM ``mvfderiv #[srcI, e]
+
+open Bundle PrettyPrinter Delaborator SubExpr
+
+/-- Delaborator for `mvfderiv`. -/
+-- There is no need to special-case any arguments which could use the T% s elaborator:
+-- the argument to `mvfderiv` is a vector-valued function, which a map to a total space
+-- can never be.
+@[app_delab mvfderiv] meta def delab_mvfderiv : Delab := do
+  whenPPOption getPPNotation do
+  withOverApp 15 do
+  let fs ← withAppArg delab
+  `(d% $fs) >>= annotateGoToSyntaxDef
+
+section tests
+
+variable {f : M → 𝕜}
+
+/-- info: d% f : (x : M) → TangentSpace I x →L[𝕜] 𝕜 -/
+#guard_msgs in
+#check mvfderiv I f
+/-- info: d% f : (x : M) → TangentSpace I x →L[𝕜] 𝕜 -/
+#guard_msgs in
+#check d% f
+
+/-- info: d% f x : TangentSpace I x →L[𝕜] 𝕜 -/
+#guard_msgs in
+#check mvfderiv I f x
+
+/-- info: d% f x : TangentSpace I x →L[𝕜] 𝕜 -/
+#guard_msgs in
+#check d% f x
+
+end tests
+
+end Manifold
+
+lemma mvfderiv_const (c : F) {x : M} : d% (fun _ : M ↦ c) x = 0 := by
+  simp [mvfderiv, mfderiv_const]
+
+@[simp, to_fun mvfderiv_fun_add]
 lemma mvfderiv_add {g g' : M → F} {x : M} (hg : MDiffAt g x) (hg' : MDiffAt g' x) :
-    mvfderiv I (g + g') x = mvfderiv I g x + mvfderiv I g' x := by
+    d% (g + g') x = d% g x + d% g' x := by
   simp [mvfderiv, mfderiv_add hg hg']
-  congr
-
+  rfl
 @[deprecated (since := "2026-05-17")] alias extDerivFun_add := mvfderiv_add
 
+@[simp, to_fun mvfderiv_fun_sub]
+lemma mvfderiv_sub {g g' : M → F} {x : M} (hg : MDiffAt g x) (hg' : MDiffAt g' x) :
+    d% (g - g') x = d% g x - d% g' x := by
+  simp [mvfderiv, mfderiv_sub hg hg']
+  rfl
+
+@[simp, to_fun mvfderiv_fun_neg]
+lemma mvfderiv_neg {g : M → F} {x : M} :
+    d% (-g) x = -d% g x := by
+  simp [mvfderiv, mfderiv_neg]
+  rfl
+
+@[simp, to_fun mvfderiv_fun_smul]
+lemma mvfderiv_smul {x : M} {a : M → 𝕜} (ha : MDiffAt a x) {g : M → F} (hg : MDiffAt g x) :
+    d% (a • g) x = a x • d% g x + (d% a x).smulRight (g x) := by
+  ext v
+  simp [mvfderiv, -Pi.smul_apply', fromTangentSpace_mfderiv_smul_apply ha hg]
+
+@[simp, to_fun mvfderiv_fun_mul]
+lemma mvfderiv_mul {f g : M → 𝕜} {x : M} (hf : MDiffAt f x) (hg : MDiffAt g x) :
+    d% (f * g) x = f x • d% g x + (g x) • (d% f x) := by
+  ext v
+  simp only [mvfderiv, ← smul_eq_mul, mfderiv_smul hf hg]
+  simp [mul_comm _ (g x)]
+
 @[simp]
-lemma mvfderiv_zero {x : M} : mvfderiv (I := I) (0 : M → F) x = 0 := by
-  have : mvfderiv I (0 : M → F) x + mvfderiv I (0 : M → F) x =
-      mvfderiv I (0 : M → F) x := by
+lemma mvfderiv_zero {x : M} : d% (0 : M → F) x = 0 := by
+  have : d% (0 : M → F) x + d% (0 : M → F) x = d% (0 : M → F) x := by
     rw [← mvfderiv_add (by exact mdifferentiable_const ..) (by exact mdifferentiable_const ..)]
     simp
   simpa using this
-
 @[deprecated (since := "2026-05-17")] alias extDerivFun_zero := mvfderiv_zero

Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/Basic.lean

@@ -96,7 +96,7 @@ structure IsCovariantDerivativeOn
     cov (σ + σ') x = cov σ x + cov σ' x
   leibniz {σ : Π x : M, V x} {g : M → 𝕜} {x}
     (hσ : MDiffAt (T% σ) x) (hg : MDiffAt g x) (hx : x ∈ s := by trivial) :
-    cov (g • σ) x = g x • cov σ x + (mvfderiv I g x).smulRight (σ x)
+    cov (g • σ) x = g x • cov σ x + (d% g x).smulRight (σ x)
 
 /--
 A covariant derivative ∇ is called of class `C^k` iff, whenever `X` is a `C^k` section and `σ` a
@@ -270,15 +270,14 @@ lemma finite_affine_combination {ι : Type*} {s : Finset ι}
     rw [← smul_add, (h i).add hσ hσ' hx]
   leibniz {σ g x} hσ hg hx := by
     calc ∑ i ∈ s, f i x • cov i (g • σ) x
-      _ = ∑ i ∈ s, (g x • f i x • cov i σ x + f i x • (mvfderiv I g x).smulRight (σ x)) := by
+      _ = ∑ i ∈ s, (g x • f i x • cov i σ x + f i x • (d% g x).smulRight (σ x)) := by
           congr! 1 with i hi
           rw [(h i).leibniz hσ hg]
           simp [mvfderiv]
           module
-      _ = g x • ∑ i ∈ s, f i x • cov i σ x +
-        (∑ i ∈ s, f i) x • (mvfderiv I g x).smulRight (σ x) := by
+      _ = g x • ∑ i ∈ s, f i x • cov i σ x + (∑ i ∈ s, f i) x • (d% g x).smulRight (σ x) := by
           rw [Finset.sum_add_distrib, Finset.smul_sum, Finset.sum_apply, Finset.sum_smul]
-      _ = g x • ∑ i ∈ s, f i x • cov i σ x + (mvfderiv I g x).smulRight (σ x) := by rw [hf]; simp
+      _ = g x • ∑ i ∈ s, f i x • cov i σ x + (d% g x).smulRight (σ x) := by rw [hf]; simp
 
 /-- An affine combination of finitely many `C^k` connections on `u` is a `C^k` connection on `u`. -/
 lemma _root_.ContMDiffCovariantDerivativeOn.finite_affine_combination [IsManifold I 1 M]

Mathlib/Geometry/Manifold/VectorField/LieBracket.lean

@@ -390,11 +390,9 @@ Product rule for Lie brackets: given two vector fields `V` and `W` on `M` and a
 -/
 lemma mlieBracket_smul_right {f : M → 𝕜} (hf : MDiffAt f x)
     (hW : MDiffAt (fun x ↦ (W x : TangentBundle I M)) x) :
-    mlieBracket I V (f • W) x =
-      (fromTangentSpace (f x) (mfderiv% f x (V x))) • (W x)
-      + (f x) • mlieBracket I V W x := by
+    mlieBracket I V (f • W) x = d% f x (V x) • (W x) + (f x) • mlieBracket I V W x := by
   rw [← mdifferentiableWithinAt_univ] at hf hW
-  rw [← mlieBracketWithin_univ, ← mfderivWithin_univ]
+  rw [← mlieBracketWithin_univ, mvfderiv, ← mfderivWithin_univ]
   exact mlieBracketWithin_smul_right hf hW (uniqueMDiffWithinAt_univ I)
 
 /--
@@ -417,11 +415,9 @@ Product rule for Lie brackets: given two vector fields `V` and `W` on `M` and a
 -/
 lemma mlieBracket_smul_left {f : M → 𝕜} (hf : MDiffAt f x)
     (hV : MDiffAt (fun x ↦ (V x : TangentBundle I M)) x) :
-    mlieBracket I (f • V) W x =
-      - (fromTangentSpace (f x) (mfderiv% f x (W x))) • (V x)
-      + (f x) • mlieBracket I V W x := by
+    mlieBracket I (f • V) W x = - d% f x (W x) • (V x) + (f x) • mlieBracket I V W x := by
   rw [← mdifferentiableWithinAt_univ] at hf hV
-  rw [← mlieBracketWithin_univ, ← mfderivWithin_univ]
+  rw [← mlieBracketWithin_univ, mvfderiv, ← mfderivWithin_univ]
   exact mlieBracketWithin_smul_left hf hV (uniqueMDiffWithinAt_univ I)
 
 lemma mlieBracketWithin_const_smul_left