card_of_dual_constrained

theorem card_of_dual_constrained [Finite G] (x : G) (hx : x ≠ 0) :    2 * Nat.card { φ: G →+ ZMod 2 | φ x = 1 } = Nat.card G := by  suffices h_eq_card :      Nat.card {φ : G →+ ZMod 2 | φ x = 1} = Nat.card {φ : G →+ ZMod 2 | φ x = 0} by    have h_eq_card :        Nat.card {φ : G →+ ZMod 2 | φ x = 1} + Nat.card {φ : G →+ ZMod 2 | φ x = 0} =          Nat.card (G →+ ZMod 2) := by      -- These two sets partition the set of all homomorphisms from $G$ to $\mathbb{Z}/2\mathbb{Z}$.      trans Nat.card (Set.univ : Set (G →+ ZMod 2))      · -- Since these two sets partition the set of all homomorphisms from $G$ to        -- $\mathbb{Z}/2\mathbb{Z}$, their cardinalities add up to the cardinality of the whole set.        have h_partition : {φ : G →+ ZMod 2 | φ x = 1} ∪ {φ : G →+ ZMod 2 | φ x = 0} = .univ := by          ext f          simp only [Set.mem_union, Set.mem_setOf_eq, Set.mem_univ, iff_true]          set y := f x          clear_value y          fin_cases y          all_goals simp; tauto        have _ := DFunLike.finite (G →+ ZMod 2)        rw [← h_partition, Nat.card_congr <| Equiv.Set.union <| Set.disjoint_left.mpr <| by          simp +contextual]        simp [Nat.card, Cardinal.toNat_add]      · simp    -- Since there are $|G|$ homomorphisms in total, we have $|G| = |H_1| + |H_0|$.    simp_all only [ne_eq, Set.coe_setOf, card_of_dual]    rw [← h_eq_card]; ring  -- Let $y$ be an additive character of $G$ such that $y(x) = 1$.  obtain ⟨y, hy⟩ : ∃ (y : G →+ ZMod 2), y x = 1 := by    -- Since $G$ is finite, there exists $y : G →+ ZMod 2$ such that    -- $\forall z, y z = \sum_{z \in \{x\}} z$. Let's choose any such $y$.    set y := (Basis.ofVectorSpace (ZMod 2) G).equivFun.toLinearMap.toAddMonoidHom;    -- Since $x \neq 0$, there exists an index $i$ such that $y(x)(i) = 1$ by definition of $y$.    -- In particular, there exists an index $i$ such that $repr x i = 1$.    obtain ⟨i, hi⟩ : ∃ i : Basis.ofVectorSpaceIndex (ZMod 2) G, (y x : _) i = 1 := by      have h_exists_i : ∃ i, (Basis.ofVectorSpace (ZMod 2) G).repr x i ≠ 0 := by        contrapose! hx        apply Basis.ofVectorSpace (ZMod 2) G |> Basis.ext_elem        simp [hx]      exact h_exists_i.imp fun _ hi ↦ (Fin.exists_fin_two.mp ⟨_, rfl⟩).resolve_left hi    -- Define $f : G →+ ZMod 2$ by $f(z) = y(z)(i)$ for all $z \in G$.    set f : G →+ ZMod 2 := (Pi.evalAddMonoidHom (fun _ => ZMod 2) i).comp y    exact ⟨f, hi⟩  -- By definition of $y$, we know that $y$ is a bijection between the set of additive characters  -- that map $x$ to 1 and the set of additive characters that map $x$ to 0.  apply Nat.card_congr  refine Equiv.ofBijective (⟨· - y, by aesop⟩) ⟨fun _ ↦ by grind, fun ⟨b, hb⟩ ↦ ?_⟩;  rw [Subtype.exists]  use b + y  aesop