chore: use more mkApp(Opt)M in the differential geometry elaborators (leanprover-community#40933)

This is more concise (and perhaps even more efficient) than converting an existing expression to Syntax and re-elaborating that. No need for this.

Author: grunweg

Mathlib/Geometry/Manifold/Notation.lean

@@ -430,7 +430,7 @@ where
         let some K ← guessBaseFieldForNormedSpace F
           | throwError "Couldn't find a `NormedSpace` structure on `{F}`"
         let tgtMod ← mkAppOptM ``modelWithCornersSelf #[K, none, F, none, none]
-        mkAppM ``ModelWithCorners.prod  #[baseModel, tgtMod]
+        mkAppM ``ModelWithCorners.prod #[baseModel, tgtMod]
       | _ =>
         throwError s!"{e} is a TotalSpace {F} {V}, but {V} is not a pi type --- \
           could not infer base of the bundle"
@@ -440,18 +440,14 @@ where
     match_expr V with
     | TangentSpace _k _ _E _ _ _H _ I M _ _ => do
       trace[Elab.DiffGeo.MDiff] "`{V}` is the total space of the `TangentBundle` of `{M}`"
-      let srcIT : Term ← Term.exprToSyntax I
-      let resTerm : Term ← ``(ModelWithCorners.tangent $srcIT)
-      Term.elabTerm resTerm none
+      mkAppM ``ModelWithCorners.tangent #[I]
     | _ => throwError "`{V}` is not a `TangentSpace`"
   /-- Attempt to find a model on a `TangentBundle` -/
   fromTangentBundle : TermElabM Expr := do
     match_expr e with
     | TangentBundle _k _ _E _ _ _H _ I M _ _ => do
       trace[Elab.DiffGeo.MDiff] "`{e}` is a `TangentBundle` over model `{I}` on `{M}`"
-      let srcIT : Term ← Term.exprToSyntax I
-      let resTerm : Term ← ``(ModelWithCorners.tangent $srcIT)
-      Term.elabTerm resTerm none
+      mkAppM ``ModelWithCorners.tangent #[I]
     | _ => throwError "`{e}` is not a `TangentBundle`"
   /-- Attempt to find the trivial model on a normed space. -/
   fromNormedSpace : TermElabM FindModelResult := do
@@ -534,18 +530,13 @@ where
     -- the standard model with corners.
     -- Therefore, we only check definitional equality at reducible transparency.
     let (k, _E, _F) ← isCLMReduciblyDefeqCoefficients e
-    let eK : Term ← Term.exprToSyntax k
-    let eT : Term ← Term.exprToSyntax e
-    let iTerm : Term ← ``(𝓘($eK, $eT))
-    Term.elabTerm iTerm none
+    mkAppOptM ``modelWithCornersSelf #[k, none, e, none, none]
   /-- Attempt to find a model with corners on a Euclidean space, half-space or quadrant -/
   fromEuclideanSpace : TermElabM Expr := do
     -- We don't use `match_expr` to avoid importing `EuclideanHalfSpace`.
     match (← instantiateMVars e).cleanupAnnotations with
     | mkApp2 (.const `EuclideanSpace _) k _n =>
-      let eK : Term ← Term.exprToSyntax k
-      let eT : Term ← Term.exprToSyntax e
-      Term.elabTerm (← ``(𝓘($eK, $eT))) none
+      mkAppOptM ``modelWithCornersSelf #[k, none, e, none, none]
     | mkApp2 (.const `EuclideanHalfSpace _) n _ =>
       mkAppOptM `modelWithCornersEuclideanHalfSpace #[n, none]
     | mkApp (.const `EuclideanQuadrant _) n =>
@@ -606,9 +597,7 @@ where
           | _ => return none
       if let some (k, R) := searchNormedAlgebra then
         trace[Elab.DiffGeo.MDiff] "found a normed algebra: `{α}` is a normed `{k}`-algebra"
-        let eK : Term ← Term.exprToSyntax k
-        let eR : Term ← Term.exprToSyntax R
-        Term.elabTerm (← ``(𝓘($eK, $eR))) none
+        mkAppOptM ``modelWithCornersSelf #[k, none, R, none, none]
       else
         trace[Elab.DiffGeo.MDiff] "`{α}` is not a normed algebra on the nose: try via a space of \
           continuous linear maps"
@@ -633,9 +622,7 @@ where
           match normedSpace? with
           | some (k, _R) =>
             trace[Elab.DiffGeo.MDiff] "found a normed space: `{V}` is a normed space over `{k}`"
-            let eK : Term ← Term.exprToSyntax k
-            let eα : Term ← Term.exprToSyntax α
-            Term.elabTerm (← ``(𝓘($eK, $eα))) none
+            mkAppOptM ``modelWithCornersSelf #[k, none, α, none, none]
           | _ => throwError  "Found no `NormedSpace` structure on `{V}` among local instances"
         else
           -- NB. If further instances of `NormedAlgebra` arise in practice, adding another check
@@ -724,10 +711,7 @@ where
     | _ => throwError "`{e}` is not a sphere in a real normed space"
   /-- 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
