\begin{lemma}\label{pfr-projection}\lean{PFR_projection}\leanok
If $G=\mathbb{F}_2^d$ and $\alpha\in (0,1)$ and $X,Y$ are $G$-valued random
variables then there is a subgroup $H\leq \mathbb{F}_2^d$ such that
\[\log \lvert H\rvert \leq 2 (\mathbb{H}(X)+\mathbb{H}(Y))\]
and if $\psi:G \to G/H$ is the natural projection then
\[\mathbb{H}(\psi(X))+\mathbb{H}(\psi(Y))\leq 34 d[\psi(X);\psi(Y)].\]
\end{lemma}
\begin{proof}
\uses{pfr-projection'}\leanok
Specialize \Cref{pfr-projection'} to $\alpha=3/5$. In the second
inequality, it gives a bound $100/3 < 34$.
\end{proof}
lemma PFR_projection (hX : Measurable X) (hY : Measurable Y) :
    ∃ H : Submodule (ZMod 2) G, log (Nat.card H) ≤ 2 * (H[X ; μ] + H[Y;μ']) ∧
    H[H.mkQ ∘ X ; μ] + H[H.mkQ ∘ Y; μ'] ≤
      34 * d[H.mkQ ∘ X ;μ # H.mkQ ∘ Y;μ'] := by
  rcases PFR_projection' X Y μ μ' ((3 : ℝ) / 5) hX hY (by norm_num) (by norm_num) with ⟨H, h, h'⟩
  refine ⟨H, ?_, ?_⟩
  · convert h
    norm_num
  · have : 0 ≤ d[⇑H.mkQ ∘ X ; μ # ⇑H.mkQ ∘ Y ; μ'] :=
      rdist_nonneg (.comp .of_discrete hX) (.comp .of_discrete hY)
    linarith

end F2_projection

open MeasureTheory ProbabilityTheory Real Set