From 279c34ff4675b81f2ec412164beed46f1633cff3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 28 Oct 2022 07:52:45 -0700
Subject: [PATCH] feat: add `MVarId.eqOfHEq` tactic

---
 src/Lean/Meta/Tactic/Refl.lean | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/Lean/Meta/Tactic/Refl.lean b/src/Lean/Meta/Tactic/Refl.lean
index 6ac24c8dfd..f40d595d4d 100644
--- a/src/Lean/Meta/Tactic/Refl.lean
+++ b/src/Lean/Meta/Tactic/Refl.lean
@@ -52,6 +52,14 @@ def _root_.Lean.MVarId.heqOfEq (mvarId : MVarId) : MetaM MVarId :=
     let some [mvarId] ← observing? do mvarId.apply (mkConst ``heq_of_eq [← mkFreshLevelMVar]) | return mvarId
     return mvarId
 
+/--
+Try to apply `eq_of_heq`. If successful, then return new goal, otherwise return `mvarId`.
+-/
+def _root_.Lean.MVarId.eqOfHEq (mvarId : MVarId) : MetaM MVarId :=
+  mvarId.withContext do
+    let some [mvarId] ← observing? do mvarId.apply (mkConst ``eq_of_heq [← mkFreshLevelMVar]) | return mvarId
+    return mvarId
+
 /--
 Close given goal using `HEq.refl`.
 -/