feat: have notation3 use elaborator when generating matchers, add support for pi/lambda (#6833)

`notation3` was generating matchers directly from syntax, which included a half-baked implementation of a term elaborator. This switches to elaborating the term and then generating matchers from the elaborated term. This
1. is more robust and consistent, since it uses the main elaborator and one can make use of other notations
2. has the nice side effect of adding term info to expansions in the `notation3` command
3. can unfortunately generate matchers that are more restrictive than before since they also match against elaborated features such as implicit arguments.

We now also generate matchers for expansions that have pi types and lambda expressions.

Author: kmill

Mathlib.lean

@@ -2198,6 +2198,7 @@ import Mathlib.Init.ZeroOne
 import Mathlib.Lean.CoreM
 import Mathlib.Lean.Data.NameMap
 import Mathlib.Lean.Elab.Tactic.Basic
+import Mathlib.Lean.Elab.Term
 import Mathlib.Lean.EnvExtension
 import Mathlib.Lean.Exception
 import Mathlib.Lean.Expr
@@ -2215,6 +2216,7 @@ import Mathlib.Lean.Meta.CongrTheorems
 import Mathlib.Lean.Meta.DiscrTree
 import Mathlib.Lean.Meta.Simp
 import Mathlib.Lean.Name
+import Mathlib.Lean.PrettyPrinter.Delaborator
 import Mathlib.Lean.SMap
 import Mathlib.Lean.System.IO
 import Mathlib.Lean.Thunk

Mathlib/Algebra/Lie/Weights/Basic.lean

@@ -55,8 +55,7 @@ open scoped BigOperators TensorProduct
 section notation_weight_space_of
 
 /-- Until we define `LieModule.weightSpaceOf`, it is useful to have some notation as follows: -/
-local notation3 (prettyPrint := false) "𝕎("M"," χ"," x")" =>
-  (toEndomorphism R L M x).maximalGeneralizedEigenspace χ
+local notation3 "𝕎("M", " χ", " x")" => (toEndomorphism R L M x).maximalGeneralizedEigenspace χ
 
 /-- See also `bourbaki1975b` Chapter VII §1.1, Proposition 2 (ii). -/
 protected theorem weight_vector_multiplication (M₁ M₂ M₃ : Type*)

Mathlib/Algebra/Order/Nonneg/Module.lean

@@ -21,8 +21,7 @@ variable {𝕜 𝕜' E : Type*}
 
 variable [OrderedSemiring 𝕜]
 
--- TODO: remove `prettyPrint := false` once #6833 is merged
-local notation3 (prettyPrint := false) "𝕜≥0" => {c : 𝕜 // 0 ≤ c}
+local notation3 "𝕜≥0" => {c : 𝕜 // 0 ≤ c}
 
 namespace Nonneg
 

Mathlib/AlgebraicGeometry/Restrict.lean

@@ -37,14 +37,11 @@ variable (X : Scheme)
 
 /-- `f ⁻¹ᵁ U` is notation for `(Opens.map f.1.base).obj U`,
   the preimage of an open set `U` under `f`. -/
-notation3:90 f:91 "⁻¹ᵁ " U:90 => Prefunctor.obj
-  (Functor.toPrefunctor <| Opens.map (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.val f))) U
+notation3:90 f:91 "⁻¹ᵁ " U:90 => (Opens.map (f : LocallyRingedSpace.Hom _ _).val.base).obj U
 
 /-- `X ∣_ᵤ U` is notation for `X.restrict U.openEmbedding`, the restriction of `X` to an open set
   `U` of `X`. -/
-notation3:60 X:60 " ∣_ᵤ " U:61 => (Scheme.restrict X (Opens.openEmbedding U))
-
-attribute [nolint docBlame] «term_⁻¹ᵁ_».delab «term_∣_ᵤ_».delab
+notation3:60 X:60 " ∣_ᵤ " U:61 => Scheme.restrict X (U : Opens X).openEmbedding
 
 /-- The restriction of a scheme to an open subset. -/
 abbrev Scheme.ιOpens {X : Scheme} (U : Opens X.carrier) : X ∣_ᵤ U ⟶ X := X.ofRestrict _

Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean

@@ -65,11 +65,9 @@ open SzemerediRegularity
 variable {α : Type*} [DecidableEq α] [Fintype α] {P : Finpartition (univ : Finset α)}
   {u : Finset α} {ε : ℝ}
 
-local notation3 (prettyPrint := false)
-  "m" => (card α / stepBound P.parts.card : ℕ)
+local notation3 "m" => (card α / stepBound P.parts.card : ℕ)
 
-local notation3 (prettyPrint := false)
-  "a" => (card α / P.parts.card - m * 4 ^ P.parts.card : ℕ)
+local notation3 "a" => (card α / P.parts.card - m * 4 ^ P.parts.card : ℕ)
 
 namespace SzemerediRegularity.Positivity
 

Mathlib/Combinatorics/SimpleGraph/Regularity/Chunk.lean

@@ -48,8 +48,7 @@ namespace SzemerediRegularity
 variable {α : Type*} [Fintype α] {P : Finpartition (univ : Finset α)} (hP : P.IsEquipartition)
   (G : SimpleGraph α) (ε : ℝ) {U : Finset α} (hU : U ∈ P.parts) (V : Finset α)
 
-local notation3 (prettyPrint := false)
-  "m" => (card α / stepBound P.parts.card : ℕ)
+local notation3 "m" => (card α / stepBound P.parts.card : ℕ)
 
 /-!
 ### Definitions

Mathlib/Combinatorics/SimpleGraph/Regularity/Increment.lean

@@ -45,8 +45,7 @@ open scoped BigOperators Classical SzemerediRegularity.Positivity
 variable {α : Type*} [Fintype α] {P : Finpartition (univ : Finset α)} (hP : P.IsEquipartition)
   (G : SimpleGraph α) (ε : ℝ)
 
-local notation3 (prettyPrint := false)
-  "m" => (card α / stepBound P.parts.card : ℕ)
+local notation3 "m" => (card α / stepBound P.parts.card : ℕ)
 
 namespace SzemerediRegularity
 

Mathlib/Data/PSigma/Order.lean

@@ -37,7 +37,8 @@ namespace PSigma
 
 /-- The notation `Σₗ' i, α i` refers to a sigma type which is locally equipped with the
 lexicographic order.-/
-notation3 "Σₗ' "(...)", "r:(scoped p => _root_.Lex (PSigma p)) => r
+-- TODO: make `Lex` be `Sort u -> Sort u` so we can remove `.{_+1, _+1}`
+notation3 "Σₗ' "(...)", "r:(scoped p => _root_.Lex (PSigma.{_+1, _+1} p)) => r
 
 namespace Lex
 

Mathlib/Lean/Elab/Term.lean

@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2023 Kyle Miller. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+-/
+import Lean.Elab
+
+/-!
+# Additions to `Lean.Elab.Term`
+-/
+
+namespace Lean.Elab.Term
+
+/-- Fully elaborates the term `patt`, allowing typeclass inference failure,
+but while setting `errToSorry` to false.
+Typeclass failures result in plain metavariables.
+Instantiates all assigned metavariables. -/
+def elabPattern (patt : Term) (expectedType? : Option Expr) : TermElabM Expr := do
+  withTheReader Term.Context ({ · with ignoreTCFailures := true, errToSorry := false }) <|
+    withSynthesizeLight do
+      let t ← elabTerm patt expectedType?
+      synthesizeSyntheticMVars (mayPostpone := false) (ignoreStuckTC := true)
+      instantiateMVars t

Mathlib/Lean/PrettyPrinter/Delaborator.lean

@@ -0,0 +1,48 @@
+/-
+Copyright (c) 2023 Kyle Miller. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+-/
+import Lean.PrettyPrinter.Delaborator.Basic
+
+/-!
+# Additions to the delaborator
+-/
+
+namespace Lean.PrettyPrinter.Delaborator
+
+open Lean.Meta Lean.SubExpr SubExpr
+
+namespace SubExpr
+
+variable {α : Type} [Inhabited α]
+variable {m : Type → Type} [Monad m]
+
+section Descend
+
+variable [MonadReaderOf SubExpr m] [MonadWithReaderOf SubExpr m]
+variable [MonadLiftT MetaM m] [MonadControlT MetaM m]
+variable [MonadLiftT IO m]
+
+/-- Assuming the current expression is a lambda or pi,
+descend into the body using the given name `n` for the username of the fvar.
+Provides `x` with the fresh fvar for the bound variable.
+See also `Lean.PrettyPrinter.Delaborator.SubExpr.withBindingBody`. -/
+def withBindingBody' (n : Name) (x : Expr → m α) : m α := do
+  let e ← getExpr
+  Meta.withLocalDecl n e.binderInfo e.bindingDomain! fun fvar =>
+    descend (e.bindingBody!.instantiate1 fvar) 1 (x fvar)
+
+end Descend
+
+end SubExpr
+
+/-- Assuming the current expression in a lambda or pi,
+descend into the body using an unused name generated from the binder's name.
+Provides `d` with both `Syntax` for the bound name as an identifier
+as well as the fresh fvar for the bound variable.
+See also `Lean.PrettyPrinter.Delaborator.withBindingBodyUnusedName`. -/
+def withBindingBodyUnusedName' {α} (d : Syntax → Expr → DelabM α) : DelabM α := do
+  let n ← getUnusedName (← getExpr).bindingName! (← getExpr).bindingBody!
+  let stxN ← annotateCurPos (mkIdent n)
+  withBindingBody' n $ d stxN