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

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.