diff --git a/Mathlib.lean b/Mathlib.lean
index b164589ad62537..7dccd338c376ea 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3936,7 +3936,6 @@ import Mathlib.Geometry.Manifold.Riemannian.PathELength
 import Mathlib.Geometry.Manifold.Sheaf.Basic
 import Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
 import Mathlib.Geometry.Manifold.Sheaf.Smooth
-import Mathlib.Geometry.Manifold.Traces
 import Mathlib.Geometry.Manifold.VectorBundle.Basic
 import Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear
 import Mathlib.Geometry.Manifold.VectorBundle.Hom
diff --git a/Mathlib/Geometry/Manifold/Elaborators.lean b/Mathlib/Geometry/Manifold/Elaborators.lean
index b59c27846e3705..e37cf621b90d9d 100644
--- a/Mathlib/Geometry/Manifold/Elaborators.lean
+++ b/Mathlib/Geometry/Manifold/Elaborators.lean
@@ -5,53 +5,65 @@ Authors: Patrick Massot, Michael Rothgang
 -/
 import Mathlib.Geometry.Manifold.ContMDiff.Defs
 import Mathlib.Geometry.Manifold.MFDeriv.Defs
-import Mathlib.Geometry.Manifold.Traces
 
 /-!
 # Elaborators for differential geometry
 
-This file defines custom elaborators for differential geometry, to allow for more compact notation.
-There are two classes of elaborators. The first provides more compact notation for differentiability
-and continuous differentiability on manifolds, including inference of the model with corners.
-All these elaborators are scoped to the `Manifold` namespace. They allow writing
-- `MDiff f` for `MDifferentiable I J f`
-- `MDiffAt f x` for `MDifferentiableAt I J f x`
-- `MDiff[u] f` for `MDifferentiableOn I J f u`
-- `MDiffAt[u] f x` for `MDifferentiableWithinAt I J f u x`
-- `CMDiff n f` for `ContMDiff I J n f`
-- `CMDiffAt n f x` for `ContMDiffAt I J n f x`
-- `CMDiff[u] n f` for `ContMDiffOn I J n f u`
-- `CMDiffAt[u] n f x` for `ContMDiffWithinAt I J n f u x`,
-- `mfderiv[u] f x` for `mfderivWithin I J f u x`,
-- `mfderiv% f x` for `mfderiv I J f x`.
+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 syntactic, hence
-hopefully fast enough to always run.
+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).
 
-Secondly, this file adds an elaborator to ease working with sections in a fibre bundle,
-converting a section `s : Π x : M, Π V x` to a non-dependent function into the total space of the
+## `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} {σ' : (x : E) → Trivial E E' x} {s : E → E'}
 
--- outputs `fun x ↦ TotalSpace.mk' F x (σ x) : M → TotalSpace F V`
-#check T% σ
+variable {σ : Π x : M, V x} in
+#check T% σ -- `(fun x ↦ TotalSpace.mk' F x (σ x)) : M → TotalSpace F V`
 
--- outputs `fun x ↦ TotalSpace.mk' E' x (σ' x) : E → TotalSpace E' (Trivial E E')`
 -- Note how the name of the bound variable `x` is preserved.
-#check T% σ'
+variable {σ : (x : E) → Trivial E E' x} in
+#check T% σ -- `(fun x ↦ TotalSpace.mk' E' x (σ x)) : E → TotalSpace E' (Trivial E E')`
 
--- outputs `fun a ↦ TotalSpace.mk' E' a (s a) : E → TotalSpace E' (Trivial E E')`
-#check T% s
+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
@@ -61,11 +73,10 @@ 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)
+  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 `PartialHomeomorph`s and `PartialEquiv`s
-
 - better error messages (as needed)
 - further testing and fixing of edge cases
 - add tests for all of the above
@@ -77,66 +88,132 @@ open scoped Bundle Manifold ContDiff
 
 open Lean Meta Elab Tactic
 open Mathlib.Tactic
