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

@@ -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