diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index 1465d575ba..8b6842a9f3 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -373,7 +373,8 @@ reflexivity theorems (e.g., `Iff.rfl`).
 macro "rfl" : tactic => `(tactic| case' _ => fail "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 reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`.")
+Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
+`exact HEq.rfl` etc.")
 
 macro_rules | `(tactic| rfl) => `(tactic| eq_refl)
 macro_rules | `(tactic| rfl) => `(tactic| exact HEq.rfl)
diff --git a/tests/lean/run/wfirred.lean b/tests/lean/run/wfirred.lean
index 6916071e95..ee96ba698a 100644
--- a/tests/lean/run/wfirred.lean
+++ b/tests/lean/run/wfirred.lean
@@ -38,7 +38,8 @@ example : foo 0 = 0 := by rfl
 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 reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`.
+Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
+`exact HEq.rfl` etc.
 n : Nat
 ⊢ foo (n + 1) = foo n
 -/
diff --git a/tests/lean/runTacticMustCatchExceptions.lean.expected.out b/tests/lean/runTacticMustCatchExceptions.lean.expected.out
index f8bb3afdc8..42215a9a19 100644
--- a/tests/lean/runTacticMustCatchExceptions.lean.expected.out
+++ b/tests/lean/runTacticMustCatchExceptions.lean.expected.out
@@ -1,20 +1,23 @@
 runTacticMustCatchExceptions.lean:2:25-2:28: 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 reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`.
+Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
+`exact HEq.rfl` etc.
 a b : Nat
 ⊢ 1 ≤ a + b
 runTacticMustCatchExceptions.lean:3:25-3:28: 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 reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`.
+Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
+`exact HEq.rfl` etc.
 a b : Nat
 this : 1 ≤ a + b
 ⊢ a + b ≤ b
 runTacticMustCatchExceptions.lean:4:25-4:28: 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 reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`.
+Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
+`exact HEq.rfl` etc.
 a b : Nat
 this✝ : 1 ≤ a + b
 this : a + b ≤ b
@@ -22,18 +25,21 @@ this : a + b ≤ b
 runTacticMustCatchExceptions.lean:9:18-9:21: 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 reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`.
+Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
+`exact HEq.rfl` etc.
 a b : Nat
 ⊢ 1 ≤ a + b
 runTacticMustCatchExceptions.lean:10:14-10:17: 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 reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`.
+Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
+`exact HEq.rfl` etc.
 a b : Nat
 ⊢ a + b ≤ b
 runTacticMustCatchExceptions.lean:11:14-11:17: 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 reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`.
+Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
+`exact HEq.rfl` etc.
 a b : Nat
 ⊢ b ≤ 2