-
-namespace Manifold
-
-/-- Elaborator for sections in a fibre bundle: converts a section as a dependent function
-to a non-dependent function into the total space. This handles the cases of
+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 operates purely syntactically, by analysing the local contexts for suitable
-hypothesis for the above cases. Therefore, it is (hopefully) fast enough to always run.
+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.
-elab:max "T% " t:term:arg : term => do
+-- TODO: factor out `MetaM` component for reuse
+scoped elab:max "T% " t:term:arg : term => do
   let e ← Term.elabTerm t none
-  let etype ← inferType e >>= instantiateMVars
+  let etype ← whnf <|← instantiateMVars <|← inferType e
   match etype with
-  | .forallE x base (mkApp3 (.const ``Bundle.Trivial _) E E' _) _ =>
-    trace[TotalSpaceMk] "Section of a trivial bundle"
-    if ← withReducible (isDefEq E base) then
-      return ← withLocalDecl x BinderInfo.default base fun x ↦ do
-        let body ← mkAppM ``Bundle.TotalSpace.mk' #[E', x, .app e x]
+  | .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
-  | .forallE x base (mkApp12 (.const ``TangentSpace _) _k _ E _ _ _H _ _I _M _ _ _x) _ =>
-    trace[TotalSpaceMk] "Vector field"
-    return ← withLocalDecl x BinderInfo.default base fun x ↦ do
-      let body ← mkAppM ``Bundle.TotalSpace.mk' #[E, x, .app e x]
+      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
-  | .forallE x base (.app V _) _ =>
-    trace[TotalSpaceMk] "Section of a bundle as a dependent function"
-    for decl in ← getLocalHyps do
-      let decltype ← inferType decl >>= instantiateMVars
-      match decltype with
-      | mkApp7 (.const `FiberBundle _) _ F _ _ E _ _ =>
-        if ← withReducible (isDefEq E V) then
-          return ← withLocalDecl x BinderInfo.default base fun x ↦ do
-            let body ← mkAppM ``Bundle.TotalSpace.mk' #[F, x, .app e x]
-            mkLambdaFVars #[x] body
-      | _ => pure ()
-  | .forallE x src tgt _ =>
-    trace[TotalSpaceMk] "Section of a trivial bundle as a non-dependent function"
-    let us ← src.getUniverse
-    let ut ← tgt.getUniverse
-    -- 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`!
-    -- xxx: is this check fine or overzealous?
-    if Lean.Expr.hasLooseBVars tgt then
-      throwError m!"Term {tgt} has loose bound variables¬
-      Hint: applying the 'T%' elaborator twice makes no sense."
-    let trivBundle := mkAppN (.const `Bundle.Trivial [us, ut]) #[src, tgt]
-    return ← withLocalDecl x BinderInfo.default src fun x ↦ do
-      let body := mkAppN (.const ``Bundle.TotalSpace.mk' [us, ut, ut])
-        #[src, trivBundle, tgt, x, .app e x]
-      mkLambdaFVars #[x] body
-  | _ => pure ()
-  return e
+    | _ => 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 expected type. This supports the following cases:
+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
@@ -154,254 +231,241 @@ corners.
 
 This implementation is not maximally robust yet.
 -/
--- FIXME: better failure when trying to find a `NormedField` instance
-def find_model (e : Expr) (baseInfo : Option (Expr × Expr) := none) : TermElabM Expr := do
-    trace[MDiffElab] m!"Searching a model for: {e}"
-    if let mkApp3 (.const ``Bundle.TotalSpace _) _ F V := e then
-      if let mkApp12 (.const ``TangentSpace _) _k _ _E _ _ _H _ I M _ _ _x := V then
-        trace[MDiffElab] m!"This is the total space of the tangent bundle of {M}"
-        let srcIT : Term ← PrettyPrinter.delab I
-        let resTerm : Term ← ``(ModelWithCorners.prod $srcIT ModelWithCorners.tangent $srcIT)
-        let res ← Term.elabTerm resTerm none
-        trace[MDiffElab] m!"Found model: {res}"
-        return res
-
-      trace[MDiffElab] m!"This is a total space with fiber {F}"
-      if let some (_src, srcI) := baseInfo then
-        let mut K : Expr := default
-        let mut normedSpaceInst : Expr := default
-        let mut Kok : Bool := false
-        for decl in ← getLocalHyps do
-          let decltype ← inferType decl >>= instantiateMVars
-          match decltype with
-          | mkApp4 (.const ``NormedSpace _) K' E _ _ =>
-            if E == F then
-              K := K'
-              trace[MDiffElab] m!"{F} is a normed field over {K}"
-              normedSpaceInst := decl
-              Kok := true
-          | _ => pure ()
-          if Kok then break
-        unless Kok do throwError
-          m!"Couldn’t find a normed space structure on {F} in local context"
-        let kT : Term ← PrettyPrinter.delab K
-        let srcIT : Term ← PrettyPrinter.delab srcI
-        let FT : Term ← PrettyPrinter.delab F
-        let iTerm : Term ← ``(ModelWithCorners.prod $srcIT 𝓘($kT, $FT))
-        let I ← Term.elabTerm iTerm none
-        trace[MDiffElab] m!"Found model: {I}"
-        return I
-      else
-        throwError "Having a TotalSpace as source is not yet supported"
-    let mut H : Expr := default
-    let mut Hok : Bool := false
-    let mut K : Expr := default
-    let mut normedSpaceInst : Expr := default
-    let mut Kok : Bool := false
-    for decl in ← getLocalHyps do
-      let decltype ← inferType decl >>= instantiateMVars
-      match decltype with
-      | mkApp4 (.const ``ChartedSpace _) H' _ M _ =>
-        if M == e then
-          H := H'
-          trace[MDiffElab] m!"H is: {H}"
-          Hok := true
-      | mkApp4 (.const ``NormedSpace _) K' E _ _ =>
-        if E == e then
-          K := K'
-          trace[MDiffElab] m!"Field is: {K}"
-          normedSpaceInst := decl
-          Kok := true
-      | _ => pure ()
-      if Hok || Kok then break
-    if Kok then
-      let eT : Term ← PrettyPrinter.delab e
-      let eK : Term ← PrettyPrinter.delab K
-      let iTerm : Term ← ``(𝓘($eK, $eT))
-      let I ← Term.elabTerm iTerm none
-      trace[MDiffElab] m!"Found model: {I}"
-      return I
-      -- let uK ← K.getUniverse
-      -- let normedFieldK ← synthInstance (.app (.const ``NontriviallyNormedField [uK]) K)
-      -- trace[MDiffElab] m!"NontriviallyNormedField instance is: {normedFieldK}"
-      -- let ue ← e.getUniverse
-      -- let normedGroupE ← synthInstance (.app (.const ``NormedAddCommGroup  [ue]) e)
-      -- trace[MDiffElab] m!"NormedAddCommGroup  instance is: {normedGroupE}"
-      -- return mkAppN (.const `modelWithCornersSelf [uK, ue])
-      --   #[K, normedFieldK, e, normedGroupE, normedSpaceInst]
-    else if Hok then
-      for decl in ← getLocalHyps do
-        let decltype ← inferType decl >>= instantiateMVars
-        match decltype with
-        | mkApp7 (.const ``ModelWithCorners  _) _ _ _ _ _ H' _ =>
-          if H' == H then
-            trace[MDiffElab] m!"Found model: {decl}"
-            return decl
-        | _ => pure ()
+-- 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. -/
+  fromTotalSpace : TermElabM Expr := do
+    match_expr e with
+    | Bundle.TotalSpace _ F V => do
+      if let some m ← tryStrategy m!"TangentSpace" (fromTotalSpace.tangentSpace V) then return m
+      if let some m ← tryStrategy m!"From base info" (fromTotalSpace.fromBaseInfo F) then return m
+      throwError "Having a TotalSpace as source is not yet supported"
+    | _ => throwError "{e} is not a `Bundle.TotalSpace`."
+  fromTotalSpace.tangentSpace (V : Expr) : TermElabM Expr := do
+    match_expr V with
+    | TangentSpace _k _ _E _ _ _H _ I M _ _ _x => 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`"
+  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
-      trace[MDiffElab] m!"Hoping {e} is a normed field"
-      let eT : Term ← PrettyPrinter.delab e
-      let iTerm : Term ← `(𝓘($eT, $eT))
-      let I ← Term.elabTerm iTerm none
-      trace[MDiffElab] m!"Found model: {I}"
-      return I
-    throwError "Couldn’t find models with corners"
-
-/-- If `etype` 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.
-
-`ef` is the term having type `etype`: this is used only for better diagnostics.
-If `estype` is `some`, we verify that `src` and `estype` are def-eq. -/
-def _find_models (etype eterm : Expr) (estype : Option Expr) :
-    TermElabM (Option (Expr × Expr)) := do
+      throwError "No `baseInfo` provided"
+  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]
+  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
+  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 defeq. -/
+def findModels (e : Expr) (es : Option Expr) : TermElabM (Expr × Expr) := do
+  let etype ← whnf <|← instantiateMVars <|← inferType e
   match etype with
   | .forallE _ src tgt _ =>
