From 74908bb9c7af439ee55ec3ff1c89cd7448e6bde6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 8 Mar 2020 11:31:05 -0700
Subject: [PATCH] fix: typo

---
 src/Init/Lean/Meta/Tactic/Injection.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Lean/Meta/Tactic/Injection.lean b/src/Init/Lean/Meta/Tactic/Injection.lean
index 8872bbfbb9..a76db94c8f 100644
--- a/src/Init/Lean/Meta/Tactic/Injection.lean
+++ b/src/Init/Lean/Meta/Tactic/Injection.lean
@@ -54,7 +54,7 @@ withMVarContext mvarId $ do
           newMVar ← mkFreshExprSyntheticOpaqueMVar newTarget tag;
           assignExprMVar mvarId (mkApp val newMVar);
           mvarId ← tryClear newMVar.mvarId! fvarId;
-          pure $ InjectionResultCore.subgoal newMVar.mvarId! aCtor.nfields
+          pure $ InjectionResultCore.subgoal mvarId aCtor.nfields
         | _ => throwTacticEx `injection mvarId "ill-formed noConfusion auxiliary construction"
     | _, _ => throwTacticEx `injection mvarId "equality of constructor applications expected"