diff --git a/Mathlib.lean b/Mathlib.lean
index fefaa8a1c7a81e..0eeae4be8d1618 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3928,6 +3928,7 @@ import Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
 import Mathlib.Geometry.Manifold.MFDeriv.Tangent
 import Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
 import Mathlib.Geometry.Manifold.Metrizable
+import Mathlib.Geometry.Manifold.Notation
 import Mathlib.Geometry.Manifold.PartitionOfUnity
 import Mathlib.Geometry.Manifold.PoincareConjecture
 import Mathlib.Geometry.Manifold.Riemannian.Basic
diff --git a/Mathlib/Geometry/Manifold/Notation.lean b/Mathlib/Geometry/Manifold/Notation.lean
new file mode 100644
index 00000000000000..52b60ff0e38028
--- /dev/null
+++ b/Mathlib/Geometry/Manifold/Notation.lean
@@ -0,0 +1,482 @@
+/-
+Copyright (c) 2025 Patrick Massot. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Patrick Massot, Michael Rothgang, Thomas Murrills
+-/
+import Mathlib.Geometry.Manifold.ContMDiff.Defs
+import Mathlib.Geometry.Manifold.MFDeriv.Defs
+
+/-!
+# Elaborators for differential geometry
+
+This file defines custom elaborators for differential geometry to allow for more compact notation.
+We introduce a class of elaborators for handling differentiability on manifolds, and the elaborator
+`T%` for converting dependent sections of fibre bundles into non-dependent functions into the total
+space.
+
+All of these elaborators are scoped to the `Manifold` namespace.
+
+## Differentiability on manifolds
+
+We provide compact notation for differentiability and continuous differentiability on manifolds,
+including inference of the model with corners.
+
+| Notation            | Elaborates to                       |
+|---------------------|-------------------------------------|
+| `MDiff f`           | `MDifferentiable I J f`             |
+| `MDiffAt f x`       | `MDifferentiableAt I J f x`         |
+| `MDiff[u] f`        | `MDifferentiableOn I J f u`         |
+| `MDiffAt[u] f x`    | `MDifferentiableWithinAt I J f u x` |
+| `CMDiff n f`        | `ContMDiff I J n f`                 |
+| `CMDiffAt n f x`    | `ContMDiffAt I J n f x`             |
+| `CMDiff[u] n f`     | `ContMDiffOn I J n f u`             |
+| `CMDiffAt[u] n f x` | `ContMDiffWithinAt I J n f u x`     |
+| `mfderiv[u] f x`    | `mfderivWithin I J f u x`           |
+| `mfderiv% f x`      | `mfderiv I J f x`                   |
+
+In each of these cases, the models with corners are inferred from the domain and codomain of `f`.
+The search for models with corners uses the local context and is (almost) only based on expression
+structure, hence hopefully fast enough to always run.
+
+This has no dedicated support for product manifolds (or product vector spaces) yet;
+adding this is left for future changes. (It would need to make a choice between e.g. the
+trivial model with corners on a product `E × F` and the product of the trivial models on `E` and
+`F`). In these settings, the elaborators should be avoided (for now).
+
+## `T%`
+
+Secondly, this file adds an elaborator `T%` to ease working with sections in a fibre bundle,
+which converts a section `s : Π x : M, V x` to a non-dependent function into the total space of the
+bundle.
+```lean
+-- omitted: let `V` be a fibre bundle over `M`
+
+variable {σ : Π x : M, V x} in
+#check T% σ -- `(fun x ↦ TotalSpace.mk' F x (σ x)) : M → TotalSpace F V`
+
+-- Note how the name of the bound variable `x` is preserved.
+variable {σ : (x : E) → Trivial E E' x} in
+#check T% σ -- `(fun x ↦ TotalSpace.mk' E' x (σ x)) : E → TotalSpace E' (Trivial E E')`
+
+variable {s : E → E'} in
+#check T% s -- `(fun a ↦ TotalSpace.mk' E' a (s a)) : E → TotalSpace E' (Trivial E E')`
+```
+
+---
+
+These elaborators can be combined: `CMDiffAt[u] n (T% s) x`
+
+**Warning.** These elaborators are a proof of concept; the implementation should be considered a
+prototype. Don't rewrite all of mathlib to use it just yet. Notable bugs and limitations include
+the following.
+
+## TODO
+- extend the elaborators to guess models with corners on product manifolds
+  (this has to make a guess, hence cannot always be correct: but it could make the guess that
+  is correct 90% of the time).
+  For products of vector spaces `E × F`, this could print a warning about making a choice between
+  the model in `E × F` and the product of the models on `E` and `F`.
+- extend the elaborators to support `OpenPartialHomeomorph`s and `PartialEquiv`s
+- better error messages (as needed)
+- further testing and fixing of edge cases
+- add tests for all of the above
+- add delaborators for these elaborators
+
+-/
+
+open scoped Bundle Manifold ContDiff
+
+open Lean Meta Elab Tactic
+open Mathlib.Tactic
+open Qq
+
+namespace Manifold.Elab
+
+/- Note: these functions are convenient in this file, and may be convenient elsewhere, but their
+precise behavior should be considered before adding them to the meta API. -/
+
+/-- Finds the first local instance of class `c` for which `p inst type` produces `some a`.
+Instantiates mvars in and runs `whnfR` on `type` before passing it to `p`. (Does not validate that
+`c` resolves to a class.) -/
+private def findSomeLocalInstanceOf? (c : Name) {α} (p : Expr → Expr → MetaM (Option α)) :
+    MetaM (Option α) := do
+  (← getLocalInstances).findSomeM? fun inst ↦ do
+    if inst.className == c then
+      let type ← whnfR <|← instantiateMVars <|← inferType inst.fvar
+      p inst.fvar type
+    else return none
+
+/-- Finds the most recent local declaration for which `p fvar type` produces `some a`.
+Skips implementation details; instantiates mvars in and runs `whnfR` on `type` before providing it
+to `p`. -/
+private def findSomeLocalHyp? {α} (p : Expr → Expr → MetaM (Option α)) : MetaM (Option α) := do
+  (← getLCtx).findDeclRevM? fun decl ↦ do
+    if decl.isImplementationDetail then return none
+    let type ← whnfR <|← instantiateMVars decl.type
+    p decl.toExpr type
+
+end Elab
+
+open Elab in
+/--
+Elaborator for sections in a fibre bundle: converts a section `s : Π x : M, V x` as a dependent
+function to a non-dependent function into the total space. This handles the cases of
+- sections of a trivial bundle
+- vector fields on a manifold (i.e., sections of the tangent bundle)
+- sections of an explicit fibre bundle
+- turning a bare function `E → E'` into a section of the trivial bundle `Bundle.Trivial E E'`
+
+This elaborator searches the local context for suitable hypotheses for the above cases by matching
+on the expression structure, avoiding `isDefEq`. Therefore, it is (hopefully) fast enough to always
+run.
+-/
+-- TODO: document how this elaborator works, any gotchas, etc.
+-- TODO: factor out `MetaM` component for reuse
+scoped elab:max "T% " t:term:arg : term => do
+  let e ← Term.elabTerm t none
+  let etype ← whnf <|← instantiateMVars <|← inferType e
+  match etype with
+  | .forallE x base tgt _ => withLocalDeclD x base fun x ↦ do
+    let tgtHasLooseBVars := tgt.hasLooseBVars
+    let tgt := tgt.instantiate1 x
+    -- Note: we do not run `whnfR` on `tgt` because `Bundle.Trivial` is reducible.
+    match_expr tgt with
+    | Bundle.Trivial E E' _ =>
+      trace[Elab.DiffGeo.TotalSpaceMk] "Section of a trivial bundle"
+      -- Note: we allow `isDefEq` here because any mvar assignments should persist.
+      if ← withReducible (isDefEq E base) then
+        let body ← mkAppM ``Bundle.TotalSpace.mk' #[E', x, e.app x]
+        mkLambdaFVars #[x] body
+      else return e
+    | TangentSpace _k _ E _ _ _H _ _I _M _ _ _x =>
+      trace[Elab.DiffGeo.TotalSpaceMk] "Vector field"
+      let body ← mkAppM ``Bundle.TotalSpace.mk' #[E, x, e.app x]
+      mkLambdaFVars #[x] body
+    | _ => match (← instantiateMVars tgt).cleanupAnnotations with
+      | .app V _ =>
+        trace[Elab.DiffGeo.TotalSpaceMk] "Section of a bundle as a dependent function"
+        let f? ← findSomeLocalInstanceOf? `FiberBundle fun _ declType ↦
+          /- Note: we do not use `match_expr` here since that would require importing
+          `Mathlib.Topology.FiberBundle.Basic` to resolve `FiberBundle`. -/
+          match declType with
+          | mkApp7 (.const `FiberBundle _) _ F _ _ E _ _ => do
+            if ← withReducible (pureIsDefEq E V) then
+              let body ← mkAppM ``Bundle.TotalSpace.mk' #[F, x, e.app x]
+              some <$> mkLambdaFVars #[x] body
+            else return none
+          | _ => return none
+        return f?.getD e
+      | tgt =>
+        trace[Elab.DiffGeo.TotalSpaceMk] "Section of a trivial bundle as a non-dependent function"
+        -- TODO: can `tgt` depend on `x` in a way that is not a function application?
+        -- Check that `x` is not a bound variable in `tgt`!
+        if tgtHasLooseBVars then
+          throwError "Attempted to fall back to creating a section of the trivial bundle out of \
+            ({e} : {etype}) as a non-dependent function, but return type {tgt} depends on the bound
+            variable ({x} : {base}).\nHint: applying the `T%` elaborator twice makes no sense."
+        let trivBundle ← mkAppOptM ``Bundle.Trivial #[base, tgt]
+        let body ← mkAppOptM ``Bundle.TotalSpace.mk' #[base, trivBundle, tgt, x, e.app x]
+        mkLambdaFVars #[x] body
+  | _ => return e
+
+namespace Elab
+
+/-- Try a strategy `x : TermElabM` which either successfully produces some `Expr` or fails. On
+failure in `x`, exceptions are caught, traced (`trace.Elab.DiffGeo.MDiff`), and `none` is
+successfully returned.
+
+We run `x` with `errToSorry == false` to convert elaboration errors into
+exceptions, and under `withSynthesize` in order to force typeclass synthesis errors to appear and
+be caught.
+
+Trace messages produced during the execution of `x` are wrapped in a collapsible trace node titled
+with `strategyDescr` and an indicator of success. -/
+private def tryStrategy (strategyDescr : MessageData) (x : TermElabM Expr) :
+    TermElabM (Option Expr) := do
+  let s ← saveState
+  try
+    withTraceNode `Elab.DiffGeo.MDiff (fun e => pure m!"{e.emoji} {strategyDescr}") do
+      let e ←
+        try
+          Term.withoutErrToSorry <| Term.withSynthesize x
+        /- Catch the exception so that we can trace it, then throw it again to inform
+        `withTraceNode` of the result. -/
+        catch ex =>
+          trace[Elab.DiffGeo.MDiff] "Failed with error:\n{ex.toMessageData}"
+          throw ex
+      trace[Elab.DiffGeo.MDiff] "Found model: {e}"
+      return e
+  catch _ =>
+    -- Restore infotrees to prevent any stale hovers, code actions, etc.
+    -- Note that this does not break tracing, which saves each trace message's context.
+    s.restore true
+    return none
+
+/-- Try to find a `ModelWithCorners` instance on a type (represented by an expression `e`),
+using the local context to infer the appropriate instance. This supports the following cases:
+- the model with corners on the total space of a vector bundle
+- a model with corners on a manifold
+- the trivial model `𝓘(𝕜, E)` on a normed space
+- if the above are not found, try to find a `NontriviallyNormedField` instance on the type of `e`,
+  and if successful, return `𝓘(𝕜)`.
+
+Further cases can be added as necessary.
+
+Return an expression describing the found model with corners.
+
+`baseInfo` is only used for the first case, a model with corners on the total space of the vector
+bundle. In this case, it contains a pair of expressions `(e, i)` describing the type of the base
+and the model with corners on the base: these are required to construct the right model with
+corners.
+
+This implementation is not maximally robust yet.
+-/
+-- TODO: better error messages when all strategies fail
+-- TODO: consider lowering monad to `MetaM`
+def findModel (e : Expr) (baseInfo : Option (Expr × Expr) := none) : TermElabM Expr := do
+  trace[Elab.DiffGeo.MDiff] "Finding a model for: {e}"
+  if let some m ← tryStrategy m!"TotalSpace"   fromTotalSpace   then return m
+  if let some m ← tryStrategy m!"NormedSpace"  fromNormedSpace  then return m
+  if let some m ← tryStrategy m!"ChartedSpace" fromChartedSpace then return m
+  if let some m ← tryStrategy m!"NormedField"  fromNormedField  then return m
+  throwError "Could not find models with corners for {e}"
+where
+  /- Note that errors thrown in the following are caught by `tryStrategy` and converted to trace
+  messages. -/
+  /-- Attempt to find a model from a `TotalSpace` first by attempting to use any provided
+  `baseInfo`, then by seeing if it is the total space of a tangent bundle. -/
+  fromTotalSpace : TermElabM Expr := do
+    match_expr e with
+    | Bundle.TotalSpace _ F V => do
+      if let some m ← tryStrategy m!"From base info" (fromTotalSpace.fromBaseInfo F) then return m
+      if let some m ← tryStrategy m!"TangentSpace" (fromTotalSpace.tangentSpace V) then return m
+      throwError "Having a TotalSpace as source is not yet supported"
+    | _ => throwError "{e} is not a `Bundle.TotalSpace`."
+  /-- Attempt to use the provided `baseInfo` to find a model. -/
+  fromTotalSpace.fromBaseInfo (F : Expr) : TermElabM Expr := do
+    if let some (src, srcI) := baseInfo then
+      trace[Elab.DiffGeo.MDiff] "Using base info {src}, {srcI}"
+      let some K ← findSomeLocalInstanceOf? ``NormedSpace fun _ type ↦ do
+          match_expr type with
+          | NormedSpace K E _ _ =>
+            if ← withReducible (pureIsDefEq E F) then return some K else return none
+          | _ => return none
+        | throwError "Couldn't find a `NormedSpace` structure on {F} among local instances."
+      trace[Elab.DiffGeo.MDiff] "{F} is a normed field over {K}"
+      let kT : Term ← Term.exprToSyntax K
+      let srcIT : Term ← Term.exprToSyntax srcI
+      let FT : Term ← Term.exprToSyntax F
+      let iTerm : Term ← ``(ModelWithCorners.prod $srcIT 𝓘($kT, $FT))
+      Term.elabTerm iTerm none
+    else
+      throwError "No `baseInfo` provided"
+  /-- Attempt to find a model from the total space of a tangent bundle. -/
+  fromTotalSpace.tangentSpace (V : Expr) : TermElabM Expr := do
+    match_expr V with
+    | TangentSpace _k _ _E _ _ _H _ I M _ _ => do
+      trace[Elab.DiffGeo.MDiff] "This is the total space of the tangent bundle of {M}"
+      let srcIT : Term ← Term.exprToSyntax I
+      let resTerm : Term ← ``(ModelWithCorners.prod $srcIT (ModelWithCorners.tangent $srcIT))
+      Term.elabTerm resTerm none
+    | _ => throwError "{V} is not a `TangentSpace`"
+  /-- Attempt to find the trivial model on a normed space. -/
+  fromNormedSpace : TermElabM Expr := do
+    let some (inst, K) ← findSomeLocalInstanceOf? ``NormedSpace fun inst type ↦ do
+        match_expr type with
+        | NormedSpace K E _ _ =>
+          if ← withReducible (pureIsDefEq E e) then return some (inst, K) else return none
+        | _ => return none
+      | throwError "Couldn't find a `NormedSpace` structure on {e} among local instances."
+    trace[Elab.DiffGeo.MDiff] "Field is: {K}"
+    mkAppOptM ``modelWithCornersSelf #[K, none, e, none, inst]
+  /-- Attempt to find a model with corners on a manifold. -/
+  fromChartedSpace : TermElabM Expr := do
+    let some H ← findSomeLocalInstanceOf? ``ChartedSpace fun _ type ↦ do
+        match_expr type with
+        | ChartedSpace H _ M _ =>
+          if ← withReducible (pureIsDefEq M e) then return some H else return none
+        | _ => return none
+      | throwError "Couldn't find a `ChartedSpace` structure on {e} among local instances."
+    trace[Elab.DiffGeo.MDiff] "H is: {H}"
+    let some m ← findSomeLocalHyp? fun fvar type ↦ do
+        match_expr type with
+        | ModelWithCorners _ _ _ _ _ H' _ => do
+          if ← withReducible (pureIsDefEq H' H) then return some fvar else return none
+        | _ => return none
+      | throwError "Couldn't find a `ModelWithCorners` with model space {H} in the local context."
+    return m
+  /-- Attempt to find a model with corners from a normed field. We attempt to find a global
+  instance here. -/
+  fromNormedField : TermElabM Expr := do
+    let eT : Term ← Term.exprToSyntax e
+    let iTerm : Term ← ``(𝓘($eT, $eT))
+    Term.elabTerm iTerm none
+
+/-- If the type of `e` is a non-dependent function between spaces `src` and `tgt`, try to find a
+model with corners on both `src` and `tgt`. If successful, return both models.
+
+We pass `e` instead of just its type for better diagnostics.
+
+If `es` is `some`, we verify that `src` and the type of `es` are definitionally equal. -/
+def findModels (e : Expr) (es : Option Expr) : TermElabM (Expr × Expr) := do
+  let etype ← whnf <|← instantiateMVars <|← inferType e
+  match etype with
+  | .forallE _ src tgt _ =>
+    if tgt.hasLooseBVars then
+      -- TODO: try `T%` here, and if it works, add an interactive suggestion to use it
+      throwError "Term {e} is a dependent function, of type {etype}\nHint: you can use the `T%` \
+        elaborator to convert a dependent function to a non-dependent one"
+    let srcI ← findModel src
+    if let some es := es then
+      let estype ← inferType es
+      /- Note: we use `isDefEq` here since persistent metavariable assignments in `src` and
+      `estype` are acceptable.
+      TODO: consider attempting to coerce `es` to a `Set`. -/
+      if !(← isDefEq estype <|← mkAppM ``Set #[src]) then
+        throwError "The domain {src} of {e} is not definitionally equal to the carrier type of \
+          the set {es} : {estype}"
+    let tgtI ← findModel tgt (src, srcI)
+    return (srcI, tgtI)
+  | _ => throwError "Expected{indentD e}\nof type{indentD etype}\nto be a function"
+
+end Elab
+
+open Elab
+
+/-- `MDiffAt[s] f x` elaborates to `MDifferentiableWithinAt I J f s x`,
+trying to determine `I` and `J` from the local context.
+The argument `x` can be omitted. -/
+scoped elab:max "MDiffAt[" s:term "]" ppSpace f:term:arg : term => do
+  let es ← Term.elabTerm s none
+  let ef ← Term.elabTerm f none
+  let (srcI, tgtI) ← findModels ef es
+  mkAppM ``MDifferentiableWithinAt #[srcI, tgtI, ef, es]
+
+/-- `MDiffAt f x` elaborates to `MDifferentiableAt I J f x`,
+trying to determine `I` and `J` from the local context.
+The argument `x` can be omitted. -/
+scoped elab:max "MDiffAt" ppSpace t:term:arg : term => do
+  let e ← Term.elabTerm t none
+  let (srcI, tgtI) ← findModels e none
+  mkAppM ``MDifferentiableAt #[srcI, tgtI, e]
+
+-- An alternate implementation for `MDiffAt`.
+-- /-- `MDiffAt2 f x` elaborates to `MDifferentiableAt I J f x`,
+-- trying to determine `I` and `J` from the local context.
+-- The argument `x` can be omitted. -/
+-- scoped elab:max "MDiffAt2" ppSpace t:term:arg : term => do
+--   let e ← Term.elabTerm t none
+--   let etype ← whnfR <|← instantiateMVars <|← inferType e
+--   forallBoundedTelescope etype (some 1) fun src tgt ↦ do
+--     if let some src := src[0]? then
+--       let srcI ← findModel (← inferType src)
+--       if Lean.Expr.occurs src tgt then
+--         throwErrorAt t "Term {e} is a dependent function, of type {etype}\n\
+--         Hint: you can use the `T%` elaborator to convert a dependent function \
+--         to a non-dependent one"
+--       let tgtI ← findModel tgt (src, srcI)
+--       mkAppM ``MDifferentiableAt #[srcI, tgtI, e]
+--     else
+--       throwErrorAt t "Expected{indentD e}\nof type{indentD etype}\nto be a function"
+
+/-- `MDiff[s] f` elaborates to `MDifferentiableOn I J f s`,
+trying to determine `I` and `J` from the local context. -/
+scoped elab:max "MDiff[" s:term "]" ppSpace t:term:arg : term => do
+  let es ← Term.elabTerm s none
+  let et ← Term.elabTerm t none
+  let (srcI, tgtI) ← findModels et es
+  mkAppM ``MDifferentiableOn #[srcI, tgtI, et, es]
+
+/-- `MDiff f` elaborates to `MDifferentiable I J f`,
+trying to determine `I` and `J` from the local context. -/
+scoped elab:max "MDiff" ppSpace t:term:arg : term => do
+  let e ← Term.elabTerm t none
+  let (srcI, tgtI) ← findModels e none
+  mkAppM ``MDifferentiable #[srcI, tgtI, e]
+
+/-- `CMDiffAt[s] n f x` elaborates to `ContMDiffWithinAt I J n f s x`,
+trying to determine `I` and `J` from the local context.
+`n` is coerced to `WithTop ℕ∞` if necessary (so passing a `ℕ`, `∞` or `ω` are all supported).
+The argument `x` can be omitted. -/
+scoped elab:max "CMDiffAt[" s:term "]" ppSpace nt:term:arg ppSpace f:term:arg : term => do
+  let es ← Term.elabTerm s none
+  let ef ← Term.elabTerm f none
+  let ne ← Term.elabTermEnsuringType nt q(WithTop ℕ∞)
+  let (srcI, tgtI) ← findModels ef es
+  mkAppM ``ContMDiffWithinAt #[srcI, tgtI, ne, ef, es]
+
+/-- `CMDiffAt n f x` elaborates to `ContMDiffAt I J n f x`
+trying to determine `I` and `J` from the local context.
+`n` is coerced to `WithTop ℕ∞` if necessary (so passing a `ℕ`, `∞` or `ω` are all supported).
+The argument `x` can be omitted. -/
+scoped elab:max "CMDiffAt" ppSpace nt:term:arg ppSpace t:term:arg : term => do
+  let e ← Term.elabTerm t none
+  let ne ← Term.elabTermEnsuringType nt q(WithTop ℕ∞)
+  let (srcI, tgtI) ← findModels e none
+  mkAppM ``ContMDiffAt #[srcI, tgtI, ne, e]
+
+/-- `CMDiff[s] n f` elaborates to `ContMDiffOn I J n f s`,
+trying to determine `I` and `J` from the local context.
+`n` is coerced to `WithTop ℕ∞` if necessary (so passing a `ℕ`, `∞` or `ω` are all supported). -/
+scoped elab:max "CMDiff[" s:term "]" ppSpace nt:term:arg ppSpace f:term:arg : term => do
+  let es ← Term.elabTerm s none
+  let ef ← Term.elabTerm f none
+  let ne ← Term.elabTermEnsuringType nt q(WithTop ℕ∞)
+  let (srcI, tgtI) ← findModels ef es
+  mkAppM ``ContMDiffOn #[srcI, tgtI, ne, ef, es]
+
+/-- `CMDiff n f` elaborates to `ContMDiff I J n f`,
+trying to determine `I` and `J` from the local context.
+`n` is coerced to `WithTop ℕ∞` if necessary (so passing a `ℕ`, `∞` or `ω` are all supported). -/
+scoped elab:max "CMDiff" ppSpace nt:term:arg ppSpace f:term:arg : term => do
+  let e ← Term.elabTerm f none
+  let ne ← Term.elabTermEnsuringType nt q(WithTop ℕ∞)
+  let (srcI, tgtI) ← findModels e none
+  mkAppM ``ContMDiff #[srcI, tgtI, ne, e]
+
+/-- `mfderiv[u] f x` elaborates to `mfderivWithin I J f u x`,
+trying to determine `I` and `J` from the local context. -/
+scoped elab:max "mfderiv[" s:term "]" ppSpace t:term:arg : term => do
+  let es ← Term.elabTerm s none
+  let e ← Term.elabTerm t none
+  let (srcI, tgtI) ← findModels e es
+  mkAppM ``mfderivWithin #[srcI, tgtI, e, es]
+
+/-- `mfderiv% f x` elaborates to `mfderiv I J f x`,
+trying to determine `I` and `J` from the local context. -/
+scoped elab:max "mfderiv%" ppSpace t:term:arg : term => do
+  let e ← Term.elabTerm t none
+  let (srcI, tgtI) ← findModels e none
+  mkAppM ``mfderiv #[srcI, tgtI, e]
+
+end Manifold
+
+section trace
+
+/-!
+### Trace classes
+
+Note that the overall `Elab` trace class does not inherit the trace classes defined in this
+section, since they provide verbose information.
+-/
+
+/--
+Trace class for differential geometry elaborators. Setting this to `true` traces elaboration
+for the `T%` elaborator (`trace.Elab.DiffGeo.TotalSpaceMk`) and the family of `MDiff`-like
+elaborators (`trace.Elab.DiffGeo.MDiff`).
+-/
+initialize registerTraceClass `Elab.DiffGeo
+
+/--
+Trace class for the `T%` elaborator, which converts a section of a vector bundle as a dependent
+function to a non-dependent function into the total space.
+-/
+initialize registerTraceClass `Elab.DiffGeo.TotalSpaceMk (inherited := true)
+
+/--
+Trace class for the `MDiff` elaborator and friends, which infer a model with corners on the domain
+(resp. codomain) of the map in question.
+-/
+initialize registerTraceClass `Elab.DiffGeo.MDiff (inherited := true)
+
+end trace
diff --git a/MathlibTest/DifferentialGeometry/Notation.lean b/MathlibTest/DifferentialGeometry/Notation.lean
new file mode 100644
index 00000000000000..1620190e4fb9a9
--- /dev/null
+++ b/MathlibTest/DifferentialGeometry/Notation.lean
@@ -0,0 +1,1021 @@
+import Mathlib.Geometry.Manifold.Notation
+import Mathlib.Geometry.Manifold.VectorBundle.SmoothSection
+import Mathlib.Geometry.Manifold.VectorBundle.Tangent
+import Mathlib.Geometry.Manifold.MFDeriv.FDeriv
+import Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
+import Mathlib.Geometry.Manifold.BumpFunction
+import Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
+import Mathlib.Geometry.Manifold.VectorField.LieBracket
+
+set_option pp.unicode.fun true
+
+open Bundle Filter Function Topology
+
+open scoped Bundle Manifold ContDiff
+
+variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
+
+section
+
+variable {E : Type*} [NormedAddCommGroup E]
+  [NormedSpace 𝕜 E] {H : Type*} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H)
+  {M : Type*} [TopologicalSpace M] [ChartedSpace H M]
+
+variable {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E']
+
+variable (F : Type*) [NormedAddCommGroup F] [NormedSpace 𝕜 F]
+  -- `F` model fiber
+  (n : WithTop ℕ∞)
+  (V : M → Type*) [TopologicalSpace (TotalSpace F V)]
+  [∀ x, AddCommGroup (V x)] [∀ x, Module 𝕜 (V x)]
+  [∀ x : M, TopologicalSpace (V x)] [∀ x, IsTopologicalAddGroup (V x)]
+  [∀ x, ContinuousSMul 𝕜 (V x)]
+  [FiberBundle F V] [VectorBundle 𝕜 F V]
+  -- `V` vector bundle
+
+/-! Tests for the `T%` elaborator, inserting calls to `TotalSpace.mk'` automatically. -/
+section TotalSpace
+
+variable {σ : Π x : M, V x}
+  {σ' : (x : E) → Trivial E E' x} {σ'' : (y : E) → Trivial E E' y} {s : E → E'}
+
+/-- info: fun x ↦ TotalSpace.mk' F x (σ x) : M → TotalSpace F V -/
+#guard_msgs in
+#check T% σ
+
+-- Testing precedence.
+variable {x : M}
+/-- info: (fun x ↦ TotalSpace.mk' F x (σ x)) x : TotalSpace F V -/
+#guard_msgs in
+#check (T% σ) x
+/-- info: (fun x ↦ TotalSpace.mk' F x (σ x)) x : TotalSpace F V -/
+#guard_msgs in
+#check T% σ x
+-- Nothing happening, as expected.
+/-- info: σ x : V x -/
+#guard_msgs in
+#check T% (σ x)
+
+-- Note how the name of the bound variable `x` resp. `y` is preserved.
+/-- info: fun x ↦ TotalSpace.mk' E' x (σ' x) : E → TotalSpace E' (Trivial E E') -/
+#guard_msgs in
+#check T% σ'
+
+/-- info: fun y ↦ TotalSpace.mk' E' y (σ'' y) : E → TotalSpace E' (Trivial E E') -/
+#guard_msgs in
+#check T% σ''
+
+/-- info: fun a ↦ TotalSpace.mk' E' a (s a) : E → TotalSpace E' (Trivial E E') -/
+#guard_msgs in
+#check T% s
+
+variable (X : (m : M) → TangentSpace I m) [IsManifold I 1 M]
+
+/-- info: fun m ↦ TotalSpace.mk' E m (X m) : M → TotalSpace E (TangentSpace I) -/
+#guard_msgs in
+#check T% X
+
+example : (fun m ↦ (X m : TangentBundle I M)) = (fun m ↦ TotalSpace.mk' E m (X m)) := rfl
+
+-- Applying a section to an argument. TODO: beta-reduce instead!
+/-- info: (fun m ↦ TotalSpace.mk' E m (X m)) x : TotalSpace E (TangentSpace I) -/
+#guard_msgs in
+#check (T% X) x
+
+-- Applying the same elaborator twice is fine (and idempotent).
+/-- info: (fun m ↦ TotalSpace.mk' E m (X m)) x : TotalSpace E (TangentSpace I) -/
+#guard_msgs in
+#check (T% (T% X)) x
+
+end TotalSpace
+
+/-! Tests for the elaborators for `MDifferentiable{WithinAt,At,On}`. -/
+section differentiability
+
+-- Start with some basic tests: a simple function, both in applied and unapplied form.
+variable {EM' : Type*} [NormedAddCommGroup EM']
+  [NormedSpace 𝕜 EM'] {H' : Type*} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 EM' H')
+  {M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M']
+
+-- General case: a function between two manifolds.
+variable {f : M → M'} {s : Set M} {m : M}
+
+/-- info: MDifferentiableWithinAt I I' f s : M → Prop -/
+#guard_msgs in
+#check MDiffAt[s] f
+
+/-- info: MDifferentiableWithinAt I I' f s m : Prop -/
+#guard_msgs in
+#check MDiffAt[s] f m
+
+/-- info: MDifferentiableAt I I' f : M → Prop -/
+#guard_msgs in
+#check MDiffAt f
+
+/-- info: MDifferentiableAt I I' f m : Prop -/
+#guard_msgs in
+#check MDiffAt f m
+
+/-- info: MDifferentiableOn I I' f s : Prop -/
+#guard_msgs in
+#check MDiff[s] f
+
+-- Testing an error message.
+section
+
+/--
+error: Function expected at
+  MDifferentiableOn I I' f s
+but this term has type
+  Prop
+
+Note: Expected a function because this term is being applied to the argument
+  m
+-/
+#guard_msgs in
+#check MDiff[s] f m
+
+/--
+error: Function expected at
+  MDifferentiableOn I I' f s
+but this term has type
+  Prop
+
+Note: Expected a function because this term is being applied to the argument
+  m
+-/
+#guard_msgs in
+#check MDifferentiableOn I I' f s m
+
+/-- info: MDifferentiable I I' f : Prop -/
+#guard_msgs in
+#check MDiff f
+
+/--
+error: Function expected at
+  MDifferentiable I I' f
+but this term has type
+  Prop
+
+Note: Expected a function because this term is being applied to the argument
+  m
+-/
+#guard_msgs in
+#check MDiff f m
+
+end
+
+-- Testing the precedence of parsing of the "within" set: regression test.
+section
+
+variable {ι : Type} {i : ι} {s : ι → Set M}
+
+/-- info: MDifferentiableOn I I' f (s i) : Prop -/
+#guard_msgs in
+#check MDiff[s i] f
+/-- info: MDifferentiableWithinAt I I' f (s i) m : Prop -/
+#guard_msgs in
+#check MDiffAt[s i] f m
+/-- info: ContMDiffOn I I' 2 f (s i) : Prop -/
+#guard_msgs in
+#check CMDiff[s i] 2 f
+/-- info: ContMDiffWithinAt I I' 0 f (s i) m : Prop -/
+#guard_msgs in
+#check CMDiffAt[s i] 0 f m
+/-- info: mfderivWithin I I' f (s i) m : TangentSpace I m →L[𝕜] TangentSpace I' (f m) -/
+#guard_msgs in
+#check mfderiv[s i] f m
+
+end
+
+-- Function from a manifold into a normed space.
+variable {g : M → E}
+
+/-- info: MDifferentiableWithinAt I 𝓘(𝕜, E) g s : M → Prop -/
+#guard_msgs in
+#check MDiffAt[s] g
+/-- info: MDifferentiableWithinAt I 𝓘(𝕜, E) g s m : Prop -/
+#guard_msgs in
+#check MDiffAt[s] g m
+/-- info: MDifferentiableAt I 𝓘(𝕜, E) g : M → Prop -/
+#guard_msgs in
+#check MDiffAt g
+/-- info: MDifferentiableAt I 𝓘(𝕜, E) g m : Prop -/
+#guard_msgs in
+#check MDiffAt g m
+/-- info: MDifferentiableOn I 𝓘(𝕜, E) g s : Prop -/
+#guard_msgs in
+#check MDiff[s] g
+-- TODO: fix and enable! #check MDiff[s] g m
+/-- info: MDifferentiable I 𝓘(𝕜, E) g : Prop -/
+#guard_msgs in
+#check MDiff g
+-- TODO: fix and enable! #check MDiff g m
+
+-- From a manifold into a field.
+variable {h : M → 𝕜}
+
+/-- info: MDifferentiableWithinAt I 𝓘(𝕜, 𝕜) h s : M → Prop -/
+#guard_msgs in
+#check MDiffAt[s] h
+/-- info: MDifferentiableWithinAt I 𝓘(𝕜, 𝕜) h s m : Prop -/
+#guard_msgs in
+#check MDiffAt[s] h m
+/-- info: MDifferentiableAt I 𝓘(𝕜, 𝕜) h : M → Prop -/
+#guard_msgs in
+#check MDiffAt h
+/-- info: MDifferentiableAt I 𝓘(𝕜, 𝕜) h m : Prop -/
+#guard_msgs in
+#check MDiffAt h m
+/-- info: MDifferentiableOn I 𝓘(𝕜, 𝕜) h s : Prop -/
+#guard_msgs in
+#check MDiff[s] h
+-- TODO: fix and enable! #check MDiff[s] h m
+/-- info: MDifferentiable I 𝓘(𝕜, 𝕜) h : Prop -/
+#guard_msgs in
+#check MDiff h
+-- TODO: fix and enable! #check MDiff h m
+
+-- The following tests are more spotty, as most code paths are already covered above.
+-- Add further details as necessary.
+
+-- From a normed space into a manifold.
+variable {f : E → M'} {s : Set E} {x : E}
+/-- info: MDifferentiableWithinAt 𝓘(𝕜, E) I' f s : E → Prop -/
+#guard_msgs in
+#check MDiffAt[s] f
+/-- info: MDifferentiableAt 𝓘(𝕜, E) I' f x : Prop -/
+#guard_msgs in
+#check MDiffAt f x
+-- TODO: fix and enable! #check MDiff[s] f x
+/-- info: MDifferentiable 𝓘(𝕜, E) I' f : Prop -/
+#guard_msgs in
+#check MDiff f
+-- TODO: should this error? if not, fix and enable! #check MDiff f x
+-- same! #check MDifferentiable% f x
+
+-- Between normed spaces.
+variable {f : E → E'} {s : Set E} {x : E}
+
+/-- info: MDifferentiableAt 𝓘(𝕜, E) 𝓘(𝕜, E') f x : Prop -/
+#guard_msgs in
+#check MDiffAt f x
+/-- info: MDifferentiableAt 𝓘(𝕜, E) 𝓘(𝕜, E') f : E → Prop -/
+#guard_msgs in
+#check MDiffAt f
+-- should this error or not? #check MDiff[s] f x
+/-- info: MDifferentiableWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') f s : E → Prop -/
+#guard_msgs in
+#check MDiffAt[s] f
+/-- info: MDifferentiableOn 𝓘(𝕜, E) 𝓘(𝕜, E') f s : Prop -/
+#guard_msgs in
+#check MDiff[s] f
+
+
+-- Normed space to a field.
+variable {f : E → 𝕜} {s : Set E} {x : E}
+
+/-- info: MDifferentiableAt 𝓘(𝕜, E) 𝓘(𝕜, 𝕜) f x : Prop -/
+#guard_msgs in
+#check MDiffAt f x
+
+-- Field into a manifold.
+variable {f : 𝕜 → M'} {u : Set 𝕜} {a : 𝕜}
+/-- info: MDifferentiableAt 𝓘(𝕜, 𝕜) I' f a : Prop -/
+#guard_msgs in
+#check MDiffAt f a
+/-- info: MDifferentiableOn 𝓘(𝕜, 𝕜) I' f u : Prop -/
+#guard_msgs in
+#check MDiff[u] f
+
+-- Field into a normed space.
+variable {f : 𝕜 → E'} {u : Set 𝕜} {a : 𝕜}
+/-- info: MDifferentiableAt 𝓘(𝕜, 𝕜) 𝓘(𝕜, E') f a : Prop -/
+#guard_msgs in
+#check MDiffAt f a
+/-- info: MDifferentiableOn 𝓘(𝕜, 𝕜) 𝓘(𝕜, E') f u : Prop -/
+#guard_msgs in
+#check MDiff[u] f
+
+-- On a field.
+variable {f : 𝕜 → 𝕜} {u : Set 𝕜} {a : 𝕜}
+/-- info: MDifferentiableAt 𝓘(𝕜, 𝕜) 𝓘(𝕜, 𝕜) f a : Prop -/
+#guard_msgs in
+#check MDiffAt f a
+/-- info: MDifferentiableOn 𝓘(𝕜, 𝕜) 𝓘(𝕜, 𝕜) f u : Prop -/
+#guard_msgs in
+#check MDiff[u] f
+
+-- This elaborator can be combined with the total space elaborator.
+-- XXX: these tests might be incomplete; extend as needed!
+
+variable {σ : Π x : M, V x} {σ' : (x : E) → Trivial E E' x} {s : E → E'}
+variable (X : (m : M) → TangentSpace I m) [IsManifold I 1 M]
+
+/-- info: MDifferentiableAt I (I.prod 𝓘(𝕜, E)) fun m ↦ TotalSpace.mk' E m (X m) : M → Prop -/
+#guard_msgs in
+#check MDiffAt (T% X)
+
+/-- info: MDifferentiableAt I (I.prod 𝓘(𝕜, F)) fun x ↦ TotalSpace.mk' F x (σ x) : M → Prop -/
+#guard_msgs in
+#check MDiffAt (T% σ)
+
+/--
+info: MDifferentiableAt 𝓘(𝕜, E) (𝓘(𝕜, E).prod 𝓘(𝕜, E')) fun x ↦ TotalSpace.mk' E' x (σ' x) : E → Prop
+-/
+#guard_msgs in
+#check MDiffAt (T% σ')
+
+section
+
+variable [IsManifold I 2 M]
+
+variable {h : Bundle.TotalSpace F (TangentSpace I : M → Type _) → F} {h' : TangentBundle I M → F}
+
+-- Test the inference of a model with corners on a trivial bundle over the tangent space of a
+-- manifold. (This code path is not covered by the other tests, hence should be kept.)
+-- Stating smoothness this way does not make sense, but finding a model with corners should work.
+/--
+error: failed to synthesize
+  TopologicalSpace (TotalSpace F (TangentSpace I))
+
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+---
+trace: [Elab.DiffGeo.MDiff] Finding a model for: TotalSpace F (TangentSpace I)
+[Elab.DiffGeo.MDiff] ✅️ TotalSpace
+  [Elab.DiffGeo.MDiff] ❌️ From base info
+    [Elab.DiffGeo.MDiff] Failed with error:
+        No `baseInfo` provided
+  [Elab.DiffGeo.MDiff] ✅️ TangentSpace
+    [Elab.DiffGeo.MDiff] This is the total space of the tangent bundle of M
+    [Elab.DiffGeo.MDiff] Found model: I.prod I.tangent
+  [Elab.DiffGeo.MDiff] Found model: I.prod I.tangent
+[Elab.DiffGeo.MDiff] Finding a model for: F
+[Elab.DiffGeo.MDiff] ❌️ TotalSpace
+  [Elab.DiffGeo.MDiff] Failed with error:
+      F is not a `Bundle.TotalSpace`.
+[Elab.DiffGeo.MDiff] ✅️ NormedSpace
+  [Elab.DiffGeo.MDiff] Field is: 𝕜
+  [Elab.DiffGeo.MDiff] Found model: 𝓘(𝕜, F)
+-/
+#guard_msgs in
+set_option trace.Elab.DiffGeo true in
+#check MDiff h
+
+-- The reason this test fails is that Bundle.TotalSpace F (TangentSpace I : M → Type _) is not
+-- the way to state smoothness.
+/--
+error: failed to synthesize
+  TopologicalSpace (TotalSpace F (TangentSpace I))
+
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+-/
+#guard_msgs in
+#synth IsManifold I.tangent 1 (Bundle.TotalSpace F (TangentSpace I : M → Type _))
+
+-- The correct way is this.
+/-- info: TotalSpace.isManifold E (TangentSpace I) -/
+#guard_msgs in
+#synth IsManifold I.tangent 1 (TangentBundle I M)
+
+/-- info: MDifferentiable I.tangent 𝓘(𝕜, F) h' : Prop -/
+#guard_msgs in
+#check MDifferentiable I.tangent 𝓘(𝕜, F) h'
+
+/-- info: MDifferentiable (I.prod 𝓘(𝕜, E)) 𝓘(𝕜, F) h' : Prop -/
+#guard_msgs in
+#check MDifferentiable (I.prod (𝓘(𝕜, E))) 𝓘(𝕜, F) h'
+
+-- TODO: implement special handling for the tangent bundle
+/-- error: Could not find models with corners for TangentBundle I M -/
+#guard_msgs in
+#check MDiff h'
+
+end
+
+/-! Error messages in case of a forgotten `T%`. -/
+section
+
+/--
+error: Term X is a dependent function, of type (m : M) → TangentSpace I m
+Hint: you can use the `T%` elaborator to convert a dependent function to a non-dependent one
+-/
+#guard_msgs in
+#check MDiff X
+
+/--
+error: Term σ is a dependent function, of type (x : M) → V x
+Hint: you can use the `T%` elaborator to convert a dependent function to a non-dependent one
+-/
+#guard_msgs in
+#check MDiff σ
+
+/--
+error: Term σ' is a dependent function, of type (x : E) → Trivial E E' x
+Hint: you can use the `T%` elaborator to convert a dependent function to a non-dependent one
+-/
+#guard_msgs in
+#check MDiff σ'
+
+/--
+error: Term σ' is a dependent function, of type (x : E) → Trivial E E' x
+Hint: you can use the `T%` elaborator to convert a dependent function to a non-dependent one
+-/
+#guard_msgs in
+#check MDiff[s] σ'
+
+/--
+error: Term X is a dependent function, of type (m : M) → TangentSpace I m
+Hint: you can use the `T%` elaborator to convert a dependent function to a non-dependent one
+-/
+#guard_msgs in
+#check MDiffAt (X)
+
+/--
+error: Term σ is a dependent function, of type (x : M) → V x
+Hint: you can use the `T%` elaborator to convert a dependent function to a non-dependent one
+-/
+#guard_msgs in
+#check MDiffAt ((σ))
+
+/--
+error: Term σ' is a dependent function, of type (x : E) → Trivial E E' x
+Hint: you can use the `T%` elaborator to convert a dependent function to a non-dependent one
+-/
+#guard_msgs in
+#check MDiff[s] σ'
+
+/--
+error: Term σ' is a dependent function, of type (x : E) → Trivial E E' x
+Hint: you can use the `T%` elaborator to convert a dependent function to a non-dependent one
+-/
+#guard_msgs in
+#check MDiffAt σ'
+
+/--
+error: Term σ' is a dependent function, of type (x : E) → Trivial E E' x
+Hint: you can use the `T%` elaborator to convert a dependent function to a non-dependent one
+-/
+#guard_msgs in
+#check MDiffAt[s] σ'
+
+end
+
+end differentiability
+
+/-! Tests for the custom elaborators for `ContMDiff{WithinAt,At,On}` -/
+section smoothness
+
+-- Copy-pasted the tests for differentiability mutatis mutandis.
+-- Start with some basic tests: a simple function, both in applied and unapplied form.
+variable {EM' : Type*} [NormedAddCommGroup EM']
+  [NormedSpace 𝕜 EM'] {H' : Type*} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 EM' H')
+  {M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M']
+
+-- TODO: add tests for the error message when smoothness hypotheses are missing
+
+-- General case: a function between two manifolds.
+variable {f : M → M'} {s : Set M} {m : M}
+
+variable [IsManifold I 1 M] [IsManifold I' 1 M']
+
+-- TODO: can there be better error messages when forgetting the smoothness exponent?
+section error
+
+-- yields a parse error, "unexpected toekn '/--'; expected term"
+-- #check CMDiffAt[s] f
+
+/--
+error: Type mismatch
+  f
+has type
+  M → M'
+of sort `Type (max u_10 u_4)` but is expected to have type
+  WithTop ℕ∞
+of sort `Type`
+---
+error: Expected
+  m
+of type
+  M
+to be a function
+-/
+#guard_msgs in
+#check CMDiffAt[s] f m
+
+/--
+error: Type mismatch
+  f
+has type
+  M → M'
+of sort `Type (max u_10 u_4)` but is expected to have type
+  WithTop ℕ∞
+of sort `Type`
+---
+error: Expected
+  m
+of type
+  M
+to be a function
+-/
+#guard_msgs in
+#check CMDiffAt[s] f m
+
+-- yields a parse error, "unexpected toekn '/--'; expected term"
+-- #check CMDiffAt f
+
+end error
+
+/-- info: ContMDiffWithinAt I I' 1 f s : M → Prop -/
+#guard_msgs in
+#check CMDiffAt[s] 1 f
+
+/-- info: ContMDiffWithinAt I I' 1 f s m : Prop -/
+#guard_msgs in
+#check CMDiffAt[s] 1 f m
+
+/-- info: ContMDiffWithinAt I I' 1 f s m : Prop -/
+#guard_msgs in
+#check CMDiffAt[s] 1 f m
+
+/-- info: ContMDiffAt I I' 1 f : M → Prop -/
+#guard_msgs in
+#check CMDiffAt 1 f
+
+/-- info: ContMDiffAt I I' 2 f m : Prop -/
+#guard_msgs in
+#check CMDiffAt 2 f m
+
+/-- info: ContMDiffOn I I' 37 f s : Prop -/
+#guard_msgs in
+#check CMDiff[s] 37 f
+
+-- Testing an error message.
+section
+
+/--
+error: Function expected at
+  ContMDiffOn I I' 2 f s
+but this term has type
+  Prop
+
+Note: Expected a function because this term is being applied to the argument
+  m
+-/
+#guard_msgs in
+#check CMDiff[s] 2 f m
+
+variable {n : WithTop ℕ∞}
+/--
+error: Function expected at
+  ContMDiffOn I I' n f s
+but this term has type
+  Prop
+
+Note: Expected a function because this term is being applied to the argument
+  m
+-/
+#guard_msgs in
+#check ContMDiffOn I I' n f s m
+
+/-- info: MDifferentiable I I' f : Prop -/
+#guard_msgs in
+#check MDiff f
+
+/--
+error: Function expected at
+  ContMDiff I I' n f
+but this term has type
+  Prop
+
+Note: Expected a function because this term is being applied to the argument
+  m
+-/
+#guard_msgs in
+#check CMDiff n f m
+
+end
+
+/-! Tests for coercions from `ℕ` or `ℕ∞` to `WithTop ℕ∞` -/
+section coercions
+
+variable {k : ℕ} {k' : ℕ∞}
+
+/-- info: ContMDiffWithinAt I I' 0 f s : M → Prop -/
+#guard_msgs in
+#check CMDiffAt[s] 0 f
+
+/-- info: ContMDiffWithinAt I I' 1 f s : M → Prop -/
+#guard_msgs in
+#check CMDiffAt[s] 1 f
+
+/-- info: ContMDiffWithinAt I I' 37 f s : M → Prop -/
+#guard_msgs in
+#check CMDiffAt[s] 37 f
+
+/-- info: ContMDiffWithinAt I I' (↑k) f s : M → Prop -/
+#guard_msgs in
+#check CMDiffAt[s] k f
+
+/-- info: ContMDiffWithinAt I I' (↑k') f s m : Prop -/
+#guard_msgs in
+#check CMDiffAt[s] k' f m
+
+/-- info: ContMDiffWithinAt I I' n f s m : Prop -/
+#guard_msgs in
+#check CMDiffAt[s] n f m
+
+/-- info: ContMDiffAt I I' (↑k) f : M → Prop -/
+#guard_msgs in
+#check CMDiffAt k f
+
+/-- info: ContMDiffAt I I' (↑k') f m : Prop -/
+#guard_msgs in
+#check CMDiffAt k' f m
+
+/-- info: ContMDiffOn I I' (↑k) f s : Prop -/
+#guard_msgs in
+#check CMDiff[s] k f
+
+/--
+error: Function expected at
+  ContMDiffOn I I' (↑k') f s
+but this term has type
+  Prop
+
+Note: Expected a function because this term is being applied to the argument
+  m
+-/
+#guard_msgs in
+#check CMDiff[s] k' f m
+
+/-- info: ContMDiff I I' (↑k) f : Prop -/
+#guard_msgs in
+#check CMDiff k f
+
+/--
+error: Function expected at
+  ContMDiff I I' (↑k') f
+but this term has type
+  Prop
+
+Note: Expected a function because this term is being applied to the argument
+  m
+-/
+#guard_msgs in
+#check CMDiff k' f m
+
+end coercions
+
+/-! Error messages for a missing `T%` elaborator. -/
+section dependent
+
+variable {σ : Π x : M, V x} {σ' : (x : E) → Trivial E E' x} {s : E → E'}
+variable (X : (m : M) → TangentSpace I m) [IsManifold I 1 M]
+
+/--
+error: Term X is a dependent function, of type (m : M) → TangentSpace I m
+Hint: you can use the `T%` elaborator to convert a dependent function to a non-dependent one
+-/
+#guard_msgs in
+#check CMDiff 0 X
+
+/--
+error: Term σ is a dependent function, of type (x : M) → V x
+Hint: you can use the `T%` elaborator to convert a dependent function to a non-dependent one
+-/
+#guard_msgs in
+#check CMDiff 0 σ
+
+/--
+error: Term σ' is a dependent function, of type (x : E) → Trivial E E' x
+Hint: you can use the `T%` elaborator to convert a dependent function to a non-dependent one
+-/
+#guard_msgs in
+#check CMDiff 0 σ'
+
+/--
+error: Term σ' is a dependent function, of type (x : E) → Trivial E E' x
+Hint: you can use the `T%` elaborator to convert a dependent function to a non-dependent one
+-/
+#guard_msgs in
+#check CMDiff[s] 0 σ'
+
+/--
+error: Term X is a dependent function, of type (m : M) → TangentSpace I m
+Hint: you can use the `T%` elaborator to convert a dependent function to a non-dependent one
+-/
+#guard_msgs in
+#check CMDiffAt 0 (X)
+
+/--
+error: Term σ is a dependent function, of type (x : M) → V x
+Hint: you can use the `T%` elaborator to convert a dependent function to a non-dependent one
+-/
+#guard_msgs in
+#check CMDiffAt 0 ((σ))
+
+/--
+error: Term σ' is a dependent function, of type (x : E) → Trivial E E' x
+Hint: you can use the `T%` elaborator to convert a dependent function to a non-dependent one
+-/
+#guard_msgs in
+#check CMDiff[s] 0 σ'
+
+/--
+error: Term σ' is a dependent function, of type (x : E) → Trivial E E' x
+Hint: you can use the `T%` elaborator to convert a dependent function to a non-dependent one
+-/
+#guard_msgs in
+#check CMDiffAt 0 σ'
+
+/--
+error: Term σ' is a dependent function, of type (x : E) → Trivial E E' x
+Hint: you can use the `T%` elaborator to convert a dependent function to a non-dependent one
+-/
+#guard_msgs in
+#check CMDiffAt[s] 0 σ'
+
+end dependent
+
+-- Function from a manifold into a normed space.
+variable {g : M → E}
+
+/-- info: ContMDiffWithinAt I 𝓘(𝕜, E) 1 g s : M → Prop -/
+#guard_msgs in
+#check CMDiffAt[s] 1 g
+/-- info: ContMDiffWithinAt I 𝓘(𝕜, E) 0 g s m : Prop -/
+#guard_msgs in
+#check CMDiffAt[s] 0 g m
+/-- info: ContMDiffAt I 𝓘(𝕜, E) 1 g : M → Prop -/
+#guard_msgs in
+#check CMDiffAt 1 g
+/-- info: ContMDiffAt I 𝓘(𝕜, E) 1 g m : Prop -/
+#guard_msgs in
+#check CMDiffAt 1 g m
+/-- info: ContMDiffOn I 𝓘(𝕜, E) n g s : Prop -/
+#guard_msgs in
+#check CMDiff[s] n g
+-- TODO: fix and enable! #check CMDiff[s] n g m
+/-- info: ContMDiff I 𝓘(𝕜, E) n g : Prop -/
+#guard_msgs in
+#check CMDiff n g
+-- TODO: fix and enable! #check CMDiff n g m
+
+-- From a manifold into a field.
+variable {h : M → 𝕜}
+
+/-- info: ContMDiffWithinAt I 𝓘(𝕜, 𝕜) 0 h s : M → Prop -/
+#guard_msgs in
+#check CMDiffAt[s] 0 h
+/-- info: ContMDiffWithinAt I 𝓘(𝕜, 𝕜) 1 h s m : Prop -/
+#guard_msgs in
+#check CMDiffAt[s] 1 h m
+/-- info: ContMDiffAt I 𝓘(𝕜, 𝕜) 2 h : M → Prop -/
+#guard_msgs in
+#check CMDiffAt 2 h
+/-- info: ContMDiffAt I 𝓘(𝕜, 𝕜) n h m : Prop -/
+#guard_msgs in
+#check CMDiffAt n h m
+/-- info: ContMDiffOn I 𝓘(𝕜, 𝕜) n h s : Prop -/
+#guard_msgs in
+#check CMDiff[s] n h
+-- TODO: fix and enable! #check CMDiff[s] n h m
+/-- info: ContMDiff I 𝓘(𝕜, 𝕜) 37 h : Prop -/
+#guard_msgs in
+#check CMDiff 37 h
+-- TODO: fix and enable! #check CMDiff 0 h m
+
+-- The following tests are more spotty, as most code paths are already covered above.
+-- Add further details as necessary.
+-- This list mirrors some of the tests for `MDifferentiable{WithinAt,At,On}`, but not all.
+
+-- From a normed space into a manifold.
+variable {f : E → M'} {s : Set E} {x : E}
+/-- info: ContMDiffWithinAt 𝓘(𝕜, E) I' 2 f s : E → Prop -/
+#guard_msgs in
+#check CMDiffAt[s] 2 f
+/-- info: ContMDiffAt 𝓘(𝕜, E) I' 3 f x : Prop -/
+#guard_msgs in
+#check CMDiffAt 3 f x
+-- TODO: fix and enable! #check CMDiff[s] 1 f x
+/-- info: ContMDiff 𝓘(𝕜, E) I' 1 f : Prop -/
+#guard_msgs in
+#check CMDiff 1 f
+-- TODO: should this error? if not, fix and enable! #check CMDiff 1 f x
+-- same! #check MDifferentiable% f x
+
+-- Between normed spaces.
+variable {f : E → E'} {s : Set E} {x : E}
+
+/-- info: ContMDiffAt 𝓘(𝕜, E) 𝓘(𝕜, E') 2 f x : Prop -/
+#guard_msgs in
+#check CMDiffAt 2 f x
+/-- info: ContMDiffAt 𝓘(𝕜, E) 𝓘(𝕜, E') 2 f : E → Prop -/
+#guard_msgs in
+#check CMDiffAt 2 f
+-- should this error or not? #check CMDiff[s] 2 f x
+/-- info: ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') 2 f s : E → Prop -/
+#guard_msgs in
+#check CMDiffAt[s] 2 f
+/-- info: ContMDiffOn 𝓘(𝕜, E) 𝓘(𝕜, E') 2 f s : Prop -/
+#guard_msgs in
+#check CMDiff[s] 2 f
+
+end smoothness
+
+/-! Tests for the custom elaborators for `mfderiv` and `mfderivWithin` -/
+section mfderiv
+
+variable {EM' : Type*} [NormedAddCommGroup EM']
+  [NormedSpace 𝕜 EM'] {H' : Type*} [TopologicalSpace H'] (I' : ModelWithCorners 𝕜 EM' H')
+  {M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M']
+
+variable {f : M → M'} {s : Set M} {m : M}
+
+/-- info: mfderiv I I' f : (x : M) → TangentSpace I x →L[𝕜] TangentSpace I' (f x) -/
+#guard_msgs in
+#check mfderiv% f
+
+/-- info: mfderiv I I' f m : TangentSpace I m →L[𝕜] TangentSpace I' (f m) -/
+#guard_msgs in
+#check mfderiv% f m
+
+/-- info: mfderivWithin I I' f s : (x : M) → TangentSpace I x →L[𝕜] TangentSpace I' (f x) -/
+#guard_msgs in
+#check mfderiv[s] f
+
+/-- info: mfderivWithin I I' f s m : TangentSpace I m →L[𝕜] TangentSpace I' (f m) -/
+#guard_msgs in
+#check mfderiv[s] f m
+
+variable {f : E → EM'} {s : Set E} {m : E}
+
+/--
+info: mfderiv 𝓘(𝕜, E) 𝓘(𝕜, EM') f : (x : E) → TangentSpace 𝓘(𝕜, E) x →L[𝕜] TangentSpace 𝓘(𝕜, EM') (f x)
+-/
+#guard_msgs in
+#check mfderiv% f
+
+/--
+info: mfderiv 𝓘(𝕜, E) 𝓘(𝕜, EM') f m : TangentSpace 𝓘(𝕜, E) m →L[𝕜] TangentSpace 𝓘(𝕜, EM') (f m)
+-/
+#guard_msgs in
+#check mfderiv% f m
+
+/--
+info: mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, EM') f s : (x : E) → TangentSpace 𝓘(𝕜, E) x →L[𝕜] TangentSpace 𝓘(𝕜, EM') (f x)
+-/
+#guard_msgs in
+#check mfderiv[s] f
+
+/--
+info: mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, EM') f s m : TangentSpace 𝓘(𝕜, E) m →L[𝕜] TangentSpace 𝓘(𝕜, EM') (f m)
+-/
+#guard_msgs in
+#check mfderiv[s] f m
+
+variable {σ : Π x : M, V x} {σ' : (x : E) → Trivial E E' x} {s : E → E'}
+variable (X : (m : M) → TangentSpace I m) [IsManifold I 1 M] {x : M}
+
+/--
+info: mfderiv I (I.prod 𝓘(𝕜, E)) (fun m ↦ TotalSpace.mk' E m (X m))
+  x : TangentSpace I x →L[𝕜] TangentSpace (I.prod 𝓘(𝕜, E)) (TotalSpace.mk' E x (X x))
+-/
+#guard_msgs in
+#check mfderiv% (T% X) x
+
+/--
+info: mfderiv I (I.prod 𝓘(𝕜, F)) (fun x ↦ TotalSpace.mk' F x (σ x))
+  x : TangentSpace I x →L[𝕜] TangentSpace (I.prod 𝓘(𝕜, F)) (TotalSpace.mk' F x (σ x))
+-/
+#guard_msgs in
+#check mfderiv% (T% σ) x
+
+variable {t : Set E} {p : E}
+
+/--
+info: mfderivWithin 𝓘(𝕜, E) (𝓘(𝕜, E).prod 𝓘(𝕜, E')) (fun x ↦ TotalSpace.mk' E' x (σ' x)) t
+  p : TangentSpace 𝓘(𝕜, E) p →L[𝕜] TangentSpace (𝓘(𝕜, E).prod 𝓘(𝕜, E')) (TotalSpace.mk' E' p (σ' p))
+-/
+#guard_msgs in
+#check mfderiv[t] (T% σ') p
+
+/--
+info: mfderivWithin 𝓘(𝕜, E) (𝓘(𝕜, E).prod 𝓘(𝕜, E')) (fun x ↦ TotalSpace.mk' E' x (σ' x))
+  t : (x : E) → TangentSpace 𝓘(𝕜, E) x →L[𝕜] TangentSpace (𝓘(𝕜, E).prod 𝓘(𝕜, E')) (TotalSpace.mk' E' x (σ' x))
+-/
+#guard_msgs in
+#check mfderiv[t] (T% σ')
+
+section errors
+
+-- Test an error message, about mismatched types.
+variable {s' : Set M} {m' : M}
+
+/--
+error: Application type mismatch: The argument
+  m'
+has type
+  M
+of sort `Type u_4` but is expected to have type
+  E
+of sort `Type u_2` in the application
+  mfderiv 𝓘(𝕜, E) 𝓘(𝕜, EM') f m'
+---
+info: mfderiv 𝓘(𝕜, E) 𝓘(𝕜, EM') f sorry : TangentSpace 𝓘(𝕜, E) sorry →L[𝕜] TangentSpace 𝓘(𝕜, EM') (f sorry)
+-/
+#guard_msgs in
+#check mfderiv% f m'
+
+-- Error messages: argument s has mismatched type.
+/--
+error: The domain E of f is not definitionally equal to the carrier type of the set s' : Set M
+-/
+#guard_msgs in
+#check mfderiv[s'] f
+
+/--
+error: The domain E of f is not definitionally equal to the carrier type of the set s' : Set M
+-/
+#guard_msgs in
+#check mfderiv[s'] f m
+
+end errors
+
+section
+
+/--
+error: Term X is a dependent function, of type (m : M) → TangentSpace I m
+Hint: you can use the `T%` elaborator to convert a dependent function to a non-dependent one
+-/
+#guard_msgs in
+#check mfderiv% X x
+
+/--
+error: Term σ is a dependent function, of type (x : M) → V x
+Hint: you can use the `T%` elaborator to convert a dependent function to a non-dependent one
+-/
+#guard_msgs in
+#check mfderiv% σ x
+
+variable {t : Set E} {p : E}
+
+/--
+error: Term σ' is a dependent function, of type (x : E) → Trivial E E' x
+Hint: you can use the `T%` elaborator to convert a dependent function to a non-dependent one
+-/
+#guard_msgs in
+#check mfderiv[t] σ' p
+
+/--
+error: Term σ' is a dependent function, of type (x : E) → Trivial E E' x
+Hint: you can use the `T%` elaborator to convert a dependent function to a non-dependent one
+-/
+#guard_msgs in
+#check mfderiv[t] σ'
+
+end
+
+end mfderiv
+
+section trace
+
+/- Test that basic tracing works. -/
+
+set_option trace.Elab.DiffGeo true
+
+variable {f : Unit → Unit}
+
+/--
+error: Could not find models with corners for Unit
+---
+trace: [Elab.DiffGeo.MDiff] Finding a model for: Unit
+[Elab.DiffGeo.MDiff] ❌️ TotalSpace
+  [Elab.DiffGeo.MDiff] Failed with error:
+      Unit is not a `Bundle.TotalSpace`.
+[Elab.DiffGeo.MDiff] ❌️ NormedSpace
+  [Elab.DiffGeo.MDiff] Failed with error:
+      Couldn't find a `NormedSpace` structure on Unit among local instances.
+[Elab.DiffGeo.MDiff] ❌️ ChartedSpace
+  [Elab.DiffGeo.MDiff] Failed with error:
+      Couldn't find a `ChartedSpace` structure on Unit among local instances.
+[Elab.DiffGeo.MDiff] ❌️ NormedField
+  [Elab.DiffGeo.MDiff] Failed with error:
+      failed to synthesize
+        NontriviallyNormedField Unit
+      ⏎
+      Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+-/
+#guard_msgs in
+#check mfderiv% f
+
+/--
+info: fun a ↦ TotalSpace.mk' Unit a (f a) : Unit → TotalSpace Unit (Trivial Unit Unit)
+---
+trace: [Elab.DiffGeo.TotalSpaceMk] Section of a trivial bundle as a non-dependent function
+-/
+#guard_msgs in
+#check T% f
+
+end trace
diff --git a/scripts/noshake.json b/scripts/noshake.json
index eb97867df63397..5953a416fa7748 100644
--- a/scripts/noshake.json
+++ b/scripts/noshake.json
@@ -49,6 +49,7 @@
   "Mathlib.Data.Set.Notation",
   "Mathlib.Data.Sym.Sym2.Init",
   "Mathlib.Data.Vector.Basic",
+  "Mathlib.Geometry.Manifold.Notation",
   "Mathlib.Geometry.Manifold.Instances.Real",
   "Mathlib.Init",
   "Mathlib.LinearAlgebra.AffineSpace.Basic",
@@ -253,9 +254,9 @@
    "Mathlib.Data.PNat.Defs"],
   "Mathlib.Tactic.Order.CollectFacts":
   ["Mathlib.Order.BoundedOrder.Basic", "Mathlib.Order.Lattice"],
+  "Mathlib.Tactic.NormNum.Parity": ["Mathlib.Algebra.Ring.Int.Parity"],
   "Mathlib.Tactic.NormNum.ModEq":
   ["Mathlib.Data.Int.ModEq", "Mathlib.Tactic.NormNum.DivMod"],
-  "Mathlib.Tactic.NormNum.Parity": ["Mathlib.Algebra.Ring.Int.Parity"],
   "Mathlib.Tactic.NormNum.Ineq":
   ["Mathlib.Algebra.Order.Field.Defs", "Mathlib.Algebra.Order.Monoid.WithTop"],
   "Mathlib.Tactic.NormNum.BigOperators":
@@ -348,6 +349,7 @@
   "Mathlib.Tactic.Algebraize": ["Mathlib.Algebra.Algebra.Tower"],
   "Mathlib.Std.Data.HashMap": ["Std.Data.HashMap.AdditionalOperations"],
   "Mathlib.RingTheory.SimpleModule.Basic": ["Mathlib.Data.Matrix.Mul"],
+  "Mathlib.RingTheory.PowerSeries.Restricted": ["Mathlib.Tactic.Bound"],
   "Mathlib.RingTheory.PowerSeries.Evaluation":
   ["Mathlib.RingTheory.PowerSeries.PiTopology"],
   "Mathlib.RingTheory.PowerSeries.Basic":
@@ -362,7 +364,6 @@
   ["Mathlib.LinearAlgebra.FreeModule.IdealQuotient"],
   "Mathlib.RingTheory.Finiteness.Defs": ["Mathlib.Data.Finsupp.Defs"],
   "Mathlib.RingTheory.Adjoin.Basic": ["Mathlib.LinearAlgebra.Finsupp.SumProd"],
-  "Mathlib.RingTheory.PowerSeries.Restricted": ["Mathlib.Tactic.Bound"],
   "Mathlib.RepresentationTheory.FdRep":
   ["Mathlib.CategoryTheory.Monoidal.Rigid.Braided"],
   "Mathlib.RepresentationTheory.FDRep":
@@ -419,6 +420,8 @@
   "Mathlib.Geometry.Manifold.PoincareConjecture":
   ["Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected",
    "Mathlib.Util.Superscript"],
+  "Mathlib.Geometry.Manifold.Notation":
+  ["Mathlib.Geometry.Manifold.ContMDiff.Defs", "Mathlib.Geometry.Manifold.MFDeriv.Defs"],
   "Mathlib.Deprecated.NatLemmas": ["Batteries.Data.Nat.Lemmas", "Batteries.WF"],
   "Mathlib.Deprecated.MinMax": ["Mathlib.Order.MinMax"],
   "Mathlib.Deprecated.LazyList": ["Mathlib.Lean.Thunk"],