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

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.