From 873a2ba8a696b8763acfd1e2b2b98971b5c8e04c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 18 Jan 2022 15:03:20 -0800
Subject: [PATCH] feat: unfold `namedPattern` applications at equation theorems

---
 src/Lean/Elab/PreDefinition/Eqns.lean | 1 +
 src/Lean/Meta/Match/MatchEqs.lean     | 9 +++++++++
 2 files changed, 10 insertions(+)

diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean
index 258afbd90c..153b23d379 100644
--- a/src/Lean/Elab/PreDefinition/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/Eqns.lean
@@ -88,6 +88,7 @@ private def saveEqn (mvarId : MVarId) : StateRefT (Array Expr) MetaM Unit := wit
         if missing?.isNone then
           fvarIds := fvarIds.push decl.fvarId
   let type ← mkForallFVars (fvarIds.map mkFVar) target
+  let type ← Match.unfoldNamedPattern type
   modify (·.push type)
 
 partial def mkEqnTypes (declNames : Array Name) (mvarId : MVarId) : MetaM (Array Expr) := do
diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean
index 282a497620..130005ad11 100644
--- a/src/Lean/Meta/Match/MatchEqs.lean
+++ b/src/Lean/Meta/Match/MatchEqs.lean
@@ -273,6 +273,14 @@ where
     let mvarId ← tryClearMany mvarId (alts.map (·.fvarId!))
     proveSubgoalLoop mvarId
 
+def unfoldNamedPattern (e : Expr) : MetaM Expr := do
+  let visit (e : Expr) : MetaM TransformStep := do
+    if e.isAppOfArity ``namedPattern 4 then
+      if let some eNew ← unfoldDefinition? e then
+        return TransformStep.visit eNew
+    return TransformStep.visit e
+  Meta.transform e (pre := visit)
+
 /--
   Create conditional equations and splitter for the given match auxiliary declaration. -/
 private partial def mkEquationsFor (matchDeclName : Name) :  MetaM MatchEqns :=
@@ -316,6 +324,7 @@ private partial def mkEquationsFor (matchDeclName : Name) :  MetaM MatchEqns :=
         let thmType ← mkEq lhs rhs
         let thmType ← hs.foldrM (init := thmType) mkArrow
         let thmType ← mkForallFVars (params ++ #[motive] ++ alts ++ ys) thmType
+        let thmType ← unfoldNamedPattern thmType
         let thmVal ← proveCondEqThm matchDeclName thmType
         addDecl <| Declaration.thmDecl {
           name        := thmName