homomorphism_pfr

theorem homomorphism_pfr (f : G → G') (S : Set G') (hS : ∀ x y : G, f (x+y) - (f x) - (f y) ∈ S) :    ∃ (φ : G →+ G') (T : Set G'), Nat.card T ≤ Nat.card S ^ 10 ∧ ∀ x : G, (f x) - (φ x) ∈ T := by  cases nonempty_fintype G  cases nonempty_fintype G'  classical  have : 0 < Nat.card G := Nat.card_pos  let A := univ.graphOn f  have hA_le : (Nat.card ↥(A + A) : ℝ) ≤ Nat.card S * Nat.card A := by    let B := A - {0}×ˢS    have hAB : A + A ⊆ B := by      intro x hx      obtain ⟨a, ha, a', ha', haa'⟩ := Set.mem_add.mp hx      simp only [mem_graphOn, A] at ha ha'      rw [Set.mem_sub]      refine ⟨(x.1, f x.1), ?_, (0, f (a.1 + a'.1) - f a.1 - f a'.1), ?_⟩      · simp [A]      · simp only [singleton_prod, mem_image, Prod.mk.injEq, true_and,          exists_eq_right, Prod.mk_sub_mk, sub_zero]        exact ⟨hS a.1 a'.1,          by rw [← Prod.fst_add, ha.2, ha'.2, sub_sub, ← Prod.snd_add, haa', sub_sub_self]⟩    have hB_card : Nat.card B ≤ Nat.card S * Nat.card A :=      natCard_sub_le.trans_eq <| by simp only [mul_comm, Set.card_singleton_prod]    norm_cast    exact (Nat.card_mono (toFinite B) hAB).trans hB_card  have hA_nonempty : A.Nonempty := by simp [A]  obtain ⟨H, c, hcS, -, -, hAcH⟩ := better_PFR_conjecture_aux hA_nonempty hA_le  have : 0 < Nat.card c := by    have : c.Nonempty := by      by_contra! H      simp only [H, empty_add, subset_empty_iff] at hAcH      simp [hAcH] at hA_nonempty    exact this.natCard_pos c.toFinite  obtain ⟨H₀, H₁, φ, hH₀₁, hH_card⟩ := goursat H  have hG_card_le : Nat.card G ≤ Nat.card c * Nat.card H₀ := by    let c' := Prod.fst '' c    have hc'_card : Nat.card c' ≤ Nat.card c := Nat.card_image_le (toFinite c)    have h_fstH : Prod.fst '' (H : Set (G × G')) = H₀:= by      ext x; simpa [hH₀₁] using fun _ ↦ ⟨φ x, by simp⟩    have hG_cover : (univ : Set G) = c' + (H₀:Set G) := by      apply (eq_univ_of_forall (fun g ↦ ?_)).symm      have := image_mono (f := Prod.fst) hAcH      rw [← AddHom.coe_fst, Set.image_add, AddHom.coe_fst, image_fst_graphOn] at this      rw [← h_fstH]      exact this (mem_univ g)    apply_fun Nat.card at hG_cover    rw [Nat.card_coe_set_eq, Set.ncard_univ] at hG_cover    rw [hG_cover]    calc      Nat.card (c' + (H₀ : Set G)) ≤ Nat.card c' * Nat.card H₀ := natCard_add_le      _ ≤ Nat.card c * Nat.card H₀ := by gcongr  have : (Nat.card H₁ : ℝ) ≤ (Nat.card H / Nat.card A) * Nat.card c := by calc      (Nat.card H₁ : ℝ) = (Nat.card H : ℝ) / Nat.card H₀ := by rw [hH_card]; push_cast; field_simp      _ ≤ (Nat.card H : ℝ) / (Nat.card G / Nat.card c) := by        gcongr        rw [div_le_iff₀' (by positivity)]        exact_mod_cast hG_card_le      _ = (Nat.card H / Nat.card G : ℝ) * Nat.card c := by field_simp      _ = (Nat.card H / Nat.card A) * Nat.card c := by congr; simp [-Nat.card_eq_fintype_card, A]  let T := (fun p ↦ p.2 - φ p.1) '' (c + {0} ×ˢ (H₁: Set G'))  have :=    calc      A ⊆ c + H := hAcH      _ ⊆ c + (({0} ×ˢ (H₁ : Set G')) + {(x, φ x) | x : G}) := by        gcongr        rintro ⟨g, g'⟩ hg        simp only [SetLike.mem_coe, hH₀₁] at hg        exact ⟨(0, g' - φ g), by simp [hg.2], (g, φ g), by simp⟩      _ = ⋃ (a ∈ T), {(x, a + φ x) | x : G} := by        rw [← add_assoc, ← vadd_eq_add, ← Set.iUnion_vadd_set, Set.biUnion_image]        congr! 3 with a        rw [← range, ← range, ← graphOn_univ_eq_range, ← graphOn_univ_eq_range, vadd_graphOn_univ]  refine ⟨φ, T, ?_, ?_⟩  · have : (Nat.card T : ℝ) ≤ (Nat.card S : ℝ) ^ (10 : ℝ) := by calc      (Nat.card T : ℝ) ≤ Nat.card (c + {(0 : G)} ×ˢ (H₁ : Set G')) := by        norm_cast; apply Nat.card_image_le (toFinite _)      _ ≤ Nat.card c * Nat.card H₁ := by        norm_cast        apply natCard_add_le.trans        rw [Set.card_singleton_prod] ; rfl      _ ≤ Nat.card c * ((Nat.card H / Nat.card A) * Nat.card c) := by gcongr      _ = Nat.card c ^ 2 * (Nat.card H / Nat.card A) := by ring      _ ≤ (Nat.card S ^ 5 * Nat.card A ^ (1 / 2 : ℝ) * Nat.card H ^ (-1 / 2 : ℝ)) ^ 2          * (Nat.card H / Nat.card A) := by gcongr; exact hcS      _ = (Nat.card S : ℝ) ^ (10 : ℝ) := by        rw [← Real.rpow_two, div_eq_mul_inv, div_eq_mul_inv, div_eq_mul_inv]        have : 0 < Nat.card S := by          have : S.Nonempty := ⟨f (0 + 0) - f 0 - f 0, hS 0 0⟩          exact this.natCard_pos S.toFinite        have : 0 < Nat.card A := hA_nonempty.natCard_pos A.toFinite        have : 0 < Nat.card H := H.nonempty.natCard_pos <| toFinite _        simp_rw [← Real.rpow_natCast]        rpow_ring        norm_num    exact_mod_cast this  · intro g    specialize this (⟨g, by simp⟩ : (g, f g) ∈ A)    simp only [mem_iUnion, mem_setOf_eq, Prod.mk.injEq, exists_eq_left] at this    obtain ⟨t, ht, h⟩ := this    rw [← h]    convert ht    abel