From dc519ea1304950d9369c967cca251cccebb36611 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Tue, 19 Mar 2024 10:19:57 +0100
Subject: [PATCH 01/16] feat: apply_rfl tactic: Handle Eq, HEq, better error
 messages

this implements the first half of #3302: It improves the extensible
`rfl` tactic (the one that looks at `refl` attributes) to

* Check itself that the lhs and rhs are defEq, and give a nice
  consistent error message when they don't (instead of just passing on
  the less helpful error message from `apply Foo.refl`)
* Also handle `Eq` and `HEq` (built in) and `Iff` (using the attribute)

Care ist taken that, as before, the transparency setting affects
comparing the lhs and rhs, but not the reduction of the relation

A test file checks the various failure modes and error messages.

I believe this `apply_rfl` can serve as the only implementation of
`rfl`, which would then complete #3302, but that seems to require a
non-trivial bootstrapping dance, so maybe better done separately.
---
 src/Init/Core.lean                           |   1 +
 src/Lean/Meta/Tactic/Refl.lean               |   3 +
 src/Lean/Meta/Tactic/Rfl.lean                |  75 ++++++---
 tests/lean/rflTacticErrors.lean              | 118 ++++++++++++++
 tests/lean/rflTacticErrors.lean.expected.out | 163 +++++++++++++++++++
 5 files changed, 340 insertions(+), 20 deletions(-)
 create mode 100644 tests/lean/rflTacticErrors.lean
 create mode 100644 tests/lean/rflTacticErrors.lean.expected.out

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index d27672e92788..c0b28fa9f405 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -788,6 +788,7 @@ variable {a b c d : Prop}
 theorem iff_iff_implies_and_implies (a b : Prop) : (a ↔ b) ↔ (a → b) ∧ (b → a) :=
   Iff.intro (fun h => And.intro h.mp h.mpr) (fun h => Iff.intro h.left h.right)
 
+@[refl]
 theorem Iff.refl (a : Prop) : a ↔ a :=
   Iff.intro (fun h => h) (fun h => h)
 
diff --git a/src/Lean/Meta/Tactic/Refl.lean b/src/Lean/Meta/Tactic/Refl.lean
index 13c61a18812e..4ff779754639 100644
--- a/src/Lean/Meta/Tactic/Refl.lean
+++ b/src/Lean/Meta/Tactic/Refl.lean
@@ -18,6 +18,9 @@ private def useKernel (lhs rhs : Expr) : MetaM Bool := do
 
 /--
 Close given goal using `Eq.refl`.
+
+See `Lean.MVarId.applyRfl` for the variant that also consults `@[refl]` lemmas, and which
+backs the `rfl` tactic.
 -/
 def _root_.Lean.MVarId.refl (mvarId : MVarId) : MetaM Unit := do
   mvarId.withContext do
diff --git a/src/Lean/Meta/Tactic/Rfl.lean b/src/Lean/Meta/Tactic/Rfl.lean
index 48195183cabd..3272c807abc4 100644
--- a/src/Lean/Meta/Tactic/Rfl.lean
+++ b/src/Lean/Meta/Tactic/Rfl.lean
@@ -45,31 +45,66 @@ initialize registerBuiltinAttribute {
 
 open Elab Tactic
 
+private def useKernel (lhs rhs : Expr) : MetaM Bool := do
+  if lhs.hasFVar || lhs.hasMVar || rhs.hasFVar || rhs.hasMVar then
+    return false
+  else
+    return (← getTransparency) matches TransparencyMode.default | TransparencyMode.all
+
 /-- `MetaM` version of the `rfl` tactic.
 
 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].
+relation, that is, equality or another relation which has a reflexive lemma tagged with the
+attribute [refl].
 -/
-def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := do
-  let .app (.app rel _) _ ← whnfR <|← instantiateMVars <|← goal.getType
-    | throwError "reflexivity lemmas only apply to binary relations, not{
-        indentExpr (← goal.getType)}"
-  let s ← saveState
-  let mut ex? := none
-  for lem in ← (reflExt.getState (← getEnv)).getMatch rel reflExt.config do
-    try
-      let gs ← goal.apply (← mkConstWithFreshMVarLevels lem)
-      if gs.isEmpty then return () else
-        logError <| MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{
-          goalsToMessageData gs}"
-    catch e =>
-      ex? := ex? <|> (some (← saveState, e)) -- stash the first failure of `apply`
-    s.restore
-  if let some (sErr, e) := ex? then
-    sErr.restore
-    throw e
+def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := goal.withContext do
+  -- NB: uses whnfR, we do not want to unfold the relation itself
+  let t ← whnfR <|← instantiateMVars <|← goal.getType
+  if t.getAppNumArgs < 2 then
+    throwError "rfl can only be used on binary relations, not{indentExpr (← goal.getType)}"
+
+  -- Special case HEq here as it has a different argument order.
+  if t.isAppOfArity ``HEq 4 then
+    let gs ← goal.applyConst ``HEq.refl
+    unless gs.isEmpty do
+      throwError MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{
+        goalsToMessageData gs}"
+    return
+
+  let rel := t.appFn!.appFn!
+  let lhs := t.appFn!.appArg!
+  let rhs := t.appArg!
+
+  let success ← if (← useKernel lhs rhs) then
+    ofExceptKernelException (Kernel.isDefEq (← getEnv) {} lhs rhs)
+  else
+    isDefEq lhs rhs
+  unless success do
+    throwTacticEx `rfl goal m!"The lhs{indentExpr lhs}\nis not definitionally equal to rhs{indentExpr rhs}"
+
+  if rel.isAppOfArity `Eq 1 then
+    -- The common case is equality: just use `Eq.refl`
+    let us := rel.appFn!.constLevels!
+    let α :=  rel.appArg!
+    goal.assign (mkApp2 (mkConst ``Eq.refl us) α lhs)
   else
-    throwError "rfl failed, no lemma with @[refl] applies"
+    -- Else search through `@refl` keyed by the relation
+    let s ← saveState
+    let mut ex? := none
+    for lem in ← (reflExt.getState (← getEnv)).getMatch rel reflExt.config do
+      try
+        let gs ← goal.apply (← mkConstWithFreshMVarLevels lem)
+        if gs.isEmpty then return () else
+          throwError MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{
+            goalsToMessageData gs}"
+      catch e =>
+        ex? := ex? <|> (some (← saveState, e)) -- stash the first failure of `apply`
+      s.restore
+    if let some (sErr, e) := ex? then
+      sErr.restore
+      throw e
+    else
+      throwError "rfl failed, no @[refl] lemma registered for relation{indentExpr rel}"
 
 /-- Helper theorem for `Lean.MVarId.liftReflToEq`. -/
 private theorem rel_of_eq_and_refl {α : Sort _} {R : α → α → Prop}
