If I have the following:
H : some complicated expression = some other complicated expression
and I want to grab
u := some other complicated expression
without hardcoding it into my proof (i.e., using pose)
Is there a clean way to do this in LTac?