approx_hom_pfr'

theorem approx_hom_pfr' [Finite G] (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'), Nat.card {x | f x = φ'' x} ≥ (Nat.card G / (2 ^ 144 * K ^ 122) - 1)/2 := by  obtain ⟨ φ, c, h ⟩ := approx_hom_pfr f K hK hf  set A := { x | f x = φ x + c }  obtain ⟨ φ', h' ⟩ := card_of_slice A  let φ'c : G →+ G' := {    toFun x := (φ' x) • c    map_add' := by intros; simp [add_smul]    map_zero' := by simp  }  use φ + φ'c  rw [ge_iff_le, div_le_iff₀ (by norm_num)]  calc    _ ≤ Nat.card A - (1:ℝ) := by gcongr    _ ≤ (Nat.card ↑A - 1:ℕ) := by norm_cast; convert Int.le_natCast_sub _ _; norm_cast    _ ≤ 2 * Nat.card ↑{x | x ∈ A ∧ φ' x = 1} := by norm_cast    _ ≤ _ := by      rw [mul_comm]; gcongr      apply Nat.card_mono      · apply Set.toFinite      intro x      simp only [Set.mem_setOf_eq, AddMonoidHom.add_apply, AddMonoidHom.coe_mk,        ZeroHom.coe_mk, and_imp, A, φ'c]      intro h1 h2      simp [h1, h2]