PFR_conjecture'

theorem PFR_conjecture' {G : Type*} [AddCommGroup G] [Module (ZMod 2) G]    {A : Set G} {K : ℝ} (hA₀ : A.Nonempty) (Afin : A.Finite)    (hA : (A + A).ncard ≤ K * A.ncard) :    ∃ (H : Submodule (ZMod 2) G) (c : Set G), c.Finite ∧ (H : Set G).Finite ∧      Nat.card c < 2 * K ^ 12 ∧ (H : Set G).ncard ≤ A.ncard ∧ A ⊆ c + H := by  let G' := Submodule.span (ZMod 2) A  let G'fin : Fintype G' := (Afin.submoduleSpan _).fintype  let ι : G'→ₗ[ZMod 2] G := G'.subtype  have ι_inj : Injective ι := G'.toAddSubgroup.subtype_injective  let A' : Set G' := ι ⁻¹' A  have A_rg : A ⊆ range ι := by simp [G', ι]  have cardA' : Nat.card A' = A.ncard := Nat.card_preimage_of_injective ι_inj A_rg  have hA' : Nat.card (A' + A') ≤ K * Nat.card A' := by    rwa [cardA', ← preimage_add _ ι_inj A_rg A_rg,         Nat.card_preimage_of_injective ι_inj (add_subset_range _ A_rg A_rg)]  rcases PFR_conjecture (hA₀.preimage' A_rg) hA' with ⟨H', c', hc', hH', hH'₂⟩  refine ⟨H'.map ι , ι '' c', toFinite _, toFinite (ι '' H'), ?_, ?_, fun x hx ↦ ?_⟩  · rwa [Nat.card_image_of_injective ι_inj]  · simpa [Set.ncard_image_of_injective _ ι_inj, ← cardA']  · erw [← image_add]    exact ⟨⟨x, Submodule.subset_span hx⟩, hH'₂ hx, rfl⟩