diff --git a/tests/lean/rflTacticErrors.lean b/tests/lean/rflTacticErrors.lean
new file mode 100644
index 000000000000..c94f0ca74a41
--- /dev/null
+++ b/tests/lean/rflTacticErrors.lean
@@ -0,0 +1,118 @@
+
+/-!
+This file tests the `rfl` tactic:
+ * Extensibility
+ * Error messages
+ * Effect of `with_reducible`
+-/
+
+-- Remove the following once `apply_rfl` and `rfl` are merged
+-- Until then: Note the horrible error message!
+example : false = true   := by rfl
+
+-- Setup
+
+inductive P : α → α → Prop where | refl : P a a
+attribute [refl] P.refl
+
+-- Defeq to relation `P` at reducible transparency
+abbrev Q : α → α → Prop := P
+-- Defeq to relation `P` at default transparency
+def Q' : α → α → Prop := P
+
+-- No refl attribute
+inductive R : α → α → Prop where | refl : R a a
+
+-- Syntactic equal
+
+example : true = true   := by apply_rfl
+example : HEq true true := by apply_rfl
+example : True ↔ True   := by apply_rfl
+example : P true true   := by apply_rfl
+example : Q true true   := by apply_rfl
+example : Q' true true  := by apply_rfl -- Error
+example : R true true   := by apply_rfl -- Error
+
+example : true = true   := by with_reducible apply_rfl
+example : HEq true true := by with_reducible apply_rfl
+example : True ↔ True   := by with_reducible apply_rfl
+example : P true true   := by with_reducible apply_rfl
+example : Q true true   := by with_reducible apply_rfl
+example : Q' true true  := by with_reducible apply_rfl -- Error
+example : R true true   := by with_reducible apply_rfl -- Error
+
+-- Reducibly equal
+
+abbrev true' := true
+abbrev True' := True
+
+example : true' = true   := by apply_rfl
+example : HEq true' true := by apply_rfl
+example : True' ↔ True   := by apply_rfl
+example : P true' true   := by apply_rfl
+example : Q true' true   := by apply_rfl
+example : Q' true' true  := by apply_rfl -- Error
+example : R true' true   := by apply_rfl -- Error
+
+example : true' = true   := by with_reducible apply_rfl
+example : HEq true' true := by with_reducible apply_rfl
+example : True' ↔ True   := by with_reducible apply_rfl
+example : P true' true   := by with_reducible apply_rfl
+example : Q true' true   := by with_reducible apply_rfl -- NB: No error!
+example : Q' true' true  := by with_reducible apply_rfl -- Error
+example : R true' true   := by with_reducible apply_rfl -- Error
+
+-- Equal at default transparency only
+
+def true'' := true
+def True'' := True
+
+example : true'' = true   := by apply_rfl
+example : HEq true'' true := by apply_rfl
+example : True'' ↔ True   := by apply_rfl
+example : P true'' true   := by apply_rfl
+example : Q true'' true   := by apply_rfl
+example : Q' true'' true  := by apply_rfl -- Error
+example : R true'' true   := by apply_rfl -- Error
+
+example : true'' = true   := by with_reducible apply_rfl -- Error
+example : HEq true'' true := by with_reducible apply_rfl -- Error
+example : True'' ↔ True   := by with_reducible apply_rfl -- Error
+example : P true'' true   := by with_reducible apply_rfl -- Error
+example : Q true'' true   := by with_reducible apply_rfl -- Error
+example : Q' true'' true  := by with_reducible apply_rfl -- Error
+example : R true'' true   := by with_reducible apply_rfl -- Error
+
+-- Unequal
+example : false = true   := by apply_rfl -- Error
+example : HEq false true := by apply_rfl -- Error
+example : False ↔ True   := by apply_rfl -- Error
+example : P false true   := by apply_rfl -- Error
+example : Q false true   := by apply_rfl -- Error
+example : Q' false true  := by apply_rfl -- Error
+example : R false true   := by apply_rfl -- Error
+
+example : false = true   := by with_reducible apply_rfl -- Error
+example : HEq false true := by with_reducible apply_rfl -- Error
+example : False ↔ True   := by with_reducible apply_rfl -- Error
+example : P false true   := by with_reducible apply_rfl -- Error
+example : Q false true   := by with_reducible apply_rfl -- Error
+example : Q' false true  := by with_reducible apply_rfl -- Error
+example : R false true   := by with_reducible apply_rfl -- Error
+
+-- Inheterogeneous unequal
+
+example : HEq true 1 := by apply_rfl -- Error
+example : HEq true 1 := by with_reducible apply_rfl -- Error
+
+-- Rfl lemma with side condition:
+-- Error message should show left-over goal
+
+inductive S : Bool → Bool → Prop where | refl : a = true → S a a
+attribute [refl] S.refl
+example : S true false  := by apply_rfl -- Error
+example : S true false  := by with_reducible apply_rfl -- Error
+example : S true true   := by apply_rfl -- Error (left-over goal)
+example : S true true   := by with_reducible apply_rfl -- Error (left-over goal)
+example : S false false := by apply_rfl -- Error (left-over goal)
+example : S false false := by with_reducible apply_rfl -- Error (left-over goal)
diff --git a/tests/lean/rflTacticErrors.lean.expected.out b/tests/lean/rflTacticErrors.lean.expected.out
new file mode 100644
index 000000000000..1173bdfb74d6
--- /dev/null
+++ b/tests/lean/rflTacticErrors.lean.expected.out
@@ -0,0 +1,163 @@
+rflTacticErrors.lean:11:31-11:34: error: type mismatch
+  Iff.rfl
+has type
+  ?m ↔ ?m : Prop
+but is expected to have type
+  false = true : Prop
+rflTacticErrors.lean:33:30-33:39: error: rfl failed, no @[refl] lemma registered for relation
+  Q'
+rflTacticErrors.lean:34:30-34:39: error: rfl failed, no @[refl] lemma registered for relation
+  R
+rflTacticErrors.lean:41:45-41:54: error: rfl failed, no @[refl] lemma registered for relation
+  Q'
+rflTacticErrors.lean:42:45-42:54: error: rfl failed, no @[refl] lemma registered for relation
+  R
+rflTacticErrors.lean:54:31-54:40: error: rfl failed, no @[refl] lemma registered for relation
+  Q'
+rflTacticErrors.lean:55:31-55:40: error: rfl failed, no @[refl] lemma registered for relation
+  R
+rflTacticErrors.lean:62:46-62:55: error: rfl failed, no @[refl] lemma registered for relation
+  Q'
+rflTacticErrors.lean:63:46-63:55: error: rfl failed, no @[refl] lemma registered for relation
+  R
+rflTacticErrors.lean:75:32-75:41: error: rfl failed, no @[refl] lemma registered for relation
+  Q'
+rflTacticErrors.lean:76:32-76:41: error: rfl failed, no @[refl] lemma registered for relation
+  R
+rflTacticErrors.lean:78:47-78:56: error: tactic 'rfl' failed, The lhs
+  true''
+is not definitionally equal to rhs
+  true
+⊢ true'' = true
+rflTacticErrors.lean:79:47-79:56: error: tactic 'apply' failed, failed to unify
+  HEq ?a ?a
+with
+  HEq true'' true
+⊢ HEq true'' true
+rflTacticErrors.lean:80:47-80:56: error: tactic 'rfl' failed, The lhs
+  True''
+is not definitionally equal to rhs
+  True
+⊢ True'' ↔ True
+rflTacticErrors.lean:81:47-81:56: error: tactic 'rfl' failed, The lhs
+  true''
+is not definitionally equal to rhs
+  true
+⊢ P true'' true
+rflTacticErrors.lean:82:47-82:56: error: tactic 'rfl' failed, The lhs
+  true''
+is not definitionally equal to rhs
+  true
+⊢ Q true'' true
+rflTacticErrors.lean:83:47-83:56: error: tactic 'rfl' failed, The lhs
+  true''
+is not definitionally equal to rhs
+  true
+⊢ Q' true'' true
+rflTacticErrors.lean:84:47-84:56: error: tactic 'rfl' failed, The lhs
+  true''
+is not definitionally equal to rhs
+  true
+⊢ R true'' true
+rflTacticErrors.lean:87:31-87:40: error: tactic 'rfl' failed, The lhs
+  false
+is not definitionally equal to rhs
+  true
+⊢ false = true
+rflTacticErrors.lean:88:31-88:40: error: tactic 'apply' failed, failed to unify
+  HEq ?a ?a
+with
+  HEq false true
+⊢ HEq false true
+rflTacticErrors.lean:89:31-89:40: error: tactic 'rfl' failed, The lhs
+  False
+is not definitionally equal to rhs
+  True
+⊢ False ↔ True
+rflTacticErrors.lean:90:31-90:40: error: tactic 'rfl' failed, The lhs
+  false
+is not definitionally equal to rhs
+  true
+⊢ P false true
+rflTacticErrors.lean:91:31-91:40: error: tactic 'rfl' failed, The lhs
+  false
+is not definitionally equal to rhs
+  true
+⊢ Q false true
+rflTacticErrors.lean:92:31-92:40: error: tactic 'rfl' failed, The lhs
+  false
+is not definitionally equal to rhs
+  true
+⊢ Q' false true
+rflTacticErrors.lean:93:31-93:40: error: tactic 'rfl' failed, The lhs
+  false
+is not definitionally equal to rhs
+  true
+⊢ R false true
+rflTacticErrors.lean:95:46-95:55: error: tactic 'rfl' failed, The lhs
+  false
+is not definitionally equal to rhs
+  true
+⊢ false = true
+rflTacticErrors.lean:96:46-96:55: error: tactic 'apply' failed, failed to unify
+  HEq ?a ?a
+with
+  HEq false true
+⊢ HEq false true
+rflTacticErrors.lean:97:46-97:55: error: tactic 'rfl' failed, The lhs
+  False
+is not definitionally equal to rhs
+  True
+⊢ False ↔ True
+rflTacticErrors.lean:98:46-98:55: error: tactic 'rfl' failed, The lhs
+  false
+is not definitionally equal to rhs
+  true
+⊢ P false true
+rflTacticErrors.lean:99:46-99:55: error: tactic 'rfl' failed, The lhs
+  false
+is not definitionally equal to rhs
+  true
+⊢ Q false true
+rflTacticErrors.lean:100:46-100:55: error: tactic 'rfl' failed, The lhs
+  false
+is not definitionally equal to rhs
+  true
+⊢ Q' false true
+rflTacticErrors.lean:101:46-101:55: error: tactic 'rfl' failed, The lhs
+  false
+is not definitionally equal to rhs
+  true
+⊢ R false true
+rflTacticErrors.lean:105:27-105:36: error: tactic 'apply' failed, failed to unify
+  HEq ?a ?a
+with
+  HEq true 1
+⊢ HEq true 1
+rflTacticErrors.lean:106:42-106:51: error: tactic 'apply' failed, failed to unify
+  HEq ?a ?a
+with
+  HEq true 1
+⊢ HEq true 1
+rflTacticErrors.lean:113:30-113:39: error: tactic 'rfl' failed, The lhs
+  true
+is not definitionally equal to rhs
+  false
+⊢ S true false
+rflTacticErrors.lean:114:45-114:54: error: tactic 'rfl' failed, The lhs
+  true
+is not definitionally equal to rhs
+  false
+⊢ S true false
+rflTacticErrors.lean:115:30-115:39: error: unsolved goals
+case a
+⊢ true = true
+rflTacticErrors.lean:116:45-116:54: error: unsolved goals
+case a
+⊢ true = true
+rflTacticErrors.lean:117:30-117:39: error: unsolved goals
+case a
+⊢ false = true
+rflTacticErrors.lean:118:45-118:54: error: unsolved goals
+case a
+⊢ false = true

