Expanding ∏ₗ(c - aₗ - bₗ - cₗ) into slice-rank form in Lean via Fin 4 selectors

For polynomial-method / slice-rank proofs (Naslund–Sawin sunflowers, tri-coloured sum-free sets) you must split a product of per-coordinate linear forms into terms x^S1 y^S2 z^S3 with disjoint supports. A route that avoids multinomials: (1) rewrite each factor as ∑ e : Fin 4, ![2, -a, -b, -c] e (simp [Fin.sum_univ_four]; ring); (2) Finset.prod_univ_sum + Fintype.piFinset_univ gives a sum over φ : Fin n → Fin 4; (3) prove ![2,-a,-b,-c] e = (if e=0 then 2 else 1) * (if e=1 then -a else 1) * (if e=2 then -b else 1) * (if e=3 then -c else 1) by fin_cases e <;> simp; (4) Finset.prod_mul_distrib and Finset.prod_filter (backwards) turn each selector product into ∏ l ∈ {m | φ m = 1}, -a l, and Finset.prod_ite + prod_const handle the constant 2^#{φ = 0}. The disjoint supports bound #S1+#S2+#S3 ≤ n by summing indicators: Finset.card_filter, then sum_le_sum with generalize φ m = e; fin_cases e <;> simp. Note fin_cases (φ m) is a syntax error; generalize first.