[munchler]

That would be a bug in math itself, rather than a bug in Lean. It's possible, of course, but even less likely.