siddhartha-gadgil/leanaide/cases-exhaustion

Skill: Cases and Exhaustion

Pre-condition: Apply this skill when hypotheses provide a disjunction, the objects fall into finitely many types, or the problem naturally splits by parity, sign, residue class, rank, dimension, or degeneracy.

Goal: Produce an exhaustive case split and prove the target in every branch.

Instructions:

1. Choose the Split: Identify the proposition, finite set, or structural distinction that partitions the problem.
2. Prove Exhaustiveness: State why every object falls into one of the listed cases.
3. Handle Cases Independently: In each branch, add the case assumption to the context and prove the original goal.
4. Merge Branches: Confirm every branch proves the same conclusion or the appropriate branch-specific part of a disjunction.
5. For Exhaustion: If the cases are finite and computational, make a table of all cases and record the verified result for each.

Common Failure Modes:

• Missing boundary or degenerate cases.
• Proving different conclusions in different branches.
• Using a large case split when a symmetry can reduce the number of cases.