port unfold_wf

Stream: mathlib4

[Henrik Böving]

For my current work on slim check it would be very useful to have this tactic https://github.com/leanprover-community/mathlib/blob/b8faf130b780a2a4b95541957e23fd8206718f13/src/tactic/interactive.lean#L58-L60 to use in sizeOf based proofs (which come up quite a lot here in the sampleable framework) should I just try and port this or do we have something that replaces it arelady?