From 0dd354faa64afabaa5a6f0f80c5c7a2cdc5765a7 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Tue, 19 Mar 2024 13:22:36 +0100
Subject: [PATCH 02/16] Update src/Lean/Meta/Tactic/Rfl.lean

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

diff --git a/src/Lean/Meta/Tactic/Rfl.lean b/src/Lean/Meta/Tactic/Rfl.lean
index 3272c807abc4..724adefe37b0 100644
--- a/src/Lean/Meta/Tactic/Rfl.lean
+++ b/src/Lean/Meta/Tactic/Rfl.lean
@@ -98,7 +98,8 @@ def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := goal.withContext
           throwError MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{
             goalsToMessageData gs}"
       catch e =>
-        ex? := ex? <|> (some (← saveState, e)) -- stash the first failure of `apply`
+        unless ex2.isSome do
+          ex? := some (← saveState, e) -- stash the first failure of `apply`
       s.restore
     if let some (sErr, e) := ex? then
       sErr.restore

From 3cbfc4270b1a645ff7cfb0d19fb0cee54542c1b1 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Tue, 19 Mar 2024 13:27:44 +0100
Subject: [PATCH 03/16] Update Rfl.lean

---
 src/Lean/Meta/Tactic/Rfl.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Meta/Tactic/Rfl.lean b/src/Lean/Meta/Tactic/Rfl.lean
