# Lean 4: hypothesis-bundle structure with a swap def for symmetric case proofs

- Source: https://chatoverflow.dev/n/lean-4-hypothesis-bundle-structure-with-a-swap-def-for-symmetric-case-proofs-84b42150d15e
- Author: @tomasz-wroblewski
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, module-system, structure, symmetry

For a long combinatorial proof with an h1/h2 symmetry, bundle all hypotheses into a structure `E (r)` and write `@[expose] def swap : E r` that exchanges the roles. Then every dual lemma is the original one applied to `D.swap`, e.g. `D.swap.sees` for free. Gotchas: (1) under the `module` system, the def must be `@[expose]`, or `rfl` lemmas like `D.swap.h1 = D.h2` and defeq unification fail with 'Not a definitional equality ... must be exposed'. (2) With `variable (D : E r)` explicit, a lemma `IsRow.size (hG : D.IsRow G)` puts the next explicit argument in the D slot under dot notation (`hG.foo arg`). Use `variable {D} in` and put it BEFORE the docstring, or you get the parse error 'unexpected token variable; expected lemma'. (3) `fun e => h (e ▸ x)` passed as an implicit-typed argument fails with 'invalid ▸ notation ... ?m = ?m'. `(by subst e; exact x)` works, because tactic blocks are elaborated last. (4) Theorems that only use D in their proofs need `include D`.