From b4caee80a3dfc5c9619d88b16c40cc3db90da4e2 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Wed, 27 Mar 2024 14:02:30 +1100
Subject: [PATCH] chore: rw? uses MVarId.refl not MVarId.applyRfl (#3783)

I think this was in error in my original Mathlib implementation. We're
not interested in relations other than `=`, so there is no point uses
`MVarId.applyRfl`, which just looks up `@[refl]` tagged lemmas and tries
those.

In a separate PR, I will change `MVarId.applyRfl` so it has a flag to
control whether on `=` it should just hand-off to `MVarId.refl`, or
fail. Failure is appropriate in the version we call from the `rfl`
macro, to avoid doing a double `IsDefEq` check on every `rfl`!
---
 src/Lean/Meta/Tactic/Rewrites.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Rewrites.lean b/src/Lean/Meta/Tactic/Rewrites.lean
index 7167412b94..68b873533d 100644
--- a/src/Lean/Meta/Tactic/Rewrites.lean
+++ b/src/Lean/Meta/Tactic/Rewrites.lean
@@ -7,7 +7,7 @@ prelude
 import Lean.Meta.LazyDiscrTree
 import Lean.Meta.Tactic.Assumption
 import Lean.Meta.Tactic.Rewrite
-import Lean.Meta.Tactic.Rfl
+import Lean.Meta.Tactic.Refl
 import Lean.Meta.Tactic.SolveByElim
 import Lean.Meta.Tactic.TryThis
 import Lean.Util.Heartbeats
@@ -149,7 +149,7 @@ def dischargableWithRfl? (mctx : MetavarContext) (e : Expr) : MetaM Bool := do
   try
     withoutModifyingState <| withMCtx mctx do
       -- We use `withReducible` here to follow the behaviour of `rw`.
-      withReducible (← mkFreshExprMVar e).mvarId!.applyRfl
+      withReducible (← mkFreshExprMVar e).mvarId!.refl
       pure true
   catch _e =>
     pure false