-    let srcI ← find_model src
-    if Lean.Expr.hasLooseBVars tgt then
-      throwError m!"Term {eterm} 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"
-    if let some es := estype then
-      if !(← isDefEq es (← mkAppM ``Set #[src])) then
-        throwError m!"The domain {src} of {eterm} is not definitionally equal to the carrier \
-        of the type '{es}' of the set 's' passed in"
-    let tgtI ← find_model tgt (src, srcI)
-    return some (srcI, tgtI)
-  | _ => return none
+    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
+      if !(← pureIsDefEq 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. -/
-elab:max "MDiffAt[" s:term:arg "]" ppSpace f:term:arg : term => do
+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 etype ← inferType ef >>= instantiateMVars
-  let estype ← inferType es >>= instantiateMVars
-  match ← _find_models etype ef estype with
-  | some (srcI, tgtI) => return ← mkAppM ``MDifferentiableWithinAt #[srcI, tgtI, ef, es]
-  | none => throwError m!"Term {ef} is not a function."
+  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. -/
-elab:max "MDiffAt" ppSpace t:term:arg : term => do
-  let e ← Term.elabTerm t none
-  let etype ← inferType e >>= instantiateMVars
-  match ← _find_models etype e none with
-  | some (srcI, tgtI) => return ← mkAppM ``MDifferentiableAt #[srcI, tgtI, e]
-  | none => throwError m!"Term {e} is not a function."
-
--- This implement is more robust (in theory), but currently fails tests.
--- TODO: investigate why, fix this and replace `MDiffAt` by this one!
-/-- `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. -/
-elab:max "MDiffAt2" ppSpace t:term:arg : term => do
+scoped elab:max "MDiffAt" ppSpace t:term:arg : term => do
   let e ← Term.elabTerm t none
-  let etype ← inferType e >>= instantiateMVars
-  forallBoundedTelescope etype (some 1) fun src tgt ↦ do
-    if let some src := src[0]? then
-      let srcI ← find_model src
-      if Lean.Expr.occurs src tgt then
-        throwError m!"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 ← find_model tgt (src, srcI)
-      return ← mkAppM ``MDifferentiableAt #[srcI, tgtI, e]
-    else
-      throwError m!"Term {e} is not a function."
+  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. -/
-elab:max "MDiff[" s:term:arg "]" ppSpace t:term:arg : term => do
+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 estype ← inferType es >>= instantiateMVars
-  let etype ← inferType et >>= instantiateMVars
-  match ← _find_models etype et estype with
-  | some (srcI, tgtI) => return ← mkAppM ``MDifferentiableOn #[srcI, tgtI, et, es]
-  | none => throwError m!"Term {et} is not a function."
+  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. -/
-elab:max "MDiff" ppSpace t:term:arg : term => do
+scoped elab:max "MDiff" ppSpace t:term:arg : term => do
   let e ← Term.elabTerm t none
-  let etype ← inferType e >>= instantiateMVars
-  match ← _find_models etype e none with
-  | some (srcI, tgtI) => return ← mkAppM ``MDifferentiable #[srcI, tgtI, e]
-  | none => throwError m!"Term {e} is not a function."
+  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. -/
-elab:max "CMDiffAt[" s:term:arg "]" ppSpace nt:term:arg ppSpace f:term:arg : term => do
+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 wtn ← Term.elabTerm (← `(WithTop ℕ∞)) none
-  let ne ← Term.elabTermEnsuringType nt wtn
-  let estype ← inferType es >>= instantiateMVars
-  let eftype ← inferType ef >>= instantiateMVars
-  match ← _find_models eftype ef estype with
-  | some (srcI, tgtI) => return ← mkAppM ``ContMDiffWithinAt #[srcI, tgtI, ne, ef, es]
-  | none => throwError m!"Term {ef} is not a function."
+  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. -/
-elab:max "CMDiffAt" ppSpace nt:term:arg ppSpace t:term:arg : term => do
+scoped elab:max "CMDiffAt" ppSpace nt:term:arg ppSpace t:term:arg : term => do
   let e ← Term.elabTerm t none
-  let wtn ← Term.elabTerm (← ``(WithTop ℕ∞)) none
-  let ne ← Term.elabTermEnsuringType nt wtn
-  let etype ← inferType e >>= instantiateMVars
-  match ← _find_models etype e none with
-  | some (srcI, tgtI) => return ← mkAppM ``ContMDiffAt #[srcI, tgtI, ne, e]
-  | none => throwError m!"Term {e} is not a function."
+  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). -/
-elab:max "CMDiff[" s:term:arg "]" ppSpace nt:term:arg ppSpace f:term:arg : term => do
+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 wtn ← Term.elabTerm (← ``(WithTop ℕ∞)) none
-  let ne ← Term.elabTermEnsuringType nt wtn
-  let estype ← inferType es >>= instantiateMVars
-  let eftype ← inferType ef >>= instantiateMVars
-  match ← _find_models eftype ef estype with
-  | some (srcI, tgtI) => return ← mkAppM ``ContMDiffOn #[srcI, tgtI, ne, ef, es]
-  | none => throwError m!"Term {ef} is not a function."
+  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). -/
-elab:max "CMDiff" ppSpace nt:term:arg ppSpace f:term:arg : term => do
+scoped elab:max "CMDiff" ppSpace nt:term:arg ppSpace f:term:arg : term => do
   let e ← Term.elabTerm f none
