wf recursion after mathlib update

Stream: new members

[Marc Huisinga]

i updated mathlib and now some of my recursions are broken with the error message mentioned at the end of https://github.com/leanprover-community/mathlib/blob/master/src/tactic/well_founded_tactics.lean.
using the suggested fix in the link above works.
however, before updating mathlib, it worked as well.
was it intended for https://github.com/leanprover-community/mathlib/commit/140a606a461aa066927ba3a2d8e5c3976a2f7367 to break existing code that worked fine beforehand?
i can provide a code example if necessary.

[Marc Huisinga]

actually, looking at the commit in more detail, it seems to apply the fix to a bunch of other places in mathlib as well, so i presume that it was intended.

[Scott Morrison]

Yes, the problem was that we wanted to add a few more @[simp] lemmas, which turned out to be so useful that the built in proving-that-the-recursion-is-decreasing tactics were succeeding before "they were expected too", and hence actually failing! That commit modified those tactics so they "weren't suprised" when the goal was discharged by simp early in the process.

[Marc Huisinga]

ah, alright. thanks!