weak_PFR_asymm

lemma weak_PFR_asymm (A B : Set G) [Finite A] [Finite B] (hA : A.Nonempty) (hB : B.Nonempty) :    WeakPFRAsymmConclusion A B := by  let P (M : ℕ) : Prop := ∀ (G : Type _) (hG_comm : AddCommGroup G) (_hG_free : Module.Free ℤ G)    (_hG_fin : Module.Finite ℤ G) (_hG_count : Countable G) (hG_mes : MeasurableSpace G)    (_hG_sing : MeasurableSingletonClass G) (A B : Set G) (_hA_fin : Finite A) (_hB_fin : Finite B)    (_hA_non : A.Nonempty) (_hB_non : B.Nonempty)    (_hM : Nat.card A + Nat.card B ≤ M), WeakPFRAsymmConclusion A B  suffices ∀ M, (∀ M', M' < M → P M') → P M by    set M := Nat.card A + Nat.card B    have hM : Nat.card A + Nat.card B ≤ M := Nat.le_refl _    convert (Nat.strong_induction_on (p := P) M this) G ‹_› ‹_› ‹_› ‹_› _ ‹_› A B ‹_› ‹_› ‹_› ‹_› hM  intro M h_induct  -- wlog we can assume A, B are not in cosets of a smaller subgroup  suffices ∀ (G : Type _) (hG_comm : AddCommGroup G) (_hG_free : Module.Free ℤ G)    (_hG_fin : Module.Finite ℤ G) (_hG_count : Countable G) (hG_mes : MeasurableSpace G)    (_hG_sing : MeasurableSingletonClass G) (A B : Set G) (_hA_fin : Finite A) (_hB_fin : Finite B)      (_hA_non : A.Nonempty) (_hB_non : B.Nonempty) (_hM : Nat.card A + Nat.card B ≤ M)    (_hnot : NotInCoset A B), WeakPFRAsymmConclusion A B by    intro G hG_comm hG_free hG_fin hG_count hG_mes hG_sing A B hA_fin hB_fin hA_non hB_non hM    obtain ⟨G', A', B', hAA', hBB', hnot'⟩ := wlog_notInCoset hA_non hB_non    have hG'_fin : Module.Finite ℤ G' :=      Module.Finite.iff_fg (N := AddSubgroup.toIntSubmodule G').2 (IsNoetherian.noetherian _)    have hG'_free : Module.Free ℤ G' := by      rcases Submodule.nonempty_basis_of_pid (Module.Free.chooseBasis ℤ G)        (AddSubgroup.toIntSubmodule G') with ⟨n, ⟨b⟩⟩      exact Module.Free.of_basis b    have hAA'_card : Nat.card A = Nat.card A' :=      Nat.card_image_of_injective Subtype.val_injective _ ▸ hAA'.card_congr    have hBB'_card : Nat.card B = Nat.card B' :=      Nat.card_image_of_injective Subtype.val_injective _ ▸ hBB'.card_congr    have hA_non' : Nonempty A := Set.nonempty_coe_sort.mpr hA_non    have hB_non' : Nonempty B := Set.nonempty_coe_sort.mpr hB_non    rw [hAA'_card, hBB'_card] at hM    have hA'_nonfin : A'.Nonempty ∧ Finite A' := by      convert Nat.card_pos_iff.mp ?_      · exact Iff.symm nonempty_coe_sort      · simpa [hAA'_card] using Nat.card_pos (α := A)    have hB'_nonfin : B'.Nonempty ∧ Finite B' := by      convert Nat.card_pos_iff.mp ?_      · exact Iff.symm nonempty_coe_sort      · simpa [hBB'_card] using Nat.card_pos (α := B)    obtain ⟨hA'_non, hA'_fin⟩ := hA'_nonfin    obtain ⟨hB'_non, hB'_fin⟩ := hB'_nonfin    replace this := this G' _ hG'_free hG'_fin (by infer_instance) (by infer_instance)      (by infer_instance) A' B' hA'_fin hB'_fin hA'_non hB'_non hM hnot'    exact conclusion_transfers G' A' B' hAA' hBB' hA'_non hB'_non this  intro G hG_comm hG_free hG_fin hG_count hG_mes hG_sing A B hA_fin hB_fin hA_non hB_non hM hnot  obtain ⟨N, x, y, Ax, By, hAx_non, hBy_non, hAx_fin, hBy_fin, hAx, hBy, hdim, hcard⟩ :=    weak_PFR_asymm_prelim A B hA_non hB_non  have hAxA : Ax ⊆ A := by rw [hAx]; simp  have hByB : By ⊆ B := by rw [hBy]; simp  have hA_pos : (0 : ℝ) < Nat.card A := Nat.cast_pos.mpr (@Nat.card_pos _ hA_non.to_subtype _)  have hB_pos : (0 : ℝ) < Nat.card B := Nat.cast_pos.mpr (@Nat.card_pos _ hB_non.to_subtype _)  rcases lt_or_ge (Nat.card Ax + Nat.card By) (Nat.card A + Nat.card B) with h | h  · replace h := h_induct (Nat.card Ax + Nat.card By) (h.trans_le hM) G hG_comm hG_free hG_fin      hG_count hG_mes hG_sing Ax By (Set.finite_coe_iff.mpr hAx_fin) hBy_fin hAx_non hBy_non le_rfl    rcases h with ⟨A', B', hA', hB', hA'_non, hB'_non, hcard_ineq, hdim_ineq⟩    use A', B'    have hAx_fin' := Set.finite_coe_iff.mpr hAx_fin    have hBy_fin' := Set.finite_coe_iff.mpr hBy_fin    have hA'_fin' := Set.finite_coe_iff.mpr (Set.Finite.subset hAx_fin hA')    have hB'_fin' := Set.finite_coe_iff.mpr (Set.Finite.subset hBy_fin hB')    have hAx_non' := Set.nonempty_coe_sort.mpr hAx_non    have hBy_non' := Set.nonempty_coe_sort.mpr hBy_non    have hA'_non' := Set.nonempty_coe_sort.mpr hA'_non    have hB'_non' := Set.nonempty_coe_sort.mpr hB'_non    have hAx_pos : (0 : ℝ) < Nat.card Ax := Nat.cast_pos.mpr Nat.card_pos    have hBy_pos : (0 : ℝ) < Nat.card By := Nat.cast_pos.mpr Nat.card_pos    have hA'_pos : (0 : ℝ) < Nat.card A' := Nat.cast_pos.mpr Nat.card_pos    have hB'_pos : (0 : ℝ) < Nat.card B' := Nat.cast_pos.mpr Nat.card_pos    have hAxA_le : (Nat.card Ax : ℝ) ≤ Nat.card A := by gcongr; exact Nat.card_mono A.toFinite hAxA    have hByB_le : (Nat.card By : ℝ) ≤ Nat.card B := by gcongr; exact Nat.card_mono B.toFinite hByB    refine ⟨hA'.trans hAxA, hB'.trans hByB, hA'_non, hB'_non, ?_, ?_⟩    · rw [four_logs hA_pos hB_pos hA'_pos hB'_pos]      rw [four_logs hAx_pos hBy_pos hA'_pos hB'_pos] at hcard_ineq      linarith only [hcard, hcard_ineq]    apply hdim_ineq.trans    gcongr    linarith only [Real.log_le_log hAx_pos hAxA_le, Real.log_le_log hBy_pos hByB_le, hcard]  use A, B  refine ⟨Eq.subset rfl, Eq.subset rfl, hA_non, hB_non, ?_, ?_⟩  · have := hA_non.to_subtype    have := hB_non.to_subtype    apply LE.le.trans _ <| mul_nonneg (by norm_num) <| setRuzsaDist_nonneg A B    rw [div_self (by positivity)]    simp  have hAx_eq : Ax = A := by    apply Set.Finite.eq_of_subset_of_card_le A.toFinite hAxA    linarith only [h, Nat.card_mono B.toFinite hByB]  have hBy_eq : By = B := by    apply Set.Finite.eq_of_subset_of_card_le B.toFinite hByB    linarith only [h, Nat.card_mono A.toFinite hAxA]  have hN : N = ⊤ := by    have : (A-A) ∪ (B-B) ⊆ N := by      rw [← hAx_eq, ← hBy_eq, hAx, hBy]      intro z hz      simp only [mk'_apply, mem_union, mem_sub, mem_setOf_eq] at hz      refine (QuotientAddGroup.eq_zero_iff z).mp ?_      rcases hz with ⟨a, ⟨-, ha⟩, a', ⟨-, ha'⟩, haa'⟩ | ⟨b, ⟨-, hb⟩, b', ⟨-,hb'⟩, hbb'⟩      · rw [← haa']; simp [ha, ha']      rw [← hbb']; simp [hb, hb']    rw [← AddSubgroup.closure_le, hnot] at this    exact top_le_iff.mp this  have : Nat.card (G ⧸ N) = 1 := by    rw [Nat.card_eq_one_iff_unique]    constructor    · rw [hN]      exact QuotientAddGroup.subsingleton_quotient_top    infer_instance  simp only [this, Nat.cast_one, log_one, zero_add] at hdim  rw [← le_div_iff₀' (by positivity)] at hdim  convert! le_trans ?_ hdim using 1  · field_simp  simp only [Nat.cast_max, max_le_iff, Nat.cast_le]  exact ⟨AffineSpace.finrank_le_moduleFinrank, AffineSpace.finrank_le_moduleFinrank⟩