Non-finishing aesops

Stream: lean4

[Darij Grinberg]

Is there a simple trick to rewrite non-finishing aesops into finishing ones without having to understand what is going on? Some kind of have? What to do if aesop creates multiple subgoals?

[Jakob von Raumer]

aesop? suggests a tactic or a chain of tactics with the same effect as the aesop call. Alternatively (though not really an actual answer to your question) one can make the warning go away by replacing it with aesop (config := { warnOnNonterminal := false }).

[Jakob von Raumer]

If the aesop results in multiple goals, it's a bit tricker, one then has to distribute the tactics that come afterwards to the sorrys in the tactics that you get from aesop?.

[Darij Grinberg]

Thanks Jakob!