[Merged by Bors] - chore: move liftReflToEq and rel_of_eq_and_refl from core

Mathlib/Tactic/CongrExclamation.lean

@@ -8,9 +8,9 @@ module
 public meta import Lean.Elab.ConfigEval
 public meta import Lean.Elab.Tactic.RCases
 public meta import Lean.Meta.Tactic.Assumption
-public meta import Lean.Meta.Tactic.Rfl
 
 public import Mathlib.Lean.Meta.CongrTheorems
+public import Mathlib.Tactic.Relation.Rfl
 public import Lean.Elab.ConfigEval
 public import Mathlib.Basic.Logic.Basic
 
@@ -95,7 +95,7 @@ public meta section
 
 universe u v
 
-open Lean Meta Elab Tactic
+open Lean Mathlib Meta Elab Tactic
 
 initialize registerTraceClass `congr!
 initialize registerTraceClass `congr!.synthesize
@@ -669,7 +669,7 @@ def Lean.MVarId.congrCore! (config : Congr!.Config) (mvarId : MVarId) :
   let s ← saveState
   /- We do `liftReflToEq` here rather than in `preCongr!` since we don't want to commit to it
      if there are no relevant congr lemmas. -/
-  let mvarId ← mvarId.liftReflToEq
+  let mvarId ← liftReflToEq mvarId
   for (passName, pass) in congrPasses! do
     try
       if let some mvarIds ← pass config mvarId then

Mathlib/Tactic/CongrM.lean

@@ -5,7 +5,7 @@ Authors: Moritz Doll, Gabriel Ebner, Damiano Testa, Kyle Miller
 -/
 module
 
-public meta import Lean.Meta.Tactic.Rfl
+public import Mathlib.Tactic.Relation.Rfl
 public import Mathlib.Tactic.TermCongr
 
 /-!
@@ -77,7 +77,7 @@ elab_rules : tactic
     trace[Tactic.congrm] "pattern: {pattern}"
     -- Chain together transformations as needed to convert the goal to an Eq if possible.
     liftMetaTactic fun g => do
-      return [← (← g.iffOfEq).liftReflToEq]
+      return [← liftReflToEq (← g.iffOfEq)]
     -- Apply `congr(...)`
     withMainContext do
       let gStx ← Term.exprToSyntax (← getMainTarget)

Mathlib/Tactic/Relation/Rfl.lean

@@ -9,19 +9,52 @@ public import Mathlib.Init
 public meta import Lean.Meta.Tactic.Rfl
 
 /-!
-# `Lean.MVarId.liftReflToEq`
+# `Mathlib.Tactic.liftReflToEq`
 
 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`.
 -/
 
-public meta section
-
 namespace Mathlib.Tactic
 
+public section
+
+/-- Helper theorem for `Mathlib.Tactic.liftReflToEq`. -/
+theorem rel_of_eq_and_refl {α : Sort*} {R : α → α → Prop}
+    {x y : α} (hxy : x = y) (h : R x x) : R x y :=
+  hxy ▸ h
+
+end
+
+public meta section
+
 open Lean Meta Elab Tactic Rfl
 
+/--
+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 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 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 ``Mathlib.Tactic.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
+
 /--
 This tactic applies to a goal whose target has the form `x ~ x`, where `~` is a reflexive
 relation, that is, a relation which has a reflexive lemma tagged with the attribute `@[refl]`.
@@ -46,4 +79,6 @@ def _root_.Lean.Expr.relSidesIfRefl? (e : Expr) : MetaM (Option (Name × Expr ×
       | none => return none
   return none
 
+end
+
 end Mathlib.Tactic