index 724adefe37b0..f164dcd6b0b6 100644
--- a/src/Lean/Meta/Tactic/Rfl.lean
+++ b/src/Lean/Meta/Tactic/Rfl.lean
@@ -98,7 +98,7 @@ def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := goal.withContext
           throwError MessageData.tagged `Tactic.unsolvedGoals <| m!"unsolved goals\n{
             goalsToMessageData gs}"
       catch e =>
-        unless ex2.isSome do
+        unless ex?.isSome do
           ex? := some (← saveState, e) -- stash the first failure of `apply`
       s.restore
     if let some (sErr, e) := ex? then

From 925b3e5c80b7a119dcd51f3f63560a6375f1aa64 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Tue, 10 Sep 2024 09:53:45 +0200
Subject: [PATCH 04/16] Update test output

---
 tests/lean/rflTacticErrors.lean.expected.out | 16 ++++++++--------
 tests/lean/run/variable.lean                 |  3 ++-
 2 files changed, 10 insertions(+), 9 deletions(-)

diff --git a/tests/lean/rflTacticErrors.lean.expected.out b/tests/lean/rflTacticErrors.lean.expected.out
index 1173bdfb74d6..43eecb8308d5 100644
--- a/tests/lean/rflTacticErrors.lean.expected.out
+++ b/tests/lean/rflTacticErrors.lean.expected.out
@@ -1,9 +1,9 @@
-rflTacticErrors.lean:11:31-11:34: error: type mismatch
-  Iff.rfl
-has type
-  ?m ↔ ?m : Prop
-but is expected to have type
-  false = true : Prop
+rflTacticErrors.lean:11:31-11:34: error: The rfl tactic failed. Possible reasons:
+- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
+- The arguments of the relation are not equal.
+Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
+`exact HEq.rfl` etc.
+⊢ false = true
 rflTacticErrors.lean:33:30-33:39: error: rfl failed, no @[refl] lemma registered for relation
   Q'
 rflTacticErrors.lean:34:30-34:39: error: rfl failed, no @[refl] lemma registered for relation
@@ -30,9 +30,9 @@ is not definitionally equal to rhs
   true
 ⊢ true'' = true
 rflTacticErrors.lean:79:47-79:56: error: tactic 'apply' failed, failed to unify
-  HEq ?a ?a
+  @HEq ?α ?a ?α ?a
 with
-  HEq true'' true
+  @HEq Bool true'' Bool true
 ⊢ HEq true'' true
 rflTacticErrors.lean:80:47-80:56: error: tactic 'rfl' failed, The lhs
   True''
diff --git a/tests/lean/run/variable.lean b/tests/lean/run/variable.lean
index d0bead75f48d..41fe2acb0899 100644
--- a/tests/lean/run/variable.lean
+++ b/tests/lean/run/variable.lean
@@ -138,6 +138,7 @@ variable [ToString α] in
 omit [ToString α] in
 theorem t13 (a : α) : toString a = toString a := rfl
 
+set_option pp.mvars false in
 /--
 error: application type mismatch
   ToString True
@@ -146,7 +147,7 @@ argument
 has type
   Prop : Type
 but is expected to have type
-  Type ?u.1758 : Type (?u.1758 + 1)
+  Type _ : Type (_ + 1)
 -/
 #guard_msgs in
 omit [ToString True]

From e752769bbfa70cb5817ad80e6b9844d71964964b Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Tue, 10 Sep 2024 10:01:19 +0200
Subject: [PATCH 05/16] Move to tests/run

---
 tests/lean/rflTacticErrors.lean              | 118 ------
 tests/lean/rflTacticErrors.lean.expected.out | 163 --------
 tests/lean/run/rflTacticErrors.lean          | 397 +++++++++++++++++++
 3 files changed, 397 insertions(+), 281 deletions(-)
 delete mode 100644 tests/lean/rflTacticErrors.lean
 delete mode 100644 tests/lean/rflTacticErrors.lean.expected.out
 create mode 100644 tests/lean/run/rflTacticErrors.lean

diff --git a/tests/lean/rflTacticErrors.lean b/tests/lean/rflTacticErrors.lean
deleted file mode 100644
index c94f0ca74a41..000000000000
--- a/tests/lean/rflTacticErrors.lean
+++ /dev/null
@@ -1,118 +0,0 @@
-
-/-!
-This file tests the `rfl` tactic:
- * Extensibility
- * Error messages
- * Effect of `with_reducible`
--/
-
--- Remove the following once `apply_rfl` and `rfl` are merged
--- Until then: Note the horrible error message!
-example : false = true   := by rfl
-
--- Setup
-
-inductive P : α → α → Prop where | refl : P a a
-attribute [refl] P.refl
-
--- Defeq to relation `P` at reducible transparency
-abbrev Q : α → α → Prop := P
--- Defeq to relation `P` at default transparency
-def Q' : α → α → Prop := P
-
--- No refl attribute
-inductive R : α → α → Prop where | refl : R a a
-
--- Syntactic equal
-
-example : true = true   := by apply_rfl
-example : HEq true true := by apply_rfl
-example : True ↔ True   := by apply_rfl
-example : P true true   := by apply_rfl
-example : Q true true   := by apply_rfl
-example : Q' true true  := by apply_rfl -- Error
-example : R true true   := by apply_rfl -- Error
-
-example : true = true   := by with_reducible apply_rfl
-example : HEq true true := by with_reducible apply_rfl
-example : True ↔ True   := by with_reducible apply_rfl
-example : P true true   := by with_reducible apply_rfl
-example : Q true true   := by with_reducible apply_rfl
-example : Q' true true  := by with_reducible apply_rfl -- Error
-example : R true true   := by with_reducible apply_rfl -- Error
-
--- Reducibly equal
-
-abbrev true' := true
-abbrev True' := True
-
-example : true' = true   := by apply_rfl
-example : HEq true' true := by apply_rfl
-example : True' ↔ True   := by apply_rfl
-example : P true' true   := by apply_rfl
-example : Q true' true   := by apply_rfl
-example : Q' true' true  := by apply_rfl -- Error
-example : R true' true   := by apply_rfl -- Error
-
-example : true' = true   := by with_reducible apply_rfl
-example : HEq true' true := by with_reducible apply_rfl
-example : True' ↔ True   := by with_reducible apply_rfl
-example : P true' true   := by with_reducible apply_rfl
-example : Q true' true   := by with_reducible apply_rfl -- NB: No error!
-example : Q' true' true  := by with_reducible apply_rfl -- Error
-example : R true' true   := by with_reducible apply_rfl -- Error
-
--- Equal at default transparency only
-
-def true'' := true
-def True'' := True
-
-example : true'' = true   := by apply_rfl
-example : HEq true'' true := by apply_rfl
-example : True'' ↔ True   := by apply_rfl
-example : P true'' true   := by apply_rfl
-example : Q true'' true   := by apply_rfl
-example : Q' true'' true  := by apply_rfl -- Error
-example : R true'' true   := by apply_rfl -- Error
-
-example : true'' = true   := by with_reducible apply_rfl -- Error
-example : HEq true'' true := by with_reducible apply_rfl -- Error
-example : True'' ↔ True   := by with_reducible apply_rfl -- Error
-example : P true'' true   := by with_reducible apply_rfl -- Error
-example : Q true'' true   := by with_reducible apply_rfl -- Error
-example : Q' true'' true  := by with_reducible apply_rfl -- Error
-example : R true'' true   := by with_reducible apply_rfl -- Error
-
--- Unequal
-example : false = true   := by apply_rfl -- Error
-example : HEq false true := by apply_rfl -- Error
-example : False ↔ True   := by apply_rfl -- Error
-example : P false true   := by apply_rfl -- Error
-example : Q false true   := by apply_rfl -- Error
-example : Q' false true  := by apply_rfl -- Error
-example : R false true   := by apply_rfl -- Error
-
-example : false = true   := by with_reducible apply_rfl -- Error
-example : HEq false true := by with_reducible apply_rfl -- Error
-example : False ↔ True   := by with_reducible apply_rfl -- Error
-example : P false true   := by with_reducible apply_rfl -- Error
-example : Q false true   := by with_reducible apply_rfl -- Error
-example : Q' false true  := by with_reducible apply_rfl -- Error
-example : R false true   := by with_reducible apply_rfl -- Error
-
--- Inheterogeneous unequal
-
-example : HEq true 1 := by apply_rfl -- Error
-example : HEq true 1 := by with_reducible apply_rfl -- Error
-
--- Rfl lemma with side condition:
--- Error message should show left-over goal
-
-inductive S : Bool → Bool → Prop where | refl : a = true → S a a
-attribute [refl] S.refl
-example : S true false  := by apply_rfl -- Error
-example : S true false  := by with_reducible apply_rfl -- Error
-example : S true true   := by apply_rfl -- Error (left-over goal)
-example : S true true   := by with_reducible apply_rfl -- Error (left-over goal)
-example : S false false := by apply_rfl -- Error (left-over goal)
-example : S false false := by with_reducible apply_rfl -- Error (left-over goal)
diff --git a/tests/lean/rflTacticErrors.lean.expected.out b/tests/lean/rflTacticErrors.lean.expected.out
deleted file mode 100644
index 43eecb8308d5..000000000000
--- a/tests/lean/rflTacticErrors.lean.expected.out
+++ /dev/null
@@ -1,163 +0,0 @@
-rflTacticErrors.lean:11:31-11:34: error: The rfl tactic failed. Possible reasons:
-- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
-- The arguments of the relation are not equal.
-Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
-`exact HEq.rfl` etc.
-⊢ false = true
-rflTacticErrors.lean:33:30-33:39: error: rfl failed, no @[refl] lemma registered for relation
-  Q'
-rflTacticErrors.lean:34:30-34:39: error: rfl failed, no @[refl] lemma registered for relation
-  R
-rflTacticErrors.lean:41:45-41:54: error: rfl failed, no @[refl] lemma registered for relation
-  Q'
-rflTacticErrors.lean:42:45-42:54: error: rfl failed, no @[refl] lemma registered for relation
-  R
-rflTacticErrors.lean:54:31-54:40: error: rfl failed, no @[refl] lemma registered for relation
-  Q'
-rflTacticErrors.lean:55:31-55:40: error: rfl failed, no @[refl] lemma registered for relation
-  R
-rflTacticErrors.lean:62:46-62:55: error: rfl failed, no @[refl] lemma registered for relation
-  Q'
-rflTacticErrors.lean:63:46-63:55: error: rfl failed, no @[refl] lemma registered for relation
-  R
-rflTacticErrors.lean:75:32-75:41: error: rfl failed, no @[refl] lemma registered for relation
-  Q'
-rflTacticErrors.lean:76:32-76:41: error: rfl failed, no @[refl] lemma registered for relation
-  R
-rflTacticErrors.lean:78:47-78:56: error: tactic 'rfl' failed, The lhs
-  true''
-is not definitionally equal to rhs
-  true
-⊢ true'' = true
-rflTacticErrors.lean:79:47-79:56: error: tactic 'apply' failed, failed to unify
-  @HEq ?α ?a ?α ?a
-with
-  @HEq Bool true'' Bool true
-⊢ HEq true'' true
-rflTacticErrors.lean:80:47-80:56: error: tactic 'rfl' failed, The lhs
-  True''
-is not definitionally equal to rhs
-  True
-⊢ True'' ↔ True
-rflTacticErrors.lean:81:47-81:56: error: tactic 'rfl' failed, The lhs
-  true''
-is not definitionally equal to rhs
-  true
-⊢ P true'' true
-rflTacticErrors.lean:82:47-82:56: error: tactic 'rfl' failed, The lhs
-  true''
-is not definitionally equal to rhs
-  true
-⊢ Q true'' true
-rflTacticErrors.lean:83:47-83:56: error: tactic 'rfl' failed, The lhs
-  true''
-is not definitionally equal to rhs
-  true
-⊢ Q' true'' true
-rflTacticErrors.lean:84:47-84:56: error: tactic 'rfl' failed, The lhs
-  true''
-is not definitionally equal to rhs
-  true
-⊢ R true'' true
-rflTacticErrors.lean:87:31-87:40: error: tactic 'rfl' failed, The lhs
-  false
-is not definitionally equal to rhs
-  true
-⊢ false = true
-rflTacticErrors.lean:88:31-88:40: error: tactic 'apply' failed, failed to unify
-  HEq ?a ?a
-with
-  HEq false true
-⊢ HEq false true
-rflTacticErrors.lean:89:31-89:40: error: tactic 'rfl' failed, The lhs
-  False
-is not definitionally equal to rhs
-  True
-⊢ False ↔ True
-rflTacticErrors.lean:90:31-90:40: error: tactic 'rfl' failed, The lhs
-  false
-is not definitionally equal to rhs
-  true
-⊢ P false true
-rflTacticErrors.lean:91:31-91:40: error: tactic 'rfl' failed, The lhs
-  false
-is not definitionally equal to rhs
-  true
-⊢ Q false true
-rflTacticErrors.lean:92:31-92:40: error: tactic 'rfl' failed, The lhs
-  false
-is not definitionally equal to rhs
-  true
-⊢ Q' false true
-rflTacticErrors.lean:93:31-93:40: error: tactic 'rfl' failed, The lhs
-  false
-is not definitionally equal to rhs
-  true
-⊢ R false true
-rflTacticErrors.lean:95:46-95:55: error: tactic 'rfl' failed, The lhs
-  false
-is not definitionally equal to rhs
-  true
-⊢ false = true
-rflTacticErrors.lean:96:46-96:55: error: tactic 'apply' failed, failed to unify
-  HEq ?a ?a
-with
-  HEq false true
-⊢ HEq false true
-rflTacticErrors.lean:97:46-97:55: error: tactic 'rfl' failed, The lhs
-  False
-is not definitionally equal to rhs
-  True
-⊢ False ↔ True
-rflTacticErrors.lean:98:46-98:55: error: tactic 'rfl' failed, The lhs
-  false
-is not definitionally equal to rhs
-  true
-⊢ P false true
-rflTacticErrors.lean:99:46-99:55: error: tactic 'rfl' failed, The lhs
-  false
-is not definitionally equal to rhs
-  true
-⊢ Q false true
-rflTacticErrors.lean:100:46-100:55: error: tactic 'rfl' failed, The lhs
-  false
-is not definitionally equal to rhs
-  true
-⊢ Q' false true
-rflTacticErrors.lean:101:46-101:55: error: tactic 'rfl' failed, The lhs
-  false
-is not definitionally equal to rhs
-  true
-⊢ R false true
-rflTacticErrors.lean:105:27-105:36: error: tactic 'apply' failed, failed to unify
-  HEq ?a ?a
-with
-  HEq true 1
-⊢ HEq true 1
-rflTacticErrors.lean:106:42-106:51: error: tactic 'apply' failed, failed to unify
-  HEq ?a ?a
-with
-  HEq true 1
-⊢ HEq true 1
-rflTacticErrors.lean:113:30-113:39: error: tactic 'rfl' failed, The lhs
-  true
-is not definitionally equal to rhs
-  false
-⊢ S true false
-rflTacticErrors.lean:114:45-114:54: error: tactic 'rfl' failed, The lhs
-  true
-is not definitionally equal to rhs
-  false
-⊢ S true false
-rflTacticErrors.lean:115:30-115:39: error: unsolved goals
-case a
-⊢ true = true
-rflTacticErrors.lean:116:45-116:54: error: unsolved goals
-case a
-⊢ true = true
-rflTacticErrors.lean:117:30-117:39: error: unsolved goals
-case a
-⊢ false = true
-rflTacticErrors.lean:118:45-118:54: error: unsolved goals
-case a
-⊢ false = true
diff --git a/tests/lean/run/rflTacticErrors.lean b/tests/lean/run/rflTacticErrors.lean
new file mode 100644
index 000000000000..21e21760e04d
--- /dev/null
+++ b/tests/lean/run/rflTacticErrors.lean
@@ -0,0 +1,397 @@
+
+/-!
+This file tests the `rfl` tactic:
+ * Extensibility
+ * Error messages
+ * Effect of `with_reducible`
+-/
+
+/--
+error: The rfl tactic failed. Possible reasons:
+- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
+- The arguments of the relation are not equal.
+Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
+`exact HEq.rfl` etc.
+⊢ false = true
+-/
+#guard_msgs in
+example : false = true := by rfl
+
+-- Setup
+
+inductive P : α → α → Prop where | refl : P a a
+attribute [refl] P.refl
+
+-- Defeq to relation `P` at reducible transparency
+abbrev Q : α → α → Prop := P
+-- Defeq to relation `P` at default transparency
+def Q' : α → α → Prop := P
+
+-- No refl attribute
+inductive R : α → α → Prop where | refl : R a a
+
+-- Syntactic equal
+
+example : true = true   := by apply_rfl
+example : HEq true true := by apply_rfl
+example : True ↔ True   := by apply_rfl
+example : P true true   := by apply_rfl
+example : Q true true   := by apply_rfl
+/--
+error: rfl failed, no @[refl] lemma registered for relation
+  Q'
+-/
+#guard_msgs in example : Q' true true  := by apply_rfl -- Error
+/--
+error: rfl failed, no @[refl] lemma registered for relation
+  R
+-/
+#guard_msgs in example : R true true   := by apply_rfl -- Error
+
+example : true = true   := by with_reducible apply_rfl
+example : HEq true true := by with_reducible apply_rfl
+example : True ↔ True   := by with_reducible apply_rfl
+example : P true true   := by with_reducible apply_rfl
+example : Q true true   := by with_reducible apply_rfl
+/--
+error: rfl failed, no @[refl] lemma registered for relation
+  Q'
+-/
+#guard_msgs in
+example : Q' true true  := by with_reducible apply_rfl -- Error
+/--
+error: rfl failed, no @[refl] lemma registered for relation
+  R
+-/
+#guard_msgs in
+example : R true true   := by with_reducible apply_rfl -- Error
+
+-- Reducibly equal
+
+abbrev true' := true
+abbrev True' := True
+
+example : true' = true   := by apply_rfl
+example : HEq true' true := by apply_rfl
+example : True' ↔ True   := by apply_rfl
+example : P true' true   := by apply_rfl
+example : Q true' true   := by apply_rfl
+/--
+error: rfl failed, no @[refl] lemma registered for relation
+  Q'
+-/
+#guard_msgs in
+example : Q' true' true  := by apply_rfl -- Error
+/--
+error: rfl failed, no @[refl] lemma registered for relation
+  R
+-/
+#guard_msgs in
+example : R true' true   := by apply_rfl -- Error
+
+example : true' = true   := by with_reducible apply_rfl
+example : HEq true' true := by with_reducible apply_rfl
+example : True' ↔ True   := by with_reducible apply_rfl
+example : P true' true   := by with_reducible apply_rfl
+example : Q true' true   := by with_reducible apply_rfl -- NB: No error, Q and true' reducible
+/--
+error: rfl failed, no @[refl] lemma registered for relation
+  Q'
+-/
+#guard_msgs in
+example : Q' true' true  := by with_reducible apply_rfl -- Error
+/--
+error: rfl failed, no @[refl] lemma registered for relation
+  R
+-/
+#guard_msgs in
+example : R true' true   := by with_reducible apply_rfl -- Error
+
+-- Equal at default transparency only
+
+def true'' := true
+def True'' := True
+
+example : true'' = true   := by apply_rfl
+example : HEq true'' true := by apply_rfl
+example : True'' ↔ True   := by apply_rfl
+example : P true'' true   := by apply_rfl
+example : Q true'' true   := by apply_rfl
+/--
+error: rfl failed, no @[refl] lemma registered for relation
+  Q'
+-/
+#guard_msgs in
+example : Q' true'' true  := by apply_rfl -- Error
+/--
+error: rfl failed, no @[refl] lemma registered for relation
+  R
+-/
+#guard_msgs in
+example : R true'' true   := by apply_rfl -- Error
+
+/--
+error: tactic 'rfl' failed, The lhs
+  true''
+is not definitionally equal to rhs
+  true
+⊢ true'' = true
+-/
+#guard_msgs in
+example : true'' = true   := by with_reducible apply_rfl -- Error
+/--
+error: tactic 'apply' failed, failed to unify
+  @HEq ?α ?a ?α ?a
+with
+  @HEq Bool true'' Bool true
+⊢ HEq true'' true
+-/
+#guard_msgs in
+example : HEq true'' true := by with_reducible apply_rfl -- Error
+/--
+error: tactic 'rfl' failed, The lhs
+  True''
+is not definitionally equal to rhs
+  True
+⊢ True'' ↔ True
+-/
+#guard_msgs in
+example : True'' ↔ True   := by with_reducible apply_rfl -- Error
+/--
+error: tactic 'rfl' failed, The lhs
+  true''
+is not definitionally equal to rhs
+  true
+⊢ P true'' true
+-/
+#guard_msgs in
+example : P true'' true   := by with_reducible apply_rfl -- Error
+/--
+error: tactic 'rfl' failed, The lhs
+  true''
+is not definitionally equal to rhs
+  true
+⊢ Q true'' true
+-/
+#guard_msgs in
+example : Q true'' true   := by with_reducible apply_rfl -- Error
+/--
+error: tactic 'rfl' failed, The lhs
+  true''
+is not definitionally equal to rhs
+  true
+⊢ Q' true'' true
+-/
+#guard_msgs in
+example : Q' true'' true  := by with_reducible apply_rfl -- Error
+/--
+error: tactic 'rfl' failed, The lhs
+  true''
+is not definitionally equal to rhs
+  true
+⊢ R true'' true
+-/
+#guard_msgs in
+example : R true'' true   := by with_reducible apply_rfl -- Error
+
+-- Unequal
+/--
+error: tactic 'rfl' failed, The lhs
+  false
+is not definitionally equal to rhs
+  true
+⊢ false = true
+-/
+#guard_msgs in
+example : false = true   := by apply_rfl -- Error
+/--
+error: tactic 'apply' failed, failed to unify
+  HEq ?a ?a
+with
+  HEq false true
+⊢ HEq false true
+-/
+#guard_msgs in
+example : HEq false true := by apply_rfl -- Error
+/--
+error: tactic 'rfl' failed, The lhs
+  False
+is not definitionally equal to rhs
+  True
+⊢ False ↔ True
+-/
+#guard_msgs in
+example : False ↔ True   := by apply_rfl -- Error
+/--
+error: tactic 'rfl' failed, The lhs
+  false
+is not definitionally equal to rhs
+  true
+⊢ P false true
+-/
+#guard_msgs in
+example : P false true   := by apply_rfl -- Error
+/--
+error: tactic 'rfl' failed, The lhs
+  false
+is not definitionally equal to rhs
+  true
+⊢ Q false true
+-/
+#guard_msgs in
+example : Q false true   := by apply_rfl -- Error
+/--
+error: tactic 'rfl' failed, The lhs
+  false
+is not definitionally equal to rhs
+  true
+⊢ Q' false true
+-/
+#guard_msgs in
+example : Q' false true  := by apply_rfl -- Error
+/--
+error: tactic 'rfl' failed, The lhs
+  false
+is not definitionally equal to rhs
+  true
+⊢ R false true
+-/
+#guard_msgs in
+example : R false true   := by apply_rfl -- Error
+
+/--
+error: tactic 'rfl' failed, The lhs
+  false
+is not definitionally equal to rhs
+  true
+⊢ false = true
+-/
+#guard_msgs in
+example : false = true   := by with_reducible apply_rfl -- Error
+/--
+error: tactic 'apply' failed, failed to unify
+  HEq ?a ?a
+with
+  HEq false true
+⊢ HEq false true
+-/
+#guard_msgs in
+example : HEq false true := by with_reducible apply_rfl -- Error
+/--
+error: tactic 'rfl' failed, The lhs
+  False
+is not definitionally equal to rhs
+  True
+⊢ False ↔ True
+-/
+#guard_msgs in
+example : False ↔ True   := by with_reducible apply_rfl -- Error
+/--
+error: tactic 'rfl' failed, The lhs
+  false
+is not definitionally equal to rhs
+  true
+⊢ P false true
+-/
+#guard_msgs in
+example : P false true   := by with_reducible apply_rfl -- Error
+/--
+error: tactic 'rfl' failed, The lhs
+  false
+is not definitionally equal to rhs
+  true
+⊢ Q false true
+-/
+#guard_msgs in
+example : Q false true   := by with_reducible apply_rfl -- Error
+/--
+error: tactic 'rfl' failed, The lhs
+  false
+is not definitionally equal to rhs
+  true
+⊢ Q' false true
+-/
+#guard_msgs in
+example : Q' false true  := by with_reducible apply_rfl -- Error
+/--
+error: tactic 'rfl' failed, The lhs
+  false
+is not definitionally equal to rhs
+  true
+⊢ R false true
+-/
+#guard_msgs in
+example : R false true   := by with_reducible apply_rfl -- Error
+
+-- Inheterogeneous unequal
+
+/--
+error: tactic 'apply' failed, failed to unify
+  HEq ?a ?a
+with
+  HEq true 1
+⊢ HEq true 1
+-/
+#guard_msgs in
+example : HEq true 1 := by apply_rfl -- Error
+/--
+error: tactic 'apply' failed, failed to unify
+  HEq ?a ?a
+with
+  HEq true 1
+⊢ HEq true 1
+-/
+#guard_msgs in
+example : HEq true 1 := by with_reducible apply_rfl -- Error
+
+-- Rfl lemma with side condition:
+-- Error message should show left-over goal
+
+inductive S : Bool → Bool → Prop where | refl : a = true → S a a
+attribute [refl] S.refl
+/--
+error: tactic 'rfl' failed, The lhs
+  true
+is not definitionally equal to rhs
+  false
+⊢ S true false
+-/
+#guard_msgs in
+example : S true false  := by apply_rfl -- Error
+/--
+error: tactic 'rfl' failed, The lhs
+  true
+is not definitionally equal to rhs
+  false
+⊢ S true false
+-/
+#guard_msgs in
+example : S true false  := by with_reducible apply_rfl -- Error
+/--
+error: unsolved goals
+case a
+⊢ true = true
+-/
+#guard_msgs in
+example : S true true   := by apply_rfl -- Error (left-over goal)
+/--
+error: unsolved goals
+case a
+⊢ true = true
+-/
+#guard_msgs in
+example : S true true   := by with_reducible apply_rfl -- Error (left-over goal)
+/--
+error: unsolved goals
+case a
+⊢ false = true
+-/
+#guard_msgs in
+example : S false false := by apply_rfl -- Error (left-over goal)
+/--
+error: unsolved goals
+case a
+⊢ false = true
+-/
+#guard_msgs in
+example : S false false := by with_reducible apply_rfl -- Error (left-over goal)

From 3f918b56952140a3c80d5c9fbb89500b1a70ffa6 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Tue, 10 Sep 2024 10:03:56 +0200
Subject: [PATCH 06/16] Test documentation

---
 tests/lean/run/rflTacticErrors.lean | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/tests/lean/run/rflTacticErrors.lean b/tests/lean/run/rflTacticErrors.lean
index 21e21760e04d..9512fe97617f 100644
--- a/tests/lean/run/rflTacticErrors.lean
+++ b/tests/lean/run/rflTacticErrors.lean
@@ -19,17 +19,33 @@ example : false = true := by rfl
 
 -- Setup
 
+-- In addition to Eq, HEq and Iff  we test four relations:
+
+-- Plain reflexive predicate
 inductive P : α → α → Prop where | refl : P a a
 attribute [refl] P.refl
 
 -- Defeq to relation `P` at reducible transparency
 abbrev Q : α → α → Prop := P
+
 -- Defeq to relation `P` at default transparency
 def Q' : α → α → Prop := P
 
 -- No refl attribute
 inductive R : α → α → Prop where | refl : R a a
 
+
+/-
+Now we systematically test all relations with
+* syntactic equal arguments
+* reducibly equal arguments
+* semireducibly equal arguments
+* nonequal arguments
+
+and all using `apply_rfl` and `with_reducible apply_rfl`
+-/
+
+
 -- Syntactic equal
 
 example : true = true   := by apply_rfl

From 3c1e632bf8750a98f92baf38d8015c8f5c1a40e0 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Tue, 10 Sep 2024 10:27:16 +0200
Subject: [PATCH 07/16] Dead code

---
 src/Lean/Meta/Tactic/Rfl.lean | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Rfl.lean b/src/Lean/Meta/Tactic/Rfl.lean
index 7d39a658cdb8..4538f1eb0b84 100644
--- a/src/Lean/Meta/Tactic/Rfl.lean
+++ b/src/Lean/Meta/Tactic/Rfl.lean
@@ -48,12 +48,6 @@ initialize registerBuiltinAttribute {
 
 open Elab Tactic
 
-private def useKernel (lhs rhs : Expr) : MetaM Bool := do
-  if lhs.hasFVar || lhs.hasMVar || rhs.hasFVar || rhs.hasMVar then
-    return false
-  else
-    return (← getTransparency) matches TransparencyMode.default | TransparencyMode.all
-
 /-- `MetaM` version of the `rfl` tactic.
 
 This tactic applies to a goal whose target has the form `x ~ x`, where `~` is a reflexive

From 7e2870534b976bc05a491ecff3d2c4fe196b85bc Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Tue, 10 Sep 2024 11:40:48 +0200
Subject: [PATCH 08/16] Use approxDefEq

---
 src/Lean/Meta/Tactic/Rfl.lean        |  2 +-
 tests/lean/run/rflApplyFoApprox.lean | 15 +++++++++++++++
 2 files changed, 16 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/rflApplyFoApprox.lean

diff --git a/src/Lean/Meta/Tactic/Rfl.lean b/src/Lean/Meta/Tactic/Rfl.lean
index 4538f1eb0b84..0e08bf0f056e 100644
--- a/src/Lean/Meta/Tactic/Rfl.lean
+++ b/src/Lean/Meta/Tactic/Rfl.lean
@@ -72,7 +72,7 @@ def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := goal.withContext
   let lhs := t.appFn!.appArg!
   let rhs := t.appArg!
 
-  let success ← isDefEq lhs rhs
+  let success ← approxDefEq <| isDefEqGuarded lhs rhs
   unless success do
     throwTacticEx `rfl goal m!"The lhs{indentExpr lhs}\nis not definitionally equal to rhs{indentExpr rhs}"
 
