\begin{corollary}\label{pfr-9-aux}\lean{better_PFR_conjecture_aux0}\leanok
If $|A+A| \leq K|A|$, then there exists a subgroup $H$ and $t\in G$ such that
$|A \cap (H+t)| \geq K^{-4} \sqrt{|A||H|}$, and $|H|/|A|\in[K^{-8},K^8]$.
\end{corollary}
\begin{proof}\leanok
  \uses{pfr-rho,rho-init,rho-subgroup}
  Apply \Cref{pfr-rho} on $U_A,U_A$ to get a subspace such that $2\rho(U_H)\le 2\rho(U_A)+8d[U_A;U_A]$. Recall that $d[U_A;U_A]\le \log K$ as proved in \Cref{pfr_aux}, and $\rho(U_A)=0$ by \Cref{rho-init}. Therefore $\rho(U_H)\le 4\log(K)$. The claim then follows from \Cref{rho-subgroup}.
\end{proof}
lemma better_PFR_conjecture_aux0 {A : Set G} (h₀A : A.Nonempty) {K : ℝ}
    (hA : Nat.card (A + A) ≤ K * Nat.card A) :
    ∃ (H : Submodule (ZMod 2) G) (t : G),
    K ^ (-4 : ℤ) * Nat.card A ^ (1 / 2 : ℝ) * Nat.card H ^ (1 / 2 : ℝ) ≤ Nat.card ↑(A ∩ (H + {t})) ∧
      Nat.card A ≤ K ^ 8 * Nat.card H ∧ Nat.card H ≤ K ^ 8 * Nat.card A := by
  have A_fin : Finite A := by infer_instance
  classical
  let mG : MeasurableSpace G := ⊤
  have : MeasurableSingletonClass G := ⟨λ _ ↦ trivial⟩
  obtain ⟨A_pos, -, K_pos⟩ : (0 : ℝ) < Nat.card A ∧ (0 : ℝ) < Nat.card (A + A) ∧ 0 < K :=
    PFR_conjecture_pos_aux' h₀A hA
  let A' := A.toFinite.toFinset
  have h₀A' : Finset.Nonempty A' := by
    simp [A', Finset.Nonempty]
    exact h₀A
  have hAA' : A' = A := Finite.coe_toFinset (toFinite A)
  rcases exists_isUniform_measureSpace A' h₀A' with ⟨Ω₀, mΩ₀, UA, hP₀, UAmeas, UAunif, -⟩
  rw [hAA'] at UAunif
  have hadd_sub : A + A = A - A := by ext; simp [Set.mem_add, Set.mem_sub, ZModModule.sub_eq_add]
  rw [hadd_sub] at hA
  have : d[UA # UA] ≤ log K := rdist_le_of_isUniform_of_card_add_le h₀A hA UAunif UAmeas
  rw [← hadd_sub] at hA
  -- entropic PFR gives a subgroup `H` which is close to `A` for the rho functional
  rcases rho_PFR_conjecture UA UA UAmeas UAmeas A' h₀A'
    with ⟨H, Ω₁, mΩ₁, UH, hP₁, UHmeas, UHunif, hUH⟩
  have ineq : ρ[UH # A'] ≤ 4 * log K := by
    rw [← hAA'] at UAunif
    have : ρ[UA # A'] = 0 := rho_of_uniform UAunif UAmeas h₀A'
    linarith
  set r := 4 * log K with hr
  have J : K ^ (-4 : ℤ) = exp (-r) := by
    rw [hr, ← neg_mul, mul_comm, exp_mul, exp_log K_pos]
    norm_cast
  have J' : K ^ 8 = exp (2 * r) := by
    have : 2 * r = 8 * log K := by ring
    rw [this, mul_comm, exp_mul, exp_log K_pos]
    norm_cast
  rw [J, J']
  refine ⟨H, ?_⟩
  have Z := rho_of_submodule UHunif h₀A' UHmeas r ineq
  have : Nat.card A = Nat.card A' := by simp [← hAA']
  have I t : t +ᵥ (H : Set G) = (H : Set G) + {t} := by
    ext z; simp [mem_vadd_set_iff_neg_vadd_mem, add_comm]
  simp_rw [← I]
  convert Z
  exact hAA'.symm

/-- Auxiliary statement towards the polynomial Freiman-Ruzsa (PFR) conjecture: if $A$ is a subset of
an elementary abelian 2-group of doubling constant at most $K$, then there exists a subgroup $H$
such that $A$ can be covered by at most $K^5 |A|^{1/2} / |H|^{1/2}$ cosets of $H$, and $H$ has
the same cardinality as $A$ up to a multiplicative factor $K^8$. -/