+  fromNormedField : TermElabM Expr := mkAppOptM ``modelWithCornersSelf #[e, none, e, none, none]
 
 /-- Try to find a `ModelWithCorners` instance on a type (represented by an expression `e`),
 using the local context to infer the appropriate instance.
@@ -802,10 +786,7 @@ where
         throwError "`{e}` is a product of normed spaces, so there are two potential models with \
         corners\nFor now, please specify the model by hand."
       -- Otherwise, we are not a normed space, and normally form the product model.
-      let eTerm : Term ← Term.exprToSyntax srcE
-      let fTerm : Term ← Term.exprToSyntax srcF
-      let iTerm : Term ← ``(ModelWithCorners.prod $eTerm $fTerm)
-      return some { model := ← Term.elabTerm iTerm none }
+      return some { model := ← mkAppM ``ModelWithCorners.prod #[srcE, srcF] }
     | Sum E F =>
       trace[Elab.DiffGeo.MDiff] "Expression `{e}` is a direct sum of `{E}` and `{F}`\n\
         We assume the models match, and only look into the first summand"

MathlibTest/DifferentialGeometry/Notation/Advanced.lean

@@ -378,10 +378,10 @@ trace: [Elab.DiffGeo.MDiff] Finding a model with corners for: `M`
       `ContinuousLinearMap id' E'' E'''` is not a coercion of a set to a type
 [Elab.DiffGeo.MDiff] 💥️ NormedField
   [Elab.DiffGeo.MDiff] Failed with error:
-      failed to synthesize instance of type class
+      failed to synthesize
         NontriviallyNormedField (ContinuousLinearMap id' E'' E''')
       ⏎
-      Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+      Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 [Elab.DiffGeo.MDiff] 💥️ InnerProductSpace
   [Elab.DiffGeo.MDiff] Failed with error:
       Couldn't find an `InnerProductSpace` structure on `ContinuousLinearMap id' E'' E'''` among local instances.
@@ -481,10 +481,10 @@ trace: [Elab.DiffGeo.MDiff] Finding a model with corners for: `M`
       `ContinuousLinearMap σ E'' E''''` is not a coercion of a set to a type
 [Elab.DiffGeo.MDiff] 💥️ NormedField
   [Elab.DiffGeo.MDiff] Failed with error:
-      failed to synthesize instance of type class
+      failed to synthesize
         NontriviallyNormedField (ContinuousLinearMap σ E'' E'''')
       ⏎
-      Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+      Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 [Elab.DiffGeo.MDiff] 💥️ InnerProductSpace
   [Elab.DiffGeo.MDiff] Failed with error:
       Couldn't find an `InnerProductSpace` structure on `ContinuousLinearMap σ E'' E''''` among local instances.
@@ -686,10 +686,10 @@ trace: [Elab.DiffGeo.MDiff] Finding a model with corners for: `↑(Set.Icc x y)`
       `Set.Icc x y` is not a sphere in a real normed space
 [Elab.DiffGeo.MDiff] 💥️ NormedField
   [Elab.DiffGeo.MDiff] Failed with error:
-      failed to synthesize instance of type class
+      failed to synthesize
         NontriviallyNormedField ↑(Set.Icc x y)
       ⏎
-      Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+      Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 [Elab.DiffGeo.MDiff] 💥️ InnerProductSpace
   [Elab.DiffGeo.MDiff] Failed with error:
       Couldn't find an `InnerProductSpace` structure on `↑(Set.Icc x y)` among local instances.

MathlibTest/DifferentialGeometry/Notation/Basic.lean

@@ -1470,10 +1470,10 @@ trace: [Elab.DiffGeo.MDiff] Finding a model with corners for: `Unit`
       `Unit` is not a coercion of a set to a type
 [Elab.DiffGeo.MDiff] 💥️ NormedField
   [Elab.DiffGeo.MDiff] Failed with error:
-      failed to synthesize instance of type class
+      failed to synthesize
         NontriviallyNormedField Unit
       ⏎
-      Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+      Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 [Elab.DiffGeo.MDiff] 💥️ InnerProductSpace
   [Elab.DiffGeo.MDiff] Failed with error:
       Couldn't find an `InnerProductSpace` structure on `Unit` among local instances.

MathlibTest/DifferentialGeometry/Notation/Sphere.lean

@@ -230,10 +230,10 @@ trace: [Elab.DiffGeo.MDiff] Finding a model with corners for: `↑(Metric.sphere
       Found no fact `finrank ℝ E'' = n + 1` in the local context
 [Elab.DiffGeo.MDiff] 💥️ NormedField
   [Elab.DiffGeo.MDiff] Failed with error:
-      failed to synthesize instance of type class
+      failed to synthesize
         NontriviallyNormedField ↑(Metric.sphere 0 1)
       ⏎
-      Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
+      Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 [Elab.DiffGeo.MDiff] 💥️ InnerProductSpace
   [Elab.DiffGeo.MDiff] Failed with error:
       Couldn't find an `InnerProductSpace` structure on `↑(Metric.sphere 0 1)` among local instances.