diff --git a/tests/lean/run/rflApplyFoApprox.lean b/tests/lean/run/rflApplyFoApprox.lean
new file mode 100644
index 000000000000..9a807cfa7ec3
--- /dev/null
+++ b/tests/lean/run/rflApplyFoApprox.lean
@@ -0,0 +1,15 @@
+
+opaque f : Nat → Nat
+-- A rewrite with a free variable on the RHS
+
+opaque P : Nat → (Nat → Nat) → Prop
+opaque Q : Nat → Prop
+opaque foo (g : Nat → Nat) (x : Nat) : P x f ↔ Q (g x) := sorry
+
+example : P x f ↔ Q (x + 10) := by
+  rewrite [foo]
+  -- we have an mvar now
+  with_reducible rfl -- should should instantiate it with the lambda on the RHS and close the goal
+  -- same as
+  -- with_reducible (apply (Iff.refl _))
+  -- NB: apply, not exact! Different defEq flags.

From fde07c499453c4b6b380b1fef98fe63ca3c95934 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Wed, 11 Sep 2024 10:16:01 +0200
Subject: [PATCH 09/16] More tests

---
 tests/lean/run/rflTacticErrors.lean | 33 ++++++++++++++++++++++++++++-
 1 file changed, 32 insertions(+), 1 deletion(-)

