MATH.19:4.2 - Work backward to sufficient claims
Inspect how the conclusion could be established. Common entry moves include:
| Wanted conclusion | First proof obligation |
|---|---|
| P implies Q | Assume P for this part of the argument and establish Q. |
| P and Q | Establish both claims under the required assumptions. |
| Every admitted x satisfies P(x) | Take an arbitrary admitted x and establish P(x) without adding a special property of it. |
| Some x satisfies P(x) | Construct a suitable x and establish P(x), when a witness construction is available. |
| Two mathematical expressions are equal | Find permitted transformations or an intermediate expression connecting them. |
| A theorem’s conclusion applies here | Match its objects and discharge all premises needed for that application. |
An established theorem can replace one target with several premise obligations. A proposed lemma can do the same, but remains an obligation until proved. Retain why the proposed premises would suffice: this is the connection that makes the lemma useful.
Some backward moves deliberately strengthen the task. To show that two complicated expressions have the same value, finding one common normal form may be convenient. If the stronger task becomes obstructed, return to the weaker conclusion or find another route.