-  let wtn ← Term.elabTerm (← `(WithTop ℕ∞)) none
-  let ne ← Term.elabTermEnsuringType nt wtn
-  let etype ← inferType e >>= instantiateMVars
-  match ← _find_models etype e none with
-  | some (srcI, tgtI) => return ← mkAppM ``ContMDiff #[srcI, tgtI, ne, e]
-  | none => throwError m!"Term {e} is not a function."
+  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. -/
-elab:max "mfderiv[" s:term:arg "]" ppSpace t:term:arg : term => do
+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 etype ← inferType e >>= instantiateMVars
-  let estype ← inferType es >>= instantiateMVars
-  match ← _find_models etype e estype with
-  | some (srcI, tgtI) => return ← mkAppM ``mfderivWithin #[srcI, tgtI, e, es]
-  | none => throwError m!"Term {e} is not a function."
+  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. -/
-elab:max "mfderiv%" ppSpace t:term:arg : term => do
+scoped elab:max "mfderiv%" ppSpace t:term:arg : term => do
   let e ← Term.elabTerm t none
-  let etype ← inferType e >>= instantiateMVars
-  match ← _find_models etype e none with
-  | some (srcI, tgtI) => return ← mkAppM ``mfderiv #[srcI, tgtI, e]
-  | none => throwError m!"Term {e} is not a function."
+  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/Mathlib/Geometry/Manifold/Traces.lean b/Mathlib/Geometry/Manifold/Traces.lean
deleted file mode 100644
index 83cdf708992932..00000000000000
--- a/Mathlib/Geometry/Manifold/Traces.lean
+++ /dev/null
@@ -1,25 +0,0 @@
-/-
-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
--/
-import Lean.Util.Trace
-
-/-!
-# Trace classes for differential geometry elaborators
-
-This file defines custom trace classes for the differential geometry elaborators in
-`Mathlib.Geometry.Manifold.Elaborators.lean`. These need to be in a different file for technical
-reasons.
-
-The `TotalSpaceMk` trace class is associated to the `T%` elaborator, which converts a section
-of a vector bundle as a dependent function to a non-dependent function into the total space.
-
-The `MDiffElab` trace class corresponds to the elaborators `CMDiff` and friends, and provides
-tracing information about inferring a model with corners on the domain (resp. codomain) of the
-map in question.
--/
-open Lean
-
-initialize registerTraceClass `TotalSpaceMk
-initialize registerTraceClass `MDiffElab
diff --git a/Mathlib/Lean/Elab/Term.lean b/Mathlib/Lean/Elab/Term.lean
index c0686023880829..d536cad0358b2b 100644
--- a/Mathlib/Lean/Elab/Term.lean
+++ b/Mathlib/Lean/Elab/Term.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kyle Miller
 -/
 import Mathlib.Init
-import Lean.Elab.Term
+import Lean.Elab.SyntheticMVars
 
 /-!
 # Additions to `Lean.Elab.Term`
@@ -23,13 +23,4 @@ def elabPattern (patt : Term) (expectedType? : Option Expr) : TermElabM Expr :=
       synthesizeSyntheticMVars (postpone := .no) (ignoreStuckTC := true)
       instantiateMVars t
 
-open Meta
-
-/-- Try to infer the universe of an expression `e` -/
-def _root_.Lean.Expr.getUniverse (e : Expr) : TermElabM (Level) := do
-    if let .sort (.succ u) ← inferType e >>= instantiateMVars then
-      return u
-    else
-      throwError m!"Could not find universe of {e}."
-
 end Lean.Elab.Term
diff --git a/Mathlib/Lean/Expr/Basic.lean b/Mathlib/Lean/Expr/Basic.lean
index ac3b8279a27cd6..9e4566f242162b 100644
--- a/Mathlib/Lean/Expr/Basic.lean
+++ b/Mathlib/Lean/Expr/Basic.lean
@@ -164,10 +164,6 @@ namespace Expr
 
 /-! ### Declarations about `Expr` -/
 
-/-- Call `mkApp` recursively with 12 arguments -/
-@[match_pattern] def _root_.mkApp12 (f a b c d e g e₁ e₂ e₃ e₄ e₅ e₆ : Expr) :=
-  mkApp6 (mkApp6 f a b c d e g) e₁ e₂ e₃ e₄ e₅ e₆
-
 def bvarIdx? : Expr → Option Nat
   | bvar idx => some idx
   | _        => none
diff --git a/MathlibTest/DifferentialGeometry/Elaborators.lean b/MathlibTest/DifferentialGeometry/Elaborators.lean
index 37fce684ce61a6..3cfe0941992e69 100644
--- a/MathlibTest/DifferentialGeometry/Elaborators.lean
+++ b/MathlibTest/DifferentialGeometry/Elaborators.lean
@@ -112,20 +112,6 @@ variable {f : M → M'} {s : Set M} {m : M}
 #guard_msgs in
 #check MDiffAt f
 
--- TODO: understand why this fails and fix it!
-/--
-error: Application type mismatch: The argument
-  a✝
-has type
-  M
-of sort `Type u_4` but is expected to have type
-  Type ?u.63952
-of sort `Type (?u.63952 + 1)` in the application
-  @modelWithCornersSelf a✝
--/
-#guard_msgs in
-#check MDiffAt2 f
-
 /-- info: MDifferentiableAt I I' f m : Prop -/
 #guard_msgs in
 #check MDiffAt f m
@@ -322,63 +308,63 @@ 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
+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
+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
+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
+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
+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
+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
+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
+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
+Hint: you can use the `T%` elaborator to convert a dependent function to a non-dependent one
 -/
 #guard_msgs in
 #check MDiffAt[s] σ'
@@ -418,7 +404,11 @@ of sort `Type (max u_10 u_4)` but is expected to have type
   WithTop ℕ∞
 of sort `Type`
 ---
-error: Term m is not a function.
+error: Expected
+  m
+of type
+  M
+to be a function
 -/
 #guard_msgs in
 #check CMDiffAt[s] f m
@@ -432,7 +422,11 @@ of sort `Type (max u_10 u_4)` but is expected to have type
   WithTop ℕ∞
 of sort `Type`
 ---
-error: Term m is not a function.
+error: Expected
+  m
+of type
+  M
+to be a function
 -/
 #guard_msgs in
 #check CMDiffAt[s] f m
@@ -591,63 +585,63 @@ 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
+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
+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
+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
+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
+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
+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
+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
+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
+Hint: you can use the `T%` elaborator to convert a dependent function to a non-dependent one
 -/
 #guard_msgs in
 #check CMDiffAt[s] 0 σ'
@@ -844,27 +838,15 @@ info: mfderiv 𝓘(𝕜, E) 𝓘(𝕜, EM') f sorry : TangentSpace 𝓘(𝕜, E)
 #guard_msgs in
 #check mfderiv% f m'
 
--- TODO: is the old error message better?
-/-
-error: Application type mismatch: The argument
-  s'
-has type
-  Set.{u_4} M
-of sort `Type u_4` but is expected to have type
-  Set.{u_2} E
-of sort `Type u_2` in the application
-  mfderivWithin 𝓘(𝕜, E) 𝓘(𝕜, EM') f s'
--/
-
 -- Error messages: argument s has mismatched type.
 /--
-error: The domain E of f is not definitionally equal to the carrier of the type 'Set M' of the set 's' passed in
+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 of the type 'Set M' of the set 's' passed in
+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
@@ -875,14 +857,14 @@ 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
+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
+Hint: you can use the `T%` elaborator to convert a dependent function to a non-dependent one
 -/
 #guard_msgs in
 #check mfderiv% σ x
@@ -891,14 +873,14 @@ 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
+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
+Hint: you can use the `T%` elaborator to convert a dependent function to a non-dependent one
 -/
 #guard_msgs in
 #check mfderiv[t] σ'
@@ -906,3 +888,44 @@ Hint: you can use the 'T%' elaborator to convert a dependent function to a non-d
 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 99609d4075c6ca..ff19c31cadcd7e 100644
--- a/scripts/noshake.json
+++ b/scripts/noshake.json
@@ -51,7 +51,6 @@
   "Mathlib.Data.Vector.Basic",
   "Mathlib.Geometry.Manifold.Instances.Real",
   "Mathlib.Geometry.Manifold.Elaborators",
-  "Mathlib.Geometry.Manifold.Traces",
   "Mathlib.Init",
   "Mathlib.LinearAlgebra.AffineSpace.Basic",
   "Mathlib.LinearAlgebra.Matrix.Notation",