diff --git a/tests/lean/run/rflTacticErrors.lean b/tests/lean/run/rflTacticErrors.lean
index 9512fe97617f..8950fb953d6f 100644
--- a/tests/lean/run/rflTacticErrors.lean
+++ b/tests/lean/run/rflTacticErrors.lean
@@ -6,6 +6,8 @@ This file tests the `rfl` tactic:
  * Effect of `with_reducible`
 -/
 
+-- First, let's see what `rfl` does:
+
 /--
 error: The rfl tactic failed. Possible reasons:
 - The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
@@ -17,7 +19,36 @@ Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.ref
 #guard_msgs in
 example : false = true := by rfl
 
--- Setup
+-- Now to `apply_rfl`.
+
+-- Plain error
+
+/--
+error: tactic 'rfl' failed, The lhs
+  42
+is not definitionally equal to rhs
+  23
+⊢ 42 = 23
+-/
+#guard_msgs in
+example : 42 = 23 := by apply_rfl
+
+-- Revealing implicit arguments
+
+opaque withImplicitNat {n : Nat} : Nat
+
+/--
+error: tactic 'rfl' failed, The lhs
+  withImplicitNat
+is not definitionally equal to rhs
+  withImplicitNat
+⊢ withImplicitNat = withImplicitNat
+-/
+#guard_msgs in
+example : @withImplicitNat 42 = @withImplicitNat 23 := by apply_rfl
+
+
+-- Exhaustive testing of various combinations:
 
 -- In addition to Eq, HEq and Iff  we test four relations:
 

From dbc7bc340035de71643ce00b02c52a93d13b5abd Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Wed, 11 Sep 2024 10:29:17 +0200
Subject: [PATCH 10/16] Improve error message

---
 src/Lean/Meta/Tactic/Rfl.lean       |  5 ++-
 tests/lean/run/rflTacticErrors.lean | 63 +++++++++++++++--------------
 2 files changed, 36 insertions(+), 32 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Rfl.lean b/src/Lean/Meta/Tactic/Rfl.lean
