Build the idea in three steps
- The whole case works with one shorthand: Fermat42 a b c says that a and b are non-zero and a ^ 4 + b ^ 4 = c ^ 2. The docstring promises the payoff: no integers satisfy it, so Fermat’s exponent four follows.
- Bundle theorems keep the dossier tidy: comm swaps a and b, because addition does not care about order — delta Fermat42 unfolds the shorthand first, then rw [add_comm] turns one side into the other.
- Name the suspect once, and every later page can say “a Fermat42 solution” instead of repeating three conditions — the same economy the whole library lives on.
A small example
Finding a field in a nested conjunction: the equation is packed as the third component — h.1.2.2 picks out a ^ 4 + b ^ 4 = c ^ 2 from the bundle, exactly how the proofs below reach it.