MATH.19:4.5 - Assemble the argument and inspect its dependencies

Order the proved claims so that each step uses available results. State an auxiliary lemma with the hypotheses under which it was proved, then bind its variables to the objects of the receiving step.

Inspect any apparent cycle. Induction can justify use of a smaller case under its decrease condition; it cannot justify using the current theorem as an unproved premise of its own auxiliary lemma. Separate the required earlier result or change the argument.

For cases, establish the target for every admitted branch. For an implication, discharge its temporary assumption when returning to the outer argument. For a contradiction argument, retain the logical principle that turns the contradiction into the requested conclusion; extracting a witness can remain a further question.

Write enough of the completed argument for another prepared reader to recover the decisive inference. A proof assistant can check a formal derivation and its dependencies when that is useful. Compare the checked statement with the intended statement before using the result.