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`.
 -/