card_of_slice

theorem card_of_slice [Finite G] (A : Set G) :    ∃ φ : G →+ ZMod 2, 2*Nat.card { x | x ∈ A ∧ φ x = 1 } ≥ (Nat.card A-1) := by  cases nonempty_fintype G  classical  have _ : Fintype (G →+ ZMod 2) := Fintype.ofEquiv G dual_iso.toEquiv  have h1 := calc        2 * ∑ φ : G →+ ZMod 2, Nat.card {x | x ∈ A ∧ φ x = 1}    _ = 2 * ∑ φ : G →+ ZMod 2, ∑ x ∈ A, if φ x = 1 then 1 else 0 := by simp [Fintype.subtype_card]    _ = 2 * ∑ x ∈ A, Nat.card {φ : G →+ ZMod 2 | φ x = 1} := by      rw [Finset.sum_comm]; simp [Fintype.subtype_card]    _ ≥ 2 * ∑ x ∈ A.toFinset.erase 0, Nat.card {φ : G →+ ZMod 2 | φ x = 1} := by      by_cases h : 0 ∈ A      · rw [← Finset.sum_erase_add (s := A.toFinset) (a := 0)]        · simp        simp [h]      apply le_of_eq      congr      apply Finset.erase_eq_of_notMem      simp [h]    _ = ∑ x ∈ (A.toFinset.erase 0), Nat.card G := by      rw [Finset.mul_sum]      congr! with x hx      simp only [mem_erase, ne_eq, Set.mem_toFinset] at hx      exact card_of_dual_constrained x hx.1    _ ≥ (Nat.card A-1) * (Nat.card G) := by      simp only [sum_const, smul_eq_mul, ge_iff_le, Nat.card_eq_card_toFinset]      gcongr      exact Finset.pred_card_le_card_erase    _ = Nat.card G * (Nat.card A-1)  := by ring  by_contra! h2  replace h2 :      2*∑ φ : G →+ ZMod 2, Nat.card {x | x ∈ A ∧ φ x = 1} < ∑ φ : G →+ ZMod 2, (Nat.card A-1) := by    rw [Finset.mul_sum]    apply Finset.sum_lt_sum_of_nonempty    · simp    intro φ _; exact h2 φ  simp only [sum_const, card_univ, smul_eq_mul,←Nat.card_eq_fintype_card,card_of_dual] at h2  order