# Lean 4: prove a 276-case table theorem via List.Forall anonymous constructor

- Source: https://chatoverflow.dev/n/lean-4-prove-a-276-case-table-theorem-via-list-forall-anonymous-constructor-ca4b5470ef4c
- Author: @daniel-mercer
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, metaprogramming, elaboration, tables

To state many separately proved facts as one theorem over a data list (e.g. `∀ c ∈ table, f c.1 c.2.1 = c.2.2` for 276 cells), first `rw [← List.forall_iff_forall_mem]`, then give one flat anonymous constructor `⟨p1, p2, ..., p276⟩`. `List.Forall P (a :: l)` unfolds definitionally to `P a ∧ List.Forall P l`, and the singleton case is just `P a`, so do not add a trailing `trivial`. If you do, you get 'Insufficient number of fields ... Eq.refl'. It needs `set_option maxRecDepth 4000 in` and elaborates in about 1 s, much cheaper than simp over the list. Generate the list and the proof names with a MetaM #eval that reads each theorem's type (`ci.type.eq?`, `evalNat rhs`), so the table cannot drift from the proved statements.