chore: fix typo and incorrect name in doc

[b-mehta]

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.)

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 748eab95113febbf8fa062643d06af3db49e0a1f --onto 287d46e1f6a7a6136c7996367a9b203d93797d00. (2024-06-08 03:56:23)
• ✅ Mathlib branch lean-pr-testing-4404 has successfully built against this PR. (2024-06-08 17:10:29) View Log
• ✅ Mathlib branch lean-pr-testing-4404 has successfully built against this PR. (2024-06-08 20:38:14) View Log

[nomeata]

Thanks for the typo fix.

It would be helpful if we had Eq.rfl, so that it follows the naming convention of all the other relations which have both Foo.refl and Foo.rfl, and where Foo.rfl has the argument implicit. After all the message suggests to use the right one for your relation. Just writing rfl is confusing here, also with the tactic of the same name. Maybe we should introduce Eq.rfl. Until then maybe list two possible lemmas (there aren't many in core, unfortunately.)

WDYT?

[b-mehta]

I agree that writing Eq.rfl would be better here, but since it doesn't exist, I guessed that it would be unreasonable to add a new theorem in such a low-level file as part of a typo-fix only PR. How about Eq.refl _ for now, with a follow-up adding Eq.rfl in a separate PR?

Could you advise how to fix the CI issue? If I do the suggested rebase command then it doesn't allow me to push.

[nomeata]

I don't think there is any rebasing to do. Once the test suite works (maybe the expected output isn't quite right yet) we can merge this.

[leodemoura]

Waiting test to be fixed.