better

Author: grunweg

Mathlib/Geometry/Manifold/Notation.lean

@@ -312,6 +312,13 @@ where
     let iTerm : Term ← ``(𝓘($eT, $eT))
     Term.elabTerm iTerm none
 
+/-- Ensures that `e` is a function. Attempts to coerce `e` to a function if necessary. -/
+def ensureIsFunction (e : Expr) : MetaM Expr := do
+  let ty ← whnf <|← instantiateMVars <|← inferType e
+  if ty.isForall then return e else (← coerceToFunction? e).getDM <|
+    throwError "Expected{indentD e}\nof type{indentD ty}\nto be a function, or to be coercible to \
+      a function"
+
 /-- 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.
 
@@ -337,43 +344,7 @@ def findModels (e : Expr) (es : Option Expr) : TermElabM (Expr × Expr) := do
           the set {es} : {estype}"
     let tgtI ← findModel tgt (src, srcI)
     return (srcI, tgtI)
-  | _ =>
-    match_expr etype with
-    | OpenPartialHomeomorph src tgt _ _ =>
-      trace[Elab.DiffGeo.MDiff] m!"found a partial homeomorphism from {src} to {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)
-    | PartialEquiv src tgt =>
-      trace[Elab.DiffGeo.MDiff] m!"found a partial equivalence from {src} to {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"
+  | _ => throwError "Expected{indentD e}\nof type{indentD etype}\nto be a function"
 
 end Elab
 
@@ -384,7 +355,7 @@ 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 ef ← ensureIsFunction <|← Term.elabTerm f none
   let (srcI, tgtI) ← findModels ef es
   mkAppM ``MDifferentiableWithinAt #[srcI, tgtI, ef, es]
 

MathlibTest/DifferentialGeometry/Notation.lean

@@ -120,40 +120,21 @@ variable {f : M → M'} {s : Set M} {m : M}
 #guard_msgs in
 #check MDiff[s] f
 
--- A partial homeomorphism or partial equivalence.
-variable {φ : OpenPartialHomeomorph M E} {ψ : PartialEquiv M E}
-
-#check MDifferentiableWithinAt I 𝓘(𝕜, E) ψ
-#check MDifferentiableWithinAt I 𝓘(𝕜, E) ψ s
+/-! A partial homeomorphism or partial equivalence. More generally, this works for any type
+with a coercion to (possibly dependent) functions. -/
+section coercion
 
+variable {φ : OpenPartialHomeomorph M E} {ψ : PartialEquiv M E}
 
-/--
-error: Application type mismatch: The argument
-  φ
-has type
-  OpenPartialHomeomorph M E
-but is expected to have type
-  ?M → ?M'
-in the application
-  MDifferentiableWithinAt I 𝓘(𝕜, E) φ
--/
+/-- info: MDifferentiableWithinAt I 𝓘(𝕜, E) (↑φ) s : M → Prop -/
 #guard_msgs in
 #check MDiffAt[s] φ
 
-/--
-error: Application type mismatch: The argument
-  ψ
-has type
-  PartialEquiv M E
-but is expected to have type
-  ?M → ?M'
-in the application
-  MDifferentiableWithinAt I 𝓘(𝕜, E) ψ
--/
+/-- info: MDifferentiableWithinAt I 𝓘(𝕜, E) (↑ψ) s : M → Prop -/
 #guard_msgs in
 #check MDiffAt[s] ψ
 
-#exit
+end coercion
 
 -- Testing an error message.
 section