PFR_conjecture_improv

theorem PFR_conjecture_improv (h₀A : A.Nonempty) (hA : Nat.card (A + A) ≤ K * A.ncard) :     ∃ (H : Submodule (ZMod 2) G) (c : Set G),      Nat.card c < 2 * K ^ 11 ∧ (H : Set G).ncard ≤ A.ncard ∧ A ⊆ c + H := by  obtain ⟨A_pos, -, K_pos⟩ : (0 : ℝ) < A.ncard ∧ (0 : ℝ) < Nat.card (A + A) ∧ 0 < K :=    PFR_conjecture_pos_aux' (Set.toFinite _) h₀A hA  -- consider the subgroup `H` given by Lemma `PFR_conjecture_aux`.  obtain ⟨H, c, hc, IHA, IAH, A_subs_cH⟩ : ∃ (H : Submodule (ZMod 2) G) (c : Set G),    Nat.card c ≤ K ^ 6 * A.ncard ^ (1/2) * (H : Set G).ncard ^ (-1/2)      ∧ (H : Set G).ncard ≤ K ^ 10 * A.ncard ∧ A.ncard ≤ K ^ 10 * (H : Set G).ncard      ∧ A ⊆ c + H :=    PFR_conjecture_improv_aux h₀A hA  have H_pos : (0 : ℝ) < (H : Set G).ncard := by    have : 0 < (H : Set G).ncard := Nat.card_pos; positivity  rcases le_or_gt ((H : Set G).ncard) A.ncard with h|h  -- If `#H ≤ #A`, then `H` satisfies the conclusion of the theorem  · refine ⟨H, c, ?_, h, A_subs_cH⟩    calc    Nat.card c ≤ K ^ 6 * A.ncard ^ (1/2) * (H : Set G).ncard ^ (-1/2) := hc    _ ≤ K ^ 6 * (K ^ 10 * (H : Set G).ncard) ^ (1/2) * (H : Set G).ncard ^ (-1/2) := by      gcongr    _ = K ^ 11 := by rpow_ring; norm_num    _ < 2 * K ^ 11 := by linarith [show 0 < K ^ 11 by positivity]  -- otherwise, we decompose `H` into cosets of one of its subgroups `H'`, chosen so that  -- `#A / 2 < #H' ≤ #A`. This `H'` satisfies the desired conclusion.  · obtain ⟨H', IH'A, IAH', H'H⟩ : ∃ H' : Submodule (ZMod 2) G, (H' : Set G).ncard ≤ A.ncard          ∧ A.ncard < 2 * (H' : Set G).ncard ∧ H' ≤ H := by      have A_pos' : 0 < A.ncard := mod_cast A_pos      exact ZModModule.exists_submodule_subset_card_le Nat.prime_two H h.le A_pos'.ne'    have : (A.ncard / 2 : ℝ) < (H' : Set G).ncard := by      rw [div_lt_iff₀ zero_lt_two, mul_comm]; norm_cast    have H'_pos : (0 : ℝ) < (H' : Set G).ncard := by      have : 0 < (H' : Set G).ncard := Nat.card_pos; positivity    obtain ⟨u, HH'u, hu⟩ :=      H'.toAddSubgroup.exists_left_transversal_of_le (H := H.toAddSubgroup) H'H    dsimp at HH'u    refine ⟨H', c + u, ?_, IH'A, by rwa [add_assoc, HH'u]⟩    calc    (Nat.card (c + u) : ℝ)      ≤ Nat.card c * Nat.card u := mod_cast natCard_add_le    _ ≤ (K ^ 6 * A.ncard ^ (1 / 2) * ((H : Set G).ncard ^ (-1 / 2)))          * ((H : Set G).ncard / (H' : Set G).ncard) := by        gcongr        apply le_of_eq        rw [eq_div_iff H'_pos.ne']        norm_cast    _ < (K ^ 6 * A.ncard ^ (1 / 2) * ((H : Set G).ncard ^ (-1 / 2)))          * ((H : Set G).ncard / (A.ncard / 2)) := by        gcongr    _ = (K ^ 6 * A.ncard ^ (1 / 2) * ((H : Set G).ncard ^ (-1 / 2)))          * ((H : Set G).ncard * (A.ncard :ℝ)⁻¹ * 2) := by        field_simp    _ = 2 * (K ^ 6 * A.ncard ^ (1 / 2) * (A.ncard :ℝ)⁻¹ *          ((H : Set G).ncard ^ (-1 / 2)) * ((H : Set G).ncard)) := by        ring    _ = 2 * K ^ 6 * A.ncard ^ (-1/2) * (H : Set G).ncard ^ (1/2) := by        rpow_ring        field_simp        norm_num    _ ≤ 2 * K ^ 6 * A.ncard ^ (-1/2) * (K ^ 10 * A.ncard) ^ (1/2) := by        gcongr    _ = 2 * K ^ 11 := by        rpow_ring        norm_num