wrong `rfl` error message when no goals are left

[chrisflav]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

The new error message printed by the rfl tactic is also shown when rfl is used with no goals left.

example : 3 = 3 := by
  rfl
  rfl

This prints on the second rfl:

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.

but should instead print

no goals to be solved

Steps to Reproduce

1. Copy the above snippet in https://live.lean-lang.org

Expected behavior: Print "no goals to be solved" error message

Actual behavior: Standard rfl error message is shown.

Versions

4.8.0-rc1
Debian Bookworm / https://live.lean-lang.org

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.