From 55441938f40e9f8c4baf4c01227681b937143e28 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Mon, 21 Feb 2022 14:49:29 +0000
Subject: [PATCH] =?UTF-8?q?feat:=20`(=E2=86=91)`=20notation=20for=20coerci?=
 =?UTF-8?q?ons=20(#199)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

See https://github.com/leanprover-community/mathport/issues/116#issuecomment-1046836990

The notation is a bit problematic for the pretty-printer, as it doesn't automatically insert parentheses to disambiguate it from the built-in coercion notation.  Alternatives:
 1. Use a different token.
 2. Magically define `(↑ ∙)` to be the eta-reduction of `fun x => ↑x`.

PS: the old macro for `↑ x` was redundant since it's been moved to core some time ago.
---
 Mathlib/Data/Subtype.lean |  2 +-
 Mathlib/Tactic/Coe.lean   | 26 +++++++++++++++-----------
 2 files changed, 16 insertions(+), 12 deletions(-)

diff --git a/Mathlib/Data/Subtype.lean b/Mathlib/Data/Subtype.lean
index 06fd145bda618..82cc216d6395d 100644
--- a/Mathlib/Data/Subtype.lean
+++ b/Mathlib/Data/Subtype.lean
@@ -84,7 +84,7 @@ f x
 lemma restrict_apply {α} {β : α → Type _} (f : ∀x, β x) (p : α → Prop) (x : Subtype p) :
   restrict f p x = f x.1 := rfl
 
-lemma restrict_def {α β} (f : α → β) (p : α → Prop) : restrict f p = f ∘ CoeHead.coe := rfl
+lemma restrict_def {α β} (f : α → β) (p : α → Prop) : restrict f p = f ∘ (↑) := rfl
 
 lemma restrict_injective {α β} {f : α → β} (p : α → Prop) (h : injective f) :
   injective (restrict f p) :=
diff --git a/Mathlib/Tactic/Coe.lean b/Mathlib/Tactic/Coe.lean
index ad2e01641f10d..31f7b15f8446d 100644
--- a/Mathlib/Tactic/Coe.lean
+++ b/Mathlib/Tactic/Coe.lean
@@ -5,20 +5,24 @@ Author: Gabriel Ebner
 -/
 import Lean
 
-open Lean Elab Term
+open Lean Elab Term Meta
 
 /-!
-Redefine the ↑-notation to elaborate in the same way as type annotations
-(i.e., unfolding the coercion instance).
+Define a `(↑)` notation for coercions equivalent to the eta-reduction of `(↑ ·)`.
 -/
 
 namespace Lean.Elab.Term.CoeImpl
 
-scoped elab "coe%" x:term : term <= expectedType => do
-  tryPostponeIfMVar expectedType
-  let x ← elabTerm x none
-  synthesizeSyntheticMVarsUsingDefault
-  ensureHasType expectedType x
-
-macro_rules
-  | `(↑ $x) => `(coe% $x)
+elab "(" "↑" ")" : term <= expectedType => do
+  let expectedType ← instantiateMVars expectedType
+  let Expr.forallE _ a b .. := expectedType | do
+    tryPostpone
+    throwError "(↑) must have a function type, not{indentExpr expectedType}"
+  if b.hasLooseBVars then
+    tryPostpone
+    throwError "(↑) must have a non-dependent function type, not{indentExpr expectedType}"
+  if a.hasExprMVar then tryPostpone
+  if b.hasExprMVar then tryPostpone
+  let f ← withLocalDeclD `x a fun x => do
+    mkLambdaFVars #[x] (← mkCoe b a x)
+  return f.etaExpanded?.getD f