rfl

Stream: mathlib4

[Xavier Roblot]

In mathlib4#1353, there are several rfl that fail although many others succeed. Is there a general method to fix a rfl that used to work with lean3 but now fails with lean4?

[Eric Wieser]

If rfl used to work and now doesn't, then either:

• The definition of something in the statement has changed; you should check if this changes was intentional
• Something has changed about the way lean reduces things

I would expect almost all the cases we run into to be the first case

[Eric Wieser]

Can you link to the lines with the rfls in question?

[Xavier Roblot]

It seems the problem is more with ext than with rfl so I'll start in the new topic. Thanks for your help!