From 481532b778f02f51c5602a8f84b1cb98fed810f9 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Thu, 14 Mar 2024 12:18:18 +1100
Subject: [PATCH] chore: upstream the Mathlib component as well

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

diff --git a/src/Lean/Meta/Tactic/Rfl.lean b/src/Lean/Meta/Tactic/Rfl.lean
index 6522d0e315d9..48195183cabd 100644
--- a/src/Lean/Meta/Tactic/Rfl.lean
+++ b/src/Lean/Meta/Tactic/Rfl.lean
@@ -71,4 +71,33 @@ def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := do
   else
     throwError "rfl failed, no lemma with @[refl] applies"
 
+/-- Helper theorem for `Lean.MVarId.liftReflToEq`. -/
+private theorem rel_of_eq_and_refl {α : Sort _} {R : α → α → Prop}
+    {x y : α} (hxy : x = y) (h : R x x) : R x y :=
+  hxy ▸ h
+
+/--
+Convert a goal of the form `x ~ y` into the form `x = y`, where `~` is a reflexive
+relation, that is, a relation which has a reflexive lemma tagged with the attribute `[refl]`.
+If this can't be done, returns the original `MVarId`.
+-/
+def _root_.Lean.MVarId.liftReflToEq (mvarId : MVarId) : MetaM MVarId := do
+  mvarId.checkNotAssigned `liftReflToEq
+  let .app (.app rel _) _ ← withReducible mvarId.getType' | return mvarId
+  if rel.isAppOf `Eq then
+    -- No need to lift Eq to Eq
+    return mvarId
+  for lem in ← (reflExt.getState (← getEnv)).getMatch rel reflExt.config do
+    let res ← observing? do
+      -- First create an equality relating the LHS and RHS
+      -- and reduce the goal to proving that LHS is related to LHS.
+      let [mvarIdEq, mvarIdR] ← mvarId.apply (← mkConstWithFreshMVarLevels ``rel_of_eq_and_refl)
+        | failure
+      -- Then fill in the proof of the latter by reflexivity.
+      let [] ← mvarIdR.apply (← mkConstWithFreshMVarLevels lem) | failure
+      return mvarIdEq
+    if let some mvarIdEq := res then
+      return mvarIdEq
+  return mvarId
+
 end Lean.Meta.Rfl