From d00d8a2104724050da99f01a8d050f0272d27291 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 6 Jun 2022 07:57:23 -0700
Subject: [PATCH] fix: typo at `copyDefaultValue?`

see #1190
---
 src/Lean/Elab/Structure.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index f79a63ef6a..a8271c22b6 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -388,7 +388,7 @@ where
         go? (b.instantiate1 arg)
     | e =>
       let r := if e.isAppOfArity ``id 2 then e.appArg! else e
-      return some (← reduceProjs (← instantiateMVars e.appArg!) expandedStructNames)
+      return some (← reduceProjs (← instantiateMVars r) expandedStructNames)
 
 private partial def copyNewFieldsFrom (structDeclName : Name) (infos : Array StructFieldInfo) (parentType : Expr) (k : Array StructFieldInfo → TermElabM α) : TermElabM α := do
   copyFields infos {} parentType fun infos _ _ => k infos