\begin{theorem}\label{weak-pfr-int}\lean{weak_PFR_int}\leanok
Let $A\subseteq \mathbb{Z}^d$ and $\lvert A-A\rvert\leq K\lvert A\rvert$.
There exists $A'\subseteq A$ such that $\lvert A'\rvert \geq K^{-17}\lvert
A\rvert$ and $\dim A' \leq \frac{40}{\log 2}\log K$.
\end{theorem}
\begin{proof}\leanok
\uses{weak-pfr-symm,dimension-def}
As in the beginning of \Cref{pfr} the doubling condition forces $d[U_A;U_A]\leq \log K$, and then we apply \Cref{weak-pfr-symm}.
\end{proof}
theorem weak_PFR_int
    {G : Type*} [AddCommGroup G] [Module.Free ℤ G] [Module.Finite ℤ G]
    {A : Set G} [A_fin : Finite A] (hnA : A.Nonempty) {K : ℝ}
    (hA : Nat.card (A-A) ≤ K * Nat.card A) :
    ∃ A' : Set G, A' ⊆ A ∧ Nat.card A' ≥ K ^ (-17 : ℝ) * Nat.card A ∧
      AffineSpace.finrank ℤ A' ≤ (40 / log 2) * log K := by
  have : Nonempty (A - A) := (hnA.sub hnA).coe_sort
  have : Finite (A - A) := Set.Finite.sub A_fin A_fin
  have hK : 0 < K := by
    have : 0 < K * Nat.card A := lt_of_lt_of_le (mod_cast Nat.card_pos) hA
    nlinarith
  have : Countable G := countable_of_finiteDimensional ℤ G
  let m : MeasurableSpace G := ⊤
  apply weak_PFR hnA hK ((setRuzsaDist_le A A hnA hnA).trans _)
  suffices log (Nat.card (A-A)) ≤ log K + log (Nat.card A) by linarith
  rw [← log_mul (by positivity) _]
  · apply log_le_log _ hA
    norm_cast
    exact Nat.card_pos
  exact_mod_cast ne_of_gt (@Nat.card_pos _ hnA.to_subtype _)