better_PFR_conjecture_aux0

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 : ℝ) * (H : Set G).ncard ^ (1 / 2 : ℝ)        ≤ Nat.card ↑(A ∩ (H + {t})) ∧      Nat.card A ≤ K ^ 8 * (H : Set G).ncard ∧ (H : Set G).ncard ≤ K ^ 8 * Nat.card A := by  have A_fin : Finite A := by infer_instance  classical  let mG : MeasurableSpace G := ⊤  have : MeasurableSingletonClass G := ⟨fun _ ↦ trivial⟩  obtain ⟨A_pos, -, K_pos⟩ : (0 : ℝ) < Nat.card A ∧ (0 : ℝ) < Nat.card (A + A) ∧ 0 < K :=    PFR_conjecture_pos_aux' (Set.toFinite _) h₀A hA  let A' := A.toFinite.toFinset  have h₀A' : Finset.Nonempty A' := by simpa [A', Finset.Nonempty]  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