Torsion PFR

theorem torsion_PFR {G : Type*} [AddCommGroup G] [Finite G] {m : ℕ} (hm : m ≥ 2)     (htorsion : ∀ x:G, m • x = 0) {A : Set G} [Finite A] {K : ℝ} (h₀A : A.Nonempty)     (hA : Nat.card (A + A) ≤ K * A.ncard) :     ∃ (H : AddSubgroup G) (c : Set G),      Nat.card c < m * K ^ (256*m^3+1) ∧ (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' ‹_› h₀A hA   -- consider the subgroup `H` given by Lemma `torsion_PFR_conjecture_aux`.  obtain ⟨H, c, hc, IHA, IAH, A_subs_cH⟩ : ∃ (H : AddSubgroup G) (c : Set G),    Nat.card c ≤ K ^ (128 * m^3+1) * A.ncard ^ (1/2:ℝ) * (H : Set G).ncard ^ (-1/2:ℝ)      ∧ (H : Set G).ncard ≤ K ^ (256*m^3) * A.ncard ∧ A.ncard ≤ K ^ (256*m^3) * (H : Set G).ncard      ∧ A ⊆ c + H :=    torsion_PFR_conjecture_aux hm htorsion 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 ^ ((128*m^3+1)) * A.ncard ^ (1/2:ℝ) * (H : Set G).ncard ^ (-1/2:ℝ) := hc    _ ≤ K ^ (128 * m ^ 3 + 1) * (K ^ (256 * m ^ 3) * (H : Set G).ncard) ^ (1/2 : ℝ) *          (H : Set G).ncard ^ (-1/2:ℝ) := by gcongr    _ = K ^ (256*m^3+1) := by      rpow_ring; norm_num      simp_rw [←Real.rpow_natCast]      rw [←Real.rpow_mul (by positivity), ←Real.rpow_add (by positivity)]      congr; push_cast; ring    _ < m * K ^ (256*m^3+1) := by      apply (lt_mul_iff_one_lt_left _).mpr      · norm_num; linarith [hm]      positivity  -- otherwise, we decompose `H` into cosets of one of its subgroups `H'`, chosen so that  -- `#A / m < #H' ≤ #A`. This `H'` satisfies the desired conclusion.  · obtain ⟨H', IH'A, IAH', H'H⟩ : ∃ H' : AddSubgroup G, (H' : Set G).ncard ≤ A.ncard          ∧ A.ncard < m * (H' : Set G).ncard ∧ H' ≤ H := by      have A_pos' : 0 < A.ncard := mod_cast A_pos      exact torsion_exists_subgroup_subset_card_le hm htorsion H h.le A_pos'.ne'    have : (A.ncard / m : ℝ) < (H' : Set G).ncard := by      rw [div_lt_iff₀, mul_comm]      · norm_cast      norm_cast; exact Nat.zero_lt_of_lt hm    have H'_pos : (0 : ℝ) < (H' : Set G).ncard := by      have : 0 < (H' : Set G).ncard := Nat.card_pos; positivity    obtain ⟨u, HH'u, hu⟩ := AddSubgroup.exists_left_transversal_of_le H'H    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 Set.natCard_add_le    _ ≤ (K ^ ((128*m^3+1)) * 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 ^ ((128*m^3+1)) * A.ncard ^ (1 / 2:ℝ) * ((H : Set G).ncard ^ (-1 / 2:ℝ)))          * ((H : Set G).ncard / (A.ncard / m)) := by        gcongr    _ = (K ^ ((128*m^3+1)) * A.ncard ^ (1 / 2:ℝ) * ((H : Set G).ncard ^ (-1 / 2:ℝ)))          * ((H : Set G).ncard * (A.ncard : ℝ)⁻¹ * m) := by        field_simp    _ = m * K ^ ((128*m^3+1)) * A.ncard ^ (-1/2:ℝ) * (H : Set G).ncard ^ (1/2:ℝ) := by        rpow_ring        field_simp        norm_num    _ ≤ m * K ^ ((128*m^3+1)) * A.ncard ^ (-1/2:ℝ) * (K ^ (256*m^3) * A.ncard) ^ (1/2:ℝ) := by        gcongr    _ = m * K ^ (256*m^3+1) := by        rpow_ring        norm_num        left        simp_rw [←Real.rpow_natCast]        rw [←Real.rpow_mul (by positivity), ←Real.rpow_add (by positivity)]        congr; push_cast; ring