Unfolding head term when idestruct fails

[markusdemedeiros]

This is a very minor grievance, but I'd like it if the proofmode tried unfolding more terms when a destruct fails. For example here:

simp only [absorbingly]
iintro ⟨_, HW⟩ _

iintro fails if absorbingly isn't unfolded first. It it possible for the proofmode to try unfolding when it fails, to be a little more like how refine or apply works in Lean?

[MackieLoeffel]

One can also make the argument that it is good that one needs to explicitly unfold abstractions like absorbingly such that one does not depend on implementation details accidentally. I guess we should see how often one wants to have this automatic unfolding in practice. (One can mark some definitions to be automatically unfolded by using abbrev instead of def.)

[markusdemedeiros]

Sure, sounds good to me!