approx_hom_pfr

theorem approx_hom_pfr (f : G → G') (K : ℝ) (hK : K > 0)    (hf : K⁻¹ ≤ Finset.dens {x : G × G | f (x.1 + x.2) = f x.1 + f x.2}) :    ∃ (φ : G →+ G') (c : G'), Nat.card {x | f x = φ x + c} ≥ Nat.card G / (2 ^ 144 * K ^ 122) := by  cases nonempty_fintype G'  classical  let A := (Set.univ.graphOn f).toFinite.toFinset  have hA : #A = Nat.card G := by rw [Set.Finite.card_toFinset]; simp [← Nat.card_eq_fintype_card]  have hA_nonempty : A.Nonempty := by simp [-Set.Finite.toFinset_setOf, A]  have : #{x : G × G | f (x.1 + x.2) = f x.1 + f x.2} = #({ab ∈ A ×ˢ A | ab.1 + ab.2 ∈ A}) := by    rw [← Nat.card_eq_finsetCard, ← Finset.coe_sort_coe, Finset.coe_filter,      Set.Finite.toFinset_prod]    simp only [Set.Finite.mem_toFinset, A, Set.graphOn_prod_graphOn]    rw [← Set.natCard_graphOn _ (Prod.map f f), Nat.card_eq_card_finite_toFinset (Set.toFinite _),      ← Finset.card_image_of_injOn (Equiv.prodProdProdComm G G' G G').injective.injOn]    congr    aesop  have := calc    (A.dens ^ 3 / K ^ 2 : ℝ)      = A.dens ^ 3 * K⁻¹ ^ 2 := by ring    _ ≤ A.dens ^ 3 * Finset.dens {x : G × G | f (x.1 + x.2) = f x.1 + f x.2} ^ 2 := by gcongr    _ = {ab ∈ A ×ˢ A | ab.1 + ab.2 ∈ A}.dens ^ 2 / A.dens := by simp [dens, hA, this]; field_simp    _ ≤ E[A] := by field_simp; norm_cast; exact card_sq_le_card_mul_addEnergy' ..  obtain ⟨A', hA', hA'1, hA'2⟩ :=    BSG_self' (sq_nonneg K) hA_nonempty (by simpa only [inv_mul_eq_div] using this)  clear hf this  replace hA'1 : (2 ^ 4)⁻¹ * (K ^ 2)⁻¹ * #A ≤ #A' := by    simp [dens] at hA'1; field_simp at ⊢ hA'1; assumption  have hA'₀ : A'.Nonempty := Finset.card_pos.1 <| Nat.cast_pos.1 <| hA'1.trans_lt' <| by positivity  have : (A' - A').card = (A' + A' : Set (G × G')).ncard := by    simp [← Finset.coe_sub, sumset_eq_sub]  replace : (A' + A' : Set (G × G')).ncard ≤ 2 ^ 14 * K ^ 12 * (A' : Set (G × G')).ncard := by    rewrite [← this]    simp [dens] at hA'2    field_simp at hA'2    simpa [← pow_mul] using hA'2  obtain ⟨H, c, hc_card, hH_le, hH_ge, hH_cover⟩ := better_PFR_conjecture_aux hA'₀ this  clear hA'2 hH_le hH_ge  obtain ⟨H₀, H₁, φ, hH₀H₁, hH₀H₁_card⟩ := goursat H  have h_le_H₀ : (A' : Set (G × G')).ncard ≤ Nat.card c * Nat.card H₀ := by    have h_le := Set.ncard_mono (Set.image_mono (f := Prod.fst) hH_cover)    have h_proj_A'' : (Prod.fst '' (A' : Set (G × G'))).ncard = (A' : Set (G × G')).ncard :=      (Set.fst_injOn_graph.mono (Set.Finite.subset_toFinset.mp hA')).ncard_image    have h_proj_c : Prod.fst '' (c + H : Set (G × G')) = (Prod.fst '' c) + H₀ := by      ext x ; constructor <;> intro hx      · obtain ⟨x, ⟨⟨c, hc, h, hh, hch⟩, hx⟩⟩ := hx        rewrite [← hx]        exact ⟨c.1, Set.mem_image_of_mem Prod.fst hc, h.1, ((hH₀H₁ h).mp hh).1,          (Prod.ext_iff.mp hch).1⟩      · obtain ⟨_, ⟨c, hc⟩, h, hh, hch⟩ := hx        refine ⟨c + (h, φ h), ⟨⟨c, hc.1, (h, φ h), ?_⟩, by rwa [← hc.2] at hch⟩⟩        exact ⟨(hH₀H₁ ⟨h, φ h⟩).mpr ⟨hh, by rw [sub_self]; apply zero_mem⟩, rfl⟩    rewrite [h_proj_A'', h_proj_c] at h_le    apply (h_le.trans Set.natCard_add_le).trans    gcongr    · exact Finite.card_image_le Prod.fst    · exact Nat.card_le_card_of_injective (fun ⦃a₁⦄ ↦ a₁) fun ⦃a₁ a₂⦄ a ↦ a  have hH₀_pos : (0 : ℝ) < Nat.card H₀ := Nat.cast_pos.mpr Nat.card_pos  have h_le_H₁ : (Nat.card H₁ : ℝ) ≤ Nat.card c * Nat.card H / (A' : Set (G × G')).ncard := calc    _ = (Nat.card H : ℝ) / Nat.card H₀ :=      (eq_div_iff <| ne_of_gt <| hH₀_pos).mpr <| by rw [mul_comm, ← Nat.cast_mul, hH₀H₁_card]    _ ≤ (Nat.card c : ℝ) * Nat.card H / (A' : Set (G × G')).ncard := by      nth_rewrite 1 [← mul_one (Nat.card H : ℝ), mul_comm (Nat.card c : ℝ)]      repeat rewrite [mul_div_assoc]      refine mul_le_mul_of_nonneg_left ?_ (Nat.cast_nonneg _)      refine le_of_mul_le_mul_right ?_ hH₀_pos      refine le_of_mul_le_mul_right ?_ (by simpa : (0 : ℝ) < (A' : Set (G × G')).ncard)      rewrite [div_mul_cancel₀ 1, mul_right_comm, one_mul, div_mul_cancel₀, ← Nat.cast_mul]      · exact Nat.cast_le.mpr h_le_H₀      · simpa      · exact ne_of_gt hH₀_pos  clear h_le_H₀ hH₀_pos hH₀H₁_card  let translate (c : G × G') (h : G') : Set (G × G') := A' ∩ ({c} + {(0, h)} + Set.univ.graphOn φ)  have h_translate (c : G × G') (h : G') :      Prod.fst '' translate c h ⊆ { x : G | f x = φ x + (-φ c.1 + c.2 + h) } := by    intro x hx    obtain ⟨x, ⟨hxA'', _, ⟨c', hc, h', hh, hch⟩, x', hx, hchx⟩, hxx⟩ := hx    change f _ = φ _ + (-φ c.1 + c.2 + h)    replace := by simpa [-Set.Finite.toFinset_setOf, A] using hA' hxA''    rewrite [← hxx, this, ← hchx, ← hch, hc, hh]    change c.2 + h + x'.2 = φ (c.1 + 0 + x'.1) + (-φ c.1 + c.2 + h)    replace : φ x'.1 = x'.2 := (Set.mem_graphOn.mp hx).2    rw [map_add, map_add, map_zero, add_zero, this, add_comm (φ c.1), add_assoc x'.2,      ← add_assoc (φ c.1), ← add_assoc (φ c.1), ← sub_eq_add_neg, sub_self, zero_add, add_comm]  have h_translate_card c h : Nat.card (translate c h) = Nat.card (Prod.fst '' translate c h) :=    Nat.card_congr (Equiv.Set.imageOfInjOn Prod.fst (translate c h) <|      Set.fst_injOn_graph.mono fun _ hx ↦ Set.Finite.subset_toFinset.mp hA' hx.1)  let cH₁ := (c ×ˢ H₁).toFinite.toFinset  replace hc : c.Nonempty := by    obtain ⟨x, hx, _, _, _⟩ := hH_cover hA'₀.choose_spec    exact ⟨x, hx⟩  replace : A' = Finset.biUnion cH₁ fun ch ↦ (translate ch.1 ch.2).toFinite.toFinset := by    ext x ; constructor <;> intro hx    · obtain ⟨c', hc, h, hh, hch⟩ := hH_cover hx      refine Finset.mem_biUnion.mpr ⟨(c', h.2 - φ h.1), ?_⟩      refine ⟨(Set.Finite.mem_toFinset _).mpr ⟨hc, ((hH₀H₁ h).mp hh).2⟩, ?_⟩      refine (Set.Finite.mem_toFinset _).mpr ⟨hx, c' + (0, h.2 - φ h.1), ?_⟩      refine ⟨⟨c', rfl, (0, h.2 - φ h.1), rfl, rfl⟩, (h.1, φ h.1), ⟨h.1, by simp⟩, ?_⟩      beta_reduce      rewrite [add_assoc]      change c' + (0 + h.1, h.2 - φ h.1 + φ h.1) = x      rewrite [zero_add, sub_add_cancel]      exact hch    · obtain ⟨ch, hch⟩ := Finset.mem_biUnion.mp hx      exact ((Set.Finite.mem_toFinset _).mp hch.2).1  replace : ∑ _ ∈ cH₁, ((2 ^ 4)⁻¹ * (K ^ 2)⁻¹ * #A / cH₁.card : ℝ) ≤      ∑ ch ∈ cH₁, ((translate ch.1 ch.2).toFinite.toFinset.card : ℝ) := by    rewrite [Finset.sum_const, nsmul_eq_mul, ← mul_div_assoc, mul_div_right_comm, div_self, one_mul]    · apply hA'1.trans      norm_cast      exact (congrArg Finset.card this).trans_le Finset.card_biUnion_le    · symm      refine ne_of_lt <| Nat.cast_zero.symm.trans_lt <| Nat.cast_lt.mpr <| Finset.card_pos.mpr ?_      exact (Set.Finite.toFinset_nonempty _).mpr <| hc.prod H₁.nonempty  obtain ⟨c', h, hch⟩ : ∃ c' : G × G', ∃ h : G', (2 ^ 4 : ℝ)⁻¹ * (K ^ 2)⁻¹ * #A / cH₁.card ≤      Nat.card { x : G | f x = φ x + (-φ c'.1 + c'.2 + h) } := by    obtain ⟨ch, hch⟩ :=      Finset.exists_le_of_sum_le ((Set.Finite.toFinset_nonempty _).mpr (hc.prod H₁.nonempty)) this    refine ⟨ch.1, ch.2, hch.2.trans ?_⟩    rewrite [Set.Finite.card_toFinset, ← Nat.card_eq_fintype_card, h_translate_card]    exact Nat.cast_le.mpr <| Nat.card_mono (Set.toFinite _) (h_translate ch.1 ch.2)  clear! hA' hA'1 hH_cover hH₀H₁ translate h_translate h_translate_card  use φ, -φ c'.1 + c'.2 + h  calc    Nat.card G / (2 ^ 144 * K ^ 122)    _ = Nat.card G / (2 ^ 4 * K ^ 2 * (2 ^ 140 * K ^ 120)) := by ring    _ ≤ Nat.card G / (2 ^ 4 * K ^ 2 * #(c ×ˢ H₁).toFinite.toFinset) := ?_    _ = (2 ^ 4)⁻¹ * (K ^ 2)⁻¹ * ↑(#A) / ↑(#cH₁) := by rw [hA, ← mul_inv, inv_mul_eq_div, div_div]    _ ≤ _ := hch  have := (c ×ˢ H₁).toFinite.toFinset_nonempty.2 (hc.prod H₁.nonempty)  gcongr  calc    (#(c ×ˢ H₁).toFinite.toFinset : ℝ)    _ = #c.toFinite.toFinset * #(H₁ : Set G').toFinite.toFinset := by      rw [← Nat.cast_mul, ← Finset.card_product, Set.Finite.toFinset_prod]    _ = Nat.card c * Nat.card H₁ := by      simp_rw [Set.Finite.card_toFinset, ← Nat.card_eq_fintype_card]; norm_cast    _ ≤ Nat.card c * (Nat.card c * Nat.card H / (A' : Set (G × G')).ncard) := by gcongr    _ = Nat.card c ^ 2 * Nat.card H / (A' : Set (G × G')).ncard := by ring    _ ≤ ((2 ^ 14 * K ^ 12) ^ 5 * (A' : Set (G × G')).ncard ^ (1 / 2 : ℝ) *      Nat.card H ^ (-1 / 2 : ℝ)) ^ 2 * Nat.card H / (A' : Set (G × G')).ncard := by      gcongr; exact hc_card    _ = 2 ^ 140 * K ^ 120 := by rpow_simp; simp [-Nat.card_eq_fintype_card]; field_simp; norm_num