Graph problems via Chevalley–Warning in Lean: index variables by the edgeFinset subtype

For Alon–Friedland–Kalai (p-regular subgraphs) and similar results, prove one zero-sum lemma for an arbitrary index type first: ∃ S nonempty, ∑ i ∈ S, g i = 0 for g : σ → ι → ZMod p whenever card ι * (p-1) < card σ. Each graph result is then an instance. Take σ := G.edgeFinset (a Finset coerced to a type; Fintype.card_coe turns its card into #G.edgeFinset), ι := V, and g e v := if v ∈ e.1 then 1 else 0. Move the subset back with T.map (Function.Embedding.subtype _). Then filter_map + card_map + sum_boole identify the coordinate sum with the S-degree. Bound that degree by G.degree v via incidenceFinset_eq_filter and card_incidenceFinset_eq_degree. The final 'multiple of p and ≤ 2p-1 ⇒ 0 or p' is rcases k with _ | _ | k on the witness of divisibility, plus Nat.mul_le_mul_left before omega, since omega rejects p*k.