MATH.19:8 - Common Anti-Patterns and How to Avoid Them
Using the desired conclusion inside its supporting lemma. If the lemma that justifies a rearrangement is proved by assuming that rearrangement, the gap remains. Prove the smaller commuting statement from its own premise, as in :5.2.
Fixing a parameter that the next step changes. The empty-accumulator hypothesis in :5.3 cannot be applied to a nonempty accumulator. Generalize the statement and recheck the base and step.
Silently changing a premise to finish the proof. Commutation makes the rearrangement in :5.2 valid. If it is absent from the intended use, state the changed theorem or retain the interleaved operation.
Closing a different composite. The two inverse identities in :5.1 support different conclusions. Compare the operands and order of the proved statement with the question being answered.