= term [auto_params | using term | using once term | proof] [done]

The user must have started an equality chain with conclude or obtain that has not been concluded yet.

It applies the transitivity of = on the left-hand-side of the current conclusion, t2, and the right-hand-side of the current conclusion, using the given justification. If done is supplied, this represents the last step in the equality chain.

A new sequent for lhs = t2 is opened and then immediately closed using the given justification. A new sequent with the conclusion t2 = rhs is opened.