chore: fix typo and incorrect name in doc (#4404)

Fixes typo "reflexivitiy" to "reflexivity", and changes exact Eq.rfl to
exact rfl, since Eq.rfl does not exist.

(I got something confused wrt the bot message on #4367 and accidentally
closed that one, so making this one instead, which I think satisfies the
requirements it wanted.)

---------

Co-authored-by: Joachim Breitner <[email protected]>

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)

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

tests/lean/runTacticMustCatchExceptions.lean.expected.out

@@ -1,39 +1,45 @@
 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
 ⊢ b ≤ 2
 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