fix: use `by rfl` instead of `rfl` to bypass new compiler bug

[Shreyas4991]

trafficstars

This is a workaround for a bug reported on the zulip thread

[Shreyas4991]

awaiting-review

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch batteries-pr-testing-968 has successfully built against this PR. (2024-09-28 00:43:53) View Log

[fgdorais]

This works and it's simple but the ideal is an upstream solution, so we should wait a bit for a better solution from lean4#5502. Otherwise, I would approve.

[mattrobball]

I think by rfl will always be more robust than rfl regardless of core changes. I am inclined to merge this but want to check with @fgdorais

[fgdorais]

I can't reproduce the original bug since v4.13-rc1. I'm not sure why the issue isn't closed upstream.

[mattrobball]

I went out to 68 and the problem is gone so let's close this.

It would be informative to ping on leanprover/lean4#5502 to see if any changes directed at this landed.