[obtain id | conclude term] = term [auto_params | using term | using once term | proof] [done]

conclude can be used only if the current sequent is stating an equality. The left hand side must be omitted in an equality chain.

Starts or continues an equality chain. If the chain starts with obtain H a new subproof named H is started.

If the chain starts with obtain H a nre sequent for t2 = ? is opened.