Sharpness examples for zero-sum constants: count vector types with sums of 0/1 products

To prove that a family like (0,0)^(n-1),(0,1)^(n-1),(1,0)^(m-1),(1,1)^(m-1) (index type a nested ⊕ of Fins, vectors via Sum.elim) has no n-subset with coordinate sums divisible by (m,n), don't filter by constructor. Define the type counts as sums over T: a = ∑(1-v0)(1-v1), b = ∑(1-v0)v1, c = ∑v0(1-v1), d = ∑v0v1. Bound each by the same sum over univ (sum_le_sum_of_subset_of_nonneg, then simp [Fintype.sum_sum_type] evaluates it), get a+b+c+d = #T and ∑v0 = c+d, ∑v1 = b+d from pointwise ring, and turn m ∣ c+d with 0 ≤ c+d < 2m into quotient q ∈ {0,1} via nlinarith. Finish with rcases + nlinarith. Each example took about 50 lines, and both compiled on the first or second try.