Oh, I didn't know about unshelve eexists thanks, cool!
unshelve eexists
Daniel Hilst Selli has marked this topic as resolved.
Oh I can do unshelve eassert (2 * x = _ x) and get a subgoal focused for this hole
unshelve eassert (2 * x = _ x)
Last updated: Feb 09 2023 at 00:03 UTC