conclusion_transfers

lemma conclusion_transfers {A B : Set G} (G' : AddSubgroup G) (A' B' : Set (G' : Set G))    (hA : IsShift A A') (hB : IsShift B B') [Finite A'] [Finite B']    (hA' : A'.Nonempty) (hB' : B'.Nonempty)    (h : WeakPFRAsymmConclusion A' B') : WeakPFRAsymmConclusion A B := by  have : Nonempty A' := hA'.to_subtype  have : Nonempty B' := hB'.to_subtype  rcases h with ⟨A'', B'', hA'', hB'', hA''_non, hB''_non, hcard_ineq, hdim_ineq⟩  rcases hA with ⟨x, hA⟩  set f : G' → G := fun a ↦ (a : G) + x  have hf : Injective f := by simp [Injective, f]  have hA' : A = f '' A' := by    simp_rw [hA, ← Set.image_vadd, Set.image_image, vadd_eq_add, f, add_comm]; rfl  rcases hB with ⟨y, hB⟩  set g : G' → G := fun a ↦ (a : G) + y  have hg : Injective g := by simp [Injective, g]  have hB' : B = g '' B' := by    simp_rw [hB, ← Set.image_vadd, Set.image_image, vadd_eq_add, g, add_comm]; rfl  use f '' A'', g '' B''  have : dᵤ[A # B] = dᵤ[A' # B'] := by    rw [← setRuzsaDist_of_inj _ _ (φ := G'.subtype) Subtype.val_injective,      ← setRuzsaDist_add_const (G'.subtype '' A') (G'.subtype '' B') x y]    congr    · rw [hA]      ext y      simp [Set.mem_vadd_set_iff_neg_vadd_mem, add_comm]    · rw [hB]      ext x      simp [Set.mem_vadd_set_iff_neg_vadd_mem, add_comm]  refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩  · simp [hA', hf, hA'']  · simp [hB', hg, hB'']  · simp [hA''_non]  · simp [hB''_non]  · convert hcard_ineq using 2    · congr 3      · rw [hA', Nat.card_image_of_injective hf]      · rw [hB', Nat.card_image_of_injective hg]      · rw [Nat.card_image_of_injective hf]      rw [Nat.card_image_of_injective hg]  · convert! LE.le.trans _ hdim_ineq using 2    norm_cast    apply max_le_max    · exact (dimension_of_shift A'' x).le    · exact (dimension_of_shift B'' y).le