\begin{lemma}[Hahn-Banach type theorem]\label{hb-thm}\lean{hahn_banach}\leanok  Let $H_0$ be a subgroup of $G$.  Then every homomorphism $\phi: H_0 \to G'$ can be extended to a homomorphism $\tilde \phi: G \to G'$.
\end{lemma}
\begin{proof}\leanok  By induction it suffices to treat the case where $H_0$ has index $2$ in $G$, but then the extension can be constructed by hand.
\end{proof}
lemma hahn_banach (H₀ : AddSubgroup G) (φ : H₀ →+ G') : ∃ (φ' : G →+ G'), ∀ x : H₀, φ x = φ' x := by
  let H₀ := AddSubgroup.toZModSubmodule 2 H₀
  let φ := (show H₀ →+ G' from φ).toZModLinearMap 2
  obtain ⟨φ', hφ'⟩ := φ.exists_extend
  use φ'; intro x; show φ x = φ'.comp H₀.subtype x; rw [hφ']

/-- Let $H$ be a subgroup of $G \times G'$. Then there exists a subgroup $H_0$ of $G$, a
subgroup $H_1$ of $G'$, and a homomorphism $\phi: G \to G'$ such that
$$ H := \{ (x, \phi(x) + y): x \in H_0, y \in H_1 \}.$$
In particular, $|H| = |H_0| |H_1|$. -/