From 108bc4c27f75c13752cc48f3188484b735c1acd8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 22 Jun 2022 19:40:06 -0700
Subject: [PATCH] fix: `extCore`

---
 src/Lean/Elab/Tactic/Conv/Congr.lean | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Elab/Tactic/Conv/Congr.lean b/src/Lean/Elab/Tactic/Conv/Congr.lean
index c6359585e3..4714ee0a81 100644
--- a/src/Lean/Elab/Tactic/Conv/Congr.lean
+++ b/src/Lean/Elab/Tactic/Conv/Congr.lean
@@ -139,20 +139,20 @@ private def extCore (mvarId : MVarId) (userName? : Option Name) : MetaM MVarId :
    withMVarContext mvarId do
      let userNames := if let some userName := userName? then [userName] else []
      let (lhs, rhs) ← getLhsRhsCore mvarId
-     let lhs := (← instantiateMVars lhs).consumeMDataAndTypeAnnotations
-     let goForall (mvarId : MVarId) := do
+     let lhs ← instantiateMVars lhs
+     if lhs.isForall then
        let [mvarId, _] ← apply mvarId (← mkConstWithFreshMVarLevels ``forall_congr) | throwError "'apply forall_congr' unexpected result"
        let (_, mvarId) ← introN mvarId 1 userNames
        markAsConvGoal mvarId
-     if lhs.isForall then
-       goForall mvarId
      else if let some mvarId ← extLetBodyCongr? mvarId lhs rhs then
        return mvarId
      else
        let lhsType ← whnfD (← inferType lhs)
        unless lhsType.isForall do
          throwError "invalid 'ext' conv tactic, function or arrow expected{indentD m!"{lhs} : {lhsType}"}"
-       goForall mvarId
+       let [mvarId] ← apply mvarId (← mkConstWithFreshMVarLevels ``funext) | throwError "'apply funext' unexpected result"
+       let (_, mvarId) ← introN mvarId 1 userNames
+       markAsConvGoal mvarId
 
 private def ext (userName? : Option Name) : TacticM Unit := do
   replaceMainGoal [← extCore (← getMainGoal) userName?]