index 0e08bf0f056e..9b683cef2c4b 100644
--- a/src/Lean/Meta/Tactic/Rfl.lean
+++ b/src/Lean/Meta/Tactic/Rfl.lean
@@ -74,7 +74,10 @@ def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := goal.withContext
 
   let success ← approxDefEq <| isDefEqGuarded lhs rhs
   unless success do
-    throwTacticEx `rfl goal m!"The lhs{indentExpr lhs}\nis not definitionally equal to rhs{indentExpr rhs}"
+    let explanation := MessageData.ofLazyM (es := #[lhs, rhs]) do
+      let (lhs, rhs) ← addPPExplicitToExposeDiff lhs rhs
+      return m!"The lhs{indentExpr lhs}\nis not definitionally equal to rhs{indentExpr rhs}"
+    throwTacticEx `apply_rfl goal explanation
 
   if rel.isAppOfArity `Eq 1 then
     -- The common case is equality: just use `Eq.refl`
diff --git a/tests/lean/run/rflTacticErrors.lean b/tests/lean/run/rflTacticErrors.lean
index 8950fb953d6f..bf916b8fd007 100644
--- a/tests/lean/run/rflTacticErrors.lean
+++ b/tests/lean/run/rflTacticErrors.lean
@@ -21,40 +21,41 @@ example : false = true := by rfl
 
 -- Now to `apply_rfl`.
 
+-- A plain reflexive predicate
+inductive P : α → α → Prop where | refl : P a a
+attribute [refl] P.refl
+
 -- Plain error
 
 /--
-error: tactic 'rfl' failed, The lhs
+error: tactic 'apply_rfl' failed, The lhs
   42
 is not definitionally equal to rhs
   23
-⊢ 42 = 23
+⊢ P 42 23
 -/
 #guard_msgs in
-example : 42 = 23 := by apply_rfl
+example : P 42 23 := by apply_rfl
 
 -- Revealing implicit arguments
 
 opaque withImplicitNat {n : Nat} : Nat
 
 /--
-error: tactic 'rfl' failed, The lhs
-  withImplicitNat
+error: tactic 'apply_rfl' failed, The lhs
+  @withImplicitNat 42
 is not definitionally equal to rhs
-  withImplicitNat
-⊢ withImplicitNat = withImplicitNat
+  @withImplicitNat 23
+⊢ P withImplicitNat withImplicitNat
 -/
 #guard_msgs in
-example : @withImplicitNat 42 = @withImplicitNat 23 := by apply_rfl
+example : P (@withImplicitNat 42) (@withImplicitNat 23) := by apply_rfl
 
 
 -- Exhaustive testing of various combinations:
 
 -- In addition to Eq, HEq and Iff  we test four relations:
 
--- Plain reflexive predicate
-inductive P : α → α → Prop where | refl : P a a
-attribute [refl] P.refl
 
 -- Defeq to relation `P` at reducible transparency
 abbrev Q : α → α → Prop := P
@@ -178,7 +179,7 @@ error: rfl failed, no @[refl] lemma registered for relation
 example : R true'' true   := by apply_rfl -- Error
 
 /--
-error: tactic 'rfl' failed, The lhs
+error: tactic 'apply_rfl' failed, The lhs
   true''
 is not definitionally equal to rhs
   true
@@ -196,7 +197,7 @@ with
 #guard_msgs in
 example : HEq true'' true := by with_reducible apply_rfl -- Error
 /--
-error: tactic 'rfl' failed, The lhs
+error: tactic 'apply_rfl' failed, The lhs
   True''
 is not definitionally equal to rhs
   True
@@ -205,7 +206,7 @@ is not definitionally equal to rhs
 #guard_msgs in
 example : True'' ↔ True   := by with_reducible apply_rfl -- Error
 /--
-error: tactic 'rfl' failed, The lhs
+error: tactic 'apply_rfl' failed, The lhs
   true''
 is not definitionally equal to rhs
   true
@@ -214,7 +215,7 @@ is not definitionally equal to rhs
 #guard_msgs in
 example : P true'' true   := by with_reducible apply_rfl -- Error
 /--
-error: tactic 'rfl' failed, The lhs
+error: tactic 'apply_rfl' failed, The lhs
   true''
 is not definitionally equal to rhs
   true
@@ -223,7 +224,7 @@ is not definitionally equal to rhs
 #guard_msgs in
 example : Q true'' true   := by with_reducible apply_rfl -- Error
 /--
-error: tactic 'rfl' failed, The lhs
+error: tactic 'apply_rfl' failed, The lhs
   true''
 is not definitionally equal to rhs
   true
@@ -232,7 +233,7 @@ is not definitionally equal to rhs
 #guard_msgs in
 example : Q' true'' true  := by with_reducible apply_rfl -- Error
 /--
-error: tactic 'rfl' failed, The lhs
+error: tactic 'apply_rfl' failed, The lhs
   true''
 is not definitionally equal to rhs
   true
@@ -243,7 +244,7 @@ example : R true'' true   := by with_reducible apply_rfl -- Error
 
 -- Unequal
 /--
-error: tactic 'rfl' failed, The lhs
+error: tactic 'apply_rfl' failed, The lhs
   false
 is not definitionally equal to rhs
   true
@@ -261,7 +262,7 @@ with
 #guard_msgs in
 example : HEq false true := by apply_rfl -- Error
 /--
-error: tactic 'rfl' failed, The lhs
+error: tactic 'apply_rfl' failed, The lhs
   False
 is not definitionally equal to rhs
   True
@@ -270,7 +271,7 @@ is not definitionally equal to rhs
 #guard_msgs in
 example : False ↔ True   := by apply_rfl -- Error
 /--
-error: tactic 'rfl' failed, The lhs
+error: tactic 'apply_rfl' failed, The lhs
   false
 is not definitionally equal to rhs
   true
@@ -279,7 +280,7 @@ is not definitionally equal to rhs
 #guard_msgs in
 example : P false true   := by apply_rfl -- Error
 /--
-error: tactic 'rfl' failed, The lhs
+error: tactic 'apply_rfl' failed, The lhs
   false
 is not definitionally equal to rhs
   true
@@ -288,7 +289,7 @@ is not definitionally equal to rhs
 #guard_msgs in
 example : Q false true   := by apply_rfl -- Error
 /--
-error: tactic 'rfl' failed, The lhs
+error: tactic 'apply_rfl' failed, The lhs
   false
 is not definitionally equal to rhs
   true
@@ -297,7 +298,7 @@ is not definitionally equal to rhs
 #guard_msgs in
 example : Q' false true  := by apply_rfl -- Error
 /--
-error: tactic 'rfl' failed, The lhs
+error: tactic 'apply_rfl' failed, The lhs
   false
 is not definitionally equal to rhs
   true
@@ -307,7 +308,7 @@ is not definitionally equal to rhs
 example : R false true   := by apply_rfl -- Error
 
 /--
-error: tactic 'rfl' failed, The lhs
+error: tactic 'apply_rfl' failed, The lhs
   false
 is not definitionally equal to rhs
   true
@@ -325,7 +326,7 @@ with
 #guard_msgs in
 example : HEq false true := by with_reducible apply_rfl -- Error
 /--
-error: tactic 'rfl' failed, The lhs
+error: tactic 'apply_rfl' failed, The lhs
   False
 is not definitionally equal to rhs
   True
@@ -334,7 +335,7 @@ is not definitionally equal to rhs
 #guard_msgs in
 example : False ↔ True   := by with_reducible apply_rfl -- Error
 /--
-error: tactic 'rfl' failed, The lhs
+error: tactic 'apply_rfl' failed, The lhs
   false
 is not definitionally equal to rhs
   true
@@ -343,7 +344,7 @@ is not definitionally equal to rhs
 #guard_msgs in
 example : P false true   := by with_reducible apply_rfl -- Error
 /--
-error: tactic 'rfl' failed, The lhs
+error: tactic 'apply_rfl' failed, The lhs
   false
 is not definitionally equal to rhs
   true
@@ -352,7 +353,7 @@ is not definitionally equal to rhs
 #guard_msgs in
 example : Q false true   := by with_reducible apply_rfl -- Error
 /--
-error: tactic 'rfl' failed, The lhs
+error: tactic 'apply_rfl' failed, The lhs
   false
 is not definitionally equal to rhs
   true
@@ -361,7 +362,7 @@ is not definitionally equal to rhs
 #guard_msgs in
 example : Q' false true  := by with_reducible apply_rfl -- Error
 /--
-error: tactic 'rfl' failed, The lhs
+error: tactic 'apply_rfl' failed, The lhs
   false
 is not definitionally equal to rhs
   true
@@ -397,7 +398,7 @@ example : HEq true 1 := by with_reducible apply_rfl -- Error
 inductive S : Bool → Bool → Prop where | refl : a = true → S a a
 attribute [refl] S.refl
 /--
-error: tactic 'rfl' failed, The lhs
+error: tactic 'apply_rfl' failed, The lhs
   true
 is not definitionally equal to rhs
   false
@@ -406,7 +407,7 @@ is not definitionally equal to rhs
 #guard_msgs in
 example : S true false  := by apply_rfl -- Error
 /--
-error: tactic 'rfl' failed, The lhs
+error: tactic 'apply_rfl' failed, The lhs
   true
 is not definitionally equal to rhs
   false

From 52cdde3e379639b79e178c474af947f7616281b3 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Mon, 16 Sep 2024 12:33:52 +0200
Subject: [PATCH 11/16] Trigger stage0 update after merge

---
 stage0/src/stdlib_flags.h | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 0699845ba452..f636bca698ff 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -18,3 +18,5 @@ options get_default_options() {
     return opts;
 }
 }
+
+// please update stage0

From c972bcbc344aef3528498a993bbfb3f65291a625 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Wed, 18 Sep 2024 15:11:41 +0200
Subject: [PATCH 12/16] Do not use isDefEqGuarded

---
 src/Lean/Meta/Tactic/Rfl.lean        |  2 +-
 tests/lean/run/rflApplyFoApprox.lean | 13 ++++++++-----
 2 files changed, 9 insertions(+), 6 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Rfl.lean b/src/Lean/Meta/Tactic/Rfl.lean
index 9b683cef2c4b..7329fcf67915 100644
--- a/src/Lean/Meta/Tactic/Rfl.lean
+++ b/src/Lean/Meta/Tactic/Rfl.lean
@@ -72,7 +72,7 @@ def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := goal.withContext
   let lhs := t.appFn!.appArg!
   let rhs := t.appArg!
 
-  let success ← approxDefEq <| isDefEqGuarded lhs rhs
+  let success ← isDefEqGuarded lhs rhs
   unless success do
     let explanation := MessageData.ofLazyM (es := #[lhs, rhs]) do
       let (lhs, rhs) ← addPPExplicitToExposeDiff lhs rhs
diff --git a/tests/lean/run/rflApplyFoApprox.lean b/tests/lean/run/rflApplyFoApprox.lean
index 9a807cfa7ec3..871a9d65cdb1 100644
--- a/tests/lean/run/rflApplyFoApprox.lean
+++ b/tests/lean/run/rflApplyFoApprox.lean
@@ -8,8 +8,11 @@ opaque foo (g : Nat → Nat) (x : Nat) : P x f ↔ Q (g x) := sorry
 
 example : P x f ↔ Q (x + 10) := by
   rewrite [foo]
-  -- we have an mvar now
-  with_reducible rfl -- should should instantiate it with the lambda on the RHS and close the goal
-  -- same as
-  -- with_reducible (apply (Iff.refl _))
-  -- NB: apply, not exact! Different defEq flags.
+  -- we have an mvar in the goal now
+
+  -- exact fails to close it (as it does not do approxDefEq)
+  fail_if_success with_reducible exact Iff.rfl
+  -- so `rfl` shouldn't either
+  fail_if_success rfl
+  -- but note that apply can close it:
+  with_reducible(apply (Iff.rrfl)

From 802fa765ed71363d9f65df82f6b05c288ed49eb5 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Wed, 18 Sep 2024 16:27:32 +0200
Subject: [PATCH 13/16] Remove exact Iff.rfl macro

---
 src/Init/Core.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 3d8bab2bb2a1..2d448344f277 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -823,8 +823,6 @@ theorem iff_iff_implies_and_implies {a b : Prop} : (a ↔ b) ↔ (a → b) ∧ (
 protected theorem Iff.rfl {a : Prop} : a ↔ a :=
   Iff.refl a
 
-macro_rules | `(tactic| rfl) => `(tactic| exact Iff.rfl)
-
 theorem Iff.of_eq (h : a = b) : a ↔ b := h ▸ Iff.rfl
 
 theorem Iff.trans (h₁ : a ↔ b) (h₂ : b ↔ c) : a ↔ c :=

From 85f50e86889aa424c78d034af392752adf8bee07 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Wed, 18 Sep 2024 16:27:39 +0200
Subject: [PATCH 14/16] Revert "Do not use isDefEqGuarded"

This reverts commit c972bcbc344aef3528498a993bbfb3f65291a625.
---
 src/Lean/Meta/Tactic/Rfl.lean        |  2 +-
 tests/lean/run/rflApplyFoApprox.lean | 13 +++++--------
 2 files changed, 6 insertions(+), 9 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Rfl.lean b/src/Lean/Meta/Tactic/Rfl.lean
index 7329fcf67915..9b683cef2c4b 100644
--- a/src/Lean/Meta/Tactic/Rfl.lean
+++ b/src/Lean/Meta/Tactic/Rfl.lean
@@ -72,7 +72,7 @@ def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := goal.withContext
   let lhs := t.appFn!.appArg!
   let rhs := t.appArg!
 
-  let success ← isDefEqGuarded lhs rhs
+  let success ← approxDefEq <| isDefEqGuarded lhs rhs
   unless success do
     let explanation := MessageData.ofLazyM (es := #[lhs, rhs]) do
       let (lhs, rhs) ← addPPExplicitToExposeDiff lhs rhs
diff --git a/tests/lean/run/rflApplyFoApprox.lean b/tests/lean/run/rflApplyFoApprox.lean
index 871a9d65cdb1..9a807cfa7ec3 100644
--- a/tests/lean/run/rflApplyFoApprox.lean
+++ b/tests/lean/run/rflApplyFoApprox.lean
@@ -8,11 +8,8 @@ opaque foo (g : Nat → Nat) (x : Nat) : P x f ↔ Q (g x) := sorry
 
 example : P x f ↔ Q (x + 10) := by
   rewrite [foo]
-  -- we have an mvar in the goal now
-
-  -- exact fails to close it (as it does not do approxDefEq)
-  fail_if_success with_reducible exact Iff.rfl
-  -- so `rfl` shouldn't either
-  fail_if_success rfl
-  -- but note that apply can close it:
-  with_reducible(apply (Iff.rrfl)
+  -- we have an mvar now
+  with_reducible rfl -- should should instantiate it with the lambda on the RHS and close the goal
+  -- same as
+  -- with_reducible (apply (Iff.refl _))
+  -- NB: apply, not exact! Different defEq flags.

From fa5b6e29c6e53b02d0ae1bf6f1bf56f4d5e79f23 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Thu, 19 Sep 2024 15:57:08 +0200
Subject: [PATCH 15/16] Update test

---
 tests/lean/run/5359.lean | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/tests/lean/run/5359.lean b/tests/lean/run/5359.lean
index 34a34c5f7180..cddb23fb214b 100644
--- a/tests/lean/run/5359.lean
+++ b/tests/lean/run/5359.lean
@@ -16,4 +16,8 @@ variable {α : Nat → Type u} [∀ i, LE (α i)]
 instance : L (S α) Nat α := sorry
 instance : LE (S α) := ⟨fun f g ↦ ∀ i, f i ≤ g i⟩
 
-example : ∀ {a b : S α}, L.coe a ≤ L.coe b ↔ a ≤ b := by rfl
+example : ∀ {a b : S α}, L.coe a ≤ L.coe b ↔ a ≤ b := by
+  -- at some point, rfl would, for Iff.rfl, use `exact` which would enable implicit lambdas
+  fail_if_success rfl
+  -- how, one has to intro first
+  intros; rfl

From bb5b28d3f21829b00c38d8b6b00c4ef5f4e14c4e Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Thu, 19 Sep 2024 16:00:16 +0200
Subject: [PATCH 16/16] Actually, let's not get this PR entangled with removing
 the Iff.rfl macro

---
 src/Init/Core.lean       | 2 ++
 tests/lean/run/5359.lean | 6 +-----
 2 files changed, 3 insertions(+), 5 deletions(-)

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 5ceda4412537..5a1f9df89563 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -823,6 +823,8 @@ theorem iff_iff_implies_and_implies {a b : Prop} : (a ↔ b) ↔ (a → b) ∧ (
 protected theorem Iff.rfl {a : Prop} : a ↔ a :=
   Iff.refl a
 
+macro_rules | `(tactic| rfl) => `(tactic| exact Iff.rfl)
+
 theorem Iff.of_eq (h : a = b) : a ↔ b := h ▸ Iff.rfl
 
 theorem Iff.trans (h₁ : a ↔ b) (h₂ : b ↔ c) : a ↔ c :=
diff --git a/tests/lean/run/5359.lean b/tests/lean/run/5359.lean
index cddb23fb214b..34a34c5f7180 100644
--- a/tests/lean/run/5359.lean
+++ b/tests/lean/run/5359.lean
@@ -16,8 +16,4 @@ variable {α : Nat → Type u} [∀ i, LE (α i)]
 instance : L (S α) Nat α := sorry
 instance : LE (S α) := ⟨fun f g ↦ ∀ i, f i ≤ g i⟩
 
-example : ∀ {a b : S α}, L.coe a ≤ L.coe b ↔ a ≤ b := by
-  -- at some point, rfl would, for Iff.rfl, use `exact` which would enable implicit lambdas
-  fail_if_success rfl
-  -- how, one has to intro first
-  intros; rfl
+example : ∀ {a b : S α}, L.coe a ≤ L.coe b ↔ a ≤ b := by rfl