Erdős problem 10 - grechuk

open scoped BigOperators

def CK : ℕ := 3942951359960012586542991835686376608231592127249807732373409846031135195659174148737161255930050543559319182152642816343958573976075461198274610155058226350701077796608546283231637018483208223116080559321429158623772466374556290759164277947630417236158147995116126734474452247965418364460529839644657

def CG : ℕ := 3942951359960012586542991835686376608231592127249807732373409846031135195659174148737161255930050543559319182152642816343958573976075461198274610155058226350701077796608546283231637018483208223116080561800334422176622099740983337736621316898600121619871377542107047343253864459964167331555646795960321

def CD : ℕ := 45592577

def CQ : ℕ := 487824887233

def CP (n : ℕ) : ℕ :=
  CD * ∏ i ∈ (Finset.range n).erase 10, Nat.fermatNumber i

def CL (j : ℕ) : ℕ := 12 * (j + 1)

def CA (j : ℕ) : ℕ := CK * CP (CL j)

lemma CD_mul_CG : CD * CG = Nat.fermatNumber 10 := by
  change CD * CG = 2 ^ 1024 + 1
  rw [show 1024 = 128 * 8 by norm_num, pow_mul]
  norm_num [CD, CG]

lemma CP_mul_CG {n : ℕ} (hn : 10 < n) :
    CP n * CG = 2 ^ (2 ^ n) - 1 := by
  have h10 : 10 ∈ Finset.range n := Finset.mem_range.mpr hn
  calc
    CP n * CG =
        (∏ i ∈ (Finset.range n).erase 10, Nat.fermatNumber i) * (CD * CG) := by
          simp [CP]
          ring
    _ = (∏ i ∈ (Finset.range n).erase 10, Nat.fermatNumber i) *
          Nat.fermatNumber 10 := by rw [CD_mul_CG]
    _ = ∏ i ∈ Finset.range n, Nat.fermatNumber i :=
      Finset.prod_erase_mul (Finset.range n) Nat.fermatNumber h10
    _ = Nat.fermatNumber n - 2 := Nat.prod_fermatNumber n
    _ = 2 ^ (2 ^ n) - 1 := by simp [Nat.fermatNumber]

lemma CP_pos (n : ℕ) : 0 < CP n := by
  apply Nat.mul_pos
  · norm_num [CD]
  · rw [CanonicallyOrderedAdd.prod_pos]
    intro i hi
    simp [Nat.fermatNumber]

lemma CL_gt_ten (j : ℕ) : 10 < CL j := by
  simp [CL]
  omega

lemma CP_mul_CG_add_one {n : ℕ} (hn : 10 < n) :
    CP n * CG + 1 = 2 ^ (2 ^ n) := by
  rw [CP_mul_CG hn]
  have hx : 0 < 2 ^ (2 ^ n) := by positivity
  omega

lemma CA_lt_power (j : ℕ) :
    CA j < 2 ^ (2 ^ CL j) := by
  have hp := CP_pos (CL j)
  have hkg : CK < CG := by norm_num [CK, CG]
  have hm := Nat.mul_lt_mul_of_pos_right hkg hp
  calc
    CA j = CK * CP (CL j) := rfl
    _ < CG * CP (CL j) := hm
    _ = CP (CL j) * CG := by ring
    _ = 2 ^ (2 ^ CL j) - 1 := CP_mul_CG (CL_gt_ten j)
    _ < 2 ^ (2 ^ CL j) := by
      have hx : 0 < 2 ^ (2 ^ CL j) := by positivity
      omega

lemma CA_ratio_lower (j : ℕ) :
    3 * (2 ^ (2 ^ CL j) - 1) < 4 * CA j := by
  have hp := CP_pos (CL j)
  have hratio : 3 * CG < 4 * CK := by norm_num [CK, CG]
  have hm := Nat.mul_lt_mul_of_pos_right hratio hp
  have hpg := CP_mul_CG (CL_gt_ten j)
  calc
    3 * (2 ^ (2 ^ CL j) - 1) = 3 * (CP (CL j) * CG) := by rw [hpg]
    _ = (3 * CG) * CP (CL j) := by ring
    _ < (4 * CK) * CP (CL j) := hm
    _ = 4 * CA j := by simp only [CA]; ring

lemma CL_ge_twelve (j : ℕ) : 12 ≤ CL j := by
  simp [CL]

lemma exponent_ge_forty_one (j : ℕ) : 41 ≤ 2 ^ CL j := by
  have h := Nat.pow_le_pow_right (by norm_num : 0 < 2) (CL_ge_twelve j)
  norm_num at h ⊢
  omega

lemma power_large (j : ℕ) :
    4 * CQ + 3 < 2 ^ (2 ^ CL j) := by
  have hbase : 4 * CQ + 3 < 2 ^ 41 := by norm_num [CQ]
  exact lt_of_lt_of_le hbase
    (Nat.pow_le_pow_right (by norm_num : 0 < 2) (exponent_ge_forty_one j))

lemma CA_ne_cover_prime (j a q : ℕ) (hqpos : 0 < q) (hqle : q ≤ CQ) :
    CA j ≠ q + 2 ^ a := by
  intro heq
  have htermA : 2 ^ a < CA j := by omega
  have htermX : 2 ^ a < 2 ^ (2 ^ CL j) :=
    lt_trans htermA (CA_lt_power j)
  have ha : a < 2 ^ CL j :=
    (Nat.pow_lt_pow_iff_right (by norm_num : 1 < 2)).mp htermX
  have hdouble : 2 * 2 ^ a ≤ 2 ^ (2 ^ CL j) := by
    calc
      2 * 2 ^ a = 2 ^ (a + 1) := by rw [pow_succ]; ring
      _ ≤ 2 ^ (2 ^ CL j) :=
        Nat.pow_le_pow_right (by norm_num : 0 < 2) (by omega)
  have hlow := CA_ratio_lower j
  have hlarge := power_large j
  rw [heq] at hlow
  omega

lemma outer_power_rewrite (j : ℕ) :
    2 ^ (2 ^ CL j) = (2 ^ 4096) ^ (4096 ^ j) := by
  calc
    2 ^ (2 ^ CL j) = 2 ^ ((2 ^ 12) ^ (j + 1)) := by
      rw [CL, pow_mul]
    _ = 2 ^ (4096 ^ (j + 1)) := by norm_num
    _ = 2 ^ (4096 * 4096 ^ j) := by
      congr 1
      rw [pow_succ]
      ring
    _ = (2 ^ 4096) ^ (4096 ^ j) := by rw [pow_mul]

lemma stable_iter {q u : ℕ} (h : u ^ 4096 ≡ u [MOD q]) :
    ∀ j : ℕ, u ^ (4096 ^ j) ≡ u [MOD q] := by
  intro j
  induction j with
  | zero => simpa using (Nat.ModEq.refl u : u ≡ u [MOD q])
  | succ j ih =>
      rw [pow_succ, pow_mul]
      exact (ih.pow 4096).trans h


lemma two_pow_mod_period {n m r q : ℕ}
    (hr : n % m = r) (hperiod : 2 ^ m ≡ 1 [MOD q]) :
    2 ^ n ≡ 2 ^ r [MOD q] := by
  have hdecomp : m * (n / m) + r = n := by
    rw [← hr]
    exact Nat.div_add_mod n m
  calc
    2 ^ n = 2 ^ (m * (n / m) + r) := by rw [hdecomp]
    _ = (2 ^ m) ^ (n / m) * 2 ^ r := by rw [pow_add, pow_mul]
    _ ≡ 1 ^ (n / m) * 2 ^ r [MOD q] :=
      (hperiod.pow (n / m)).mul (Nat.ModEq.refl (2 ^ r))
    _ = 2 ^ r := by simp

abbrev CoverCert (m r q u : ℕ) : Prop :=
  0 < q ∧ q ≤ CQ ∧ q ≠ 1 ∧ Nat.gcd q CG = 1 ∧ 1 ≤ u ∧
  2 ^ m ≡ 1 [MOD q] ∧
  2 ^ (4096 % m) ≡ u [MOD q] ∧
  (4096 * 4096) % m = 4096 % m ∧
  CK * (u - 1) ≡ CG * 2 ^ r [MOD q]

lemma one_power_case
    (j a p m r q u : ℕ)
    (ha : a % m = r)
    (hp : p.Prime)
    (heq : CA j = p + 2 ^ a)
    (hc : CoverCert m r q u) : False := by
  rcases hc with
    ⟨hqpos, hqle, hqone, hcop, huone, hperiod, husmall, hcycle, hbase⟩
  have hu : 2 ^ 4096 ≡ u [MOD q] :=
    (two_pow_mod_period (rfl : 4096 % m = 4096 % m) hperiod).trans husmall
  have hstable : u ^ 4096 ≡ u [MOD q] := by
    calc
      u ^ 4096 ≡ (2 ^ 4096) ^ 4096 [MOD q] := (hu.pow 4096).symm
      _ = 2 ^ (4096 * 4096) := by rw [pow_mul]
      _ ≡ 2 ^ (4096 % m) [MOD q] := two_pow_mod_period hcycle hperiod
      _ ≡ u [MOD q] := husmall
  have hXU : 2 ^ (2 ^ CL j) ≡ u [MOD q] := by
    rw [outer_power_rewrite]
    exact (hu.pow (4096 ^ j)).trans (stable_iter hstable j)
  have hXone : 1 ≤ 2 ^ (2 ^ CL j) := by
    have hx : 0 < 2 ^ (2 ^ CL j) := by positivity
    omega
  have hXm1 : 2 ^ (2 ^ CL j) - 1 ≡ u - 1 [MOD q] :=
    hXU.sub hXone huone (Nat.ModEq.refl 1)
  have hGA : CG * CA j ≡ CG * 2 ^ r [MOD q] := by
    calc
      CG * CA j = CK * (CP (CL j) * CG) := by
        simp only [CA]
        ring
      _ = CK * (2 ^ (2 ^ CL j) - 1) := by
        rw [CP_mul_CG (CL_gt_ten j)]
      _ ≡ CK * (u - 1) [MOD q] := hXm1.mul_left CK
      _ ≡ CG * 2 ^ r [MOD q] := hbase
  have hA : CA j ≡ 2 ^ r [MOD q] :=
    hGA.cancel_left_of_coprime hcop
  have hpow : 2 ^ a ≡ 2 ^ r [MOD q] :=
    two_pow_mod_period ha hperiod
  have hrepr : p + 2 ^ a ≡ 2 ^ r [MOD q] := by
    rw [← heq]
    exact hA
  have hpr : p + 2 ^ r ≡ 2 ^ r [MOD q] :=
    ((Nat.ModEq.refl p).add hpow).symm.trans hrepr
  have hpzero : p ≡ 0 [MOD q] := by
    apply Nat.ModEq.add_right_cancel' (2 ^ r)
    simpa using hpr
  have hdiv : q ∣ p := Nat.modEq_zero_iff_dvd.mp hpzero
  rcases (Nat.dvd_prime hp).mp hdiv with hq | hq
  · exact hqone hq
  · exact CA_ne_cover_prime j a q hqpos hqle (by simpa [hq] using heq)

lemma cover_cert_3_0_7 : CoverCert 3 0 7 2 := by
  norm_num [CoverCert, Nat.ModEq, CK, CG, CQ]



lemma cover_cert_5_0_31 :
    CoverCert 5 0 31 2 := by
  decide

lemma cover_cert_9_1_73 :
    CoverCert 9 1 73 2 := by
  decide

lemma cover_cert_10_1_11 :
    CoverCert 10 1 11 9 := by
  decide

lemma cover_cert_12_8_13 :
    CoverCert 12 8 13 3 := by
  decide

lemma cover_cert_15_8_151 :
    CoverCert 15 8 151 2 := by
  decide

lemma cover_cert_18_4_19 :
    CoverCert 18 4 19 17 := by
  decide

lemma cover_cert_20_7_41 :
    CoverCert 20 7 41 18 := by
  decide

lemma cover_cert_24_5_241 :
    CoverCert 24 5 241 225 := by
  decide

lemma cover_cert_30_29_331 :
    CoverCert 30 29 331 329 := by
  decide

lemma cover_cert_36_2_37 :
    CoverCert 36 2 37 12 := by
  decide

lemma cover_cert_36_14_109 :
    CoverCert 36 14 109 66 := by
  decide

lemma cover_cert_40_17_61681 :
    CoverCert 40 17 61681 3855 := by
  decide

lemma cover_cert_45_34_631 :
    CoverCert 45 34 631 2 := by
  decide

lemma cover_cert_45_43_23311 :
    CoverCert 45 43 23311 2 := by
  decide

lemma cover_cert_48_13_97 :
    CoverCert 48 13 97 61 := by
  decide

lemma cover_cert_48_37_673 :
    CoverCert 48 37 673 255 := by
  decide

lemma cover_cert_60_16_61 :
    CoverCert 60 16 61 22 := by
  decide

lemma cover_cert_60_19_1321 :
    CoverCert 60 19 1321 807 := by
  decide

lemma cover_cert_72_26_433 :
    CoverCert 72 26 433 296 := by
  decide

lemma cover_cert_72_62_38737 :
    CoverCert 72 62 38737 11954 := by
  decide

lemma cover_cert_90_52_18837001 :
    CoverCert 90 52 18837001 18836999 := by
  decide

lemma cover_cert_120_37_4562284561 :
    CoverCert 120 37 4562284561 65536 := by
  decide

lemma cover_cert_144_49_577 :
    CoverCert 144 49 577 435 := by
  decide

lemma cover_cert_144_121_487824887233 :
    CoverCert 144 121 487824887233 123861787774 := by
  decide

lemma cover_cert_180_103_181 :
    CoverCert 180 103 181 38 := by
  decide

lemma cover_cert_180_106_54001 :
    CoverCert 180 106 54001 17097 := by
  decide

lemma cover_cert_360_229_168692292721 :
    CoverCert 360 229 168692292721 140414064110 := by
  decide

abbrev Covered (x : ℕ) : Prop :=
    x % 3 = 0 ∨
    x % 5 = 0 ∨
    x % 9 = 1 ∨
    x % 10 = 1 ∨
    x % 12 = 8 ∨
    x % 15 = 8 ∨
    x % 18 = 4 ∨
    x % 20 = 7 ∨
    x % 24 = 5 ∨
    x % 30 = 29 ∨
    x % 36 = 2 ∨
    x % 36 = 14 ∨
    x % 40 = 17 ∨
    x % 45 = 34 ∨
    x % 45 = 43 ∨
    x % 48 = 13 ∨
    x % 48 = 37 ∨
    x % 60 = 16 ∨
    x % 60 = 19 ∨
    x % 72 = 26 ∨
    x % 72 = 62 ∨
    x % 90 = 52 ∨
    x % 120 = 37 ∨
    x % 144 = 49 ∨
    x % 144 = 121 ∨
    x % 180 = 103 ∨
    x % 180 = 106 ∨
    x % 360 = 229

lemma cover_grid :
    ∀ i : Fin 24, ∀ j : Fin 30, Covered (30 * i.val + j.val) := by
  decide

lemma cover_system (a : ℕ) : Covered a := by
  let x := a % 720
  have hi : x / 30 < 24 := by
    dsimp [x]
    omega
  have hj : x % 30 < 30 := Nat.mod_lt _ (by norm_num)
  have h := cover_grid ⟨x / 30, hi⟩ ⟨x % 30, hj⟩
  have heq : 30 * (x / 30) + x % 30 = x := Nat.div_add_mod x 30
  rw [heq] at h
  dsimp [Covered, x] at h ⊢
  norm_num [Nat.mod_mod_of_dvd] at h ⊢
  exact h

lemma CA_not_prime_plus_power (j a p : ℕ) (hp : p.Prime) :
    CA j ≠ p + 2 ^ a := by
  intro heq
  rcases cover_system a with h | h | h | h | h | h | h | h | h | h | h | h | h | h | h | h | h | h | h | h | h | h | h | h | h | h | h | h
  · exact one_power_case j a p 3 0 7 2 h hp heq cover_cert_3_0_7
  · exact one_power_case j a p 5 0 31 2 h hp heq cover_cert_5_0_31
  · exact one_power_case j a p 9 1 73 2 h hp heq cover_cert_9_1_73
  · exact one_power_case j a p 10 1 11 9 h hp heq cover_cert_10_1_11
  · exact one_power_case j a p 12 8 13 3 h hp heq cover_cert_12_8_13
  · exact one_power_case j a p 15 8 151 2 h hp heq cover_cert_15_8_151
  · exact one_power_case j a p 18 4 19 17 h hp heq cover_cert_18_4_19
  · exact one_power_case j a p 20 7 41 18 h hp heq cover_cert_20_7_41
  · exact one_power_case j a p 24 5 241 225 h hp heq cover_cert_24_5_241
  · exact one_power_case j a p 30 29 331 329 h hp heq cover_cert_30_29_331
  · exact one_power_case j a p 36 2 37 12 h hp heq cover_cert_36_2_37
  · exact one_power_case j a p 36 14 109 66 h hp heq cover_cert_36_14_109
  · exact one_power_case j a p 40 17 61681 3855 h hp heq cover_cert_40_17_61681
  · exact one_power_case j a p 45 34 631 2 h hp heq cover_cert_45_34_631
  · exact one_power_case j a p 45 43 23311 2 h hp heq cover_cert_45_43_23311
  · exact one_power_case j a p 48 13 97 61 h hp heq cover_cert_48_13_97
  · exact one_power_case j a p 48 37 673 255 h hp heq cover_cert_48_37_673
  · exact one_power_case j a p 60 16 61 22 h hp heq cover_cert_60_16_61
  · exact one_power_case j a p 60 19 1321 807 h hp heq cover_cert_60_19_1321
  · exact one_power_case j a p 72 26 433 296 h hp heq cover_cert_72_26_433
  · exact one_power_case j a p 72 62 38737 11954 h hp heq cover_cert_72_62_38737
  · exact one_power_case j a p 90 52 18837001 18836999 h hp heq cover_cert_90_52_18837001
  · exact one_power_case j a p 120 37 4562284561 65536 h hp heq cover_cert_120_37_4562284561
  · exact one_power_case j a p 144 49 577 435 h hp heq cover_cert_144_49_577
  · exact one_power_case j a p 144 121 487824887233 123861787774 h hp heq cover_cert_144_121_487824887233
  · exact one_power_case j a p 180 103 181 38 h hp heq cover_cert_180_103_181
  · exact one_power_case j a p 180 106 54001 17097 h hp heq cover_cert_180_106_54001
  · exact one_power_case j a p 360 229 168692292721 140414064110 h hp heq cover_cert_360_229_168692292721


lemma two_pow_mod_sixteen_zero {a : ℕ} (ha : 4 ≤ a) :
    2 ^ a % 16 = 0 := by
  have hsplit : a = 4 + (a - 4) := by omega
  rw [hsplit, pow_add]
  norm_num

lemma CA_mod_sixteen (j : ℕ) : CA j % 16 = 15 := by
  have hfour : 4 ≤ 2 ^ CL j := by
    exact le_trans (by norm_num) (exponent_ge_forty_one j)
  have hzero : 2 ^ (2 ^ CL j) ≡ 0 [MOD 16] := by
    exact two_pow_mod_sixteen_zero hfour
  have hsixteen : 2 ^ (2 ^ CL j) ≡ 16 [MOD 16] := by
    exact hzero.trans (by norm_num [Nat.ModEq])
  have hpos0 : 0 < 2 ^ (2 ^ CL j) := by positivity
  have hpos : 1 ≤ 2 ^ (2 ^ CL j) := by omega
  have hsub : 2 ^ (2 ^ CL j) - 1 ≡ 15 [MOD 16] := by
    simpa using hsixteen.sub hpos (by norm_num : 1 ≤ 16) (Nat.ModEq.refl 1)
  have hprod : CP (CL j) * CG ≡ 15 [MOD 16] := by
    rw [CP_mul_CG (CL_gt_ten j)]
    exact hsub
  have hG : CG ≡ 1 [MOD 16] := by
    norm_num [Nat.ModEq, CG]
  have hP : CP (CL j) ≡ 15 [MOD 16] := by
    calc
      CP (CL j) = CP (CL j) * 1 := by simp
      _ ≡ CP (CL j) * CG [MOD 16] :=
        ((Nat.ModEq.refl (CP (CL j))).mul hG).symm
      _ ≡ 15 [MOD 16] := hprod
  have hK : CK ≡ 1 [MOD 16] := by
    norm_num [Nat.ModEq, CK]
  have hA : CA j ≡ 15 [MOD 16] := by
    calc
      CA j = CK * CP (CL j) := rfl
      _ ≡ 1 * 15 [MOD 16] := hK.mul hP
      _ = 15 := by norm_num
  exact hA

lemma CP_one_lt (n : ℕ) : 1 < CP n := by
  have hprodpos : 0 < ∏ i ∈ (Finset.range n).erase 10, Nat.fermatNumber i := by
    rw [CanonicallyOrderedAdd.prod_pos]
    intro i hi
    simp [Nat.fermatNumber]
  have hprod : 1 ≤ ∏ i ∈ (Finset.range n).erase 10, Nat.fermatNumber i := by
    omega
  calc
    1 < CD := by norm_num [CD]
    _ = CD * 1 := by simp
    _ ≤ CD * ∏ i ∈ (Finset.range n).erase 10, Nat.fermatNumber i :=
      Nat.mul_le_mul_left CD hprod
    _ = CP n := rfl

lemma CA_gt_fifteen (j : ℕ) : 15 < CA j := by
  have hppos : 0 < CP (CL j) := CP_pos _
  have hp : 1 ≤ CP (CL j) := by omega
  calc
    15 < CK := by norm_num [CK]
    _ = CK * 1 := by simp
    _ ≤ CK * CP (CL j) := Nat.mul_le_mul_left CK hp
    _ = CA j := rfl

lemma CA_not_prime (j : ℕ) : ¬(CA j).Prime := by
  intro hp
  have hkdvd : CK ∣ CA j := by
    refine ⟨CP (CL j), ?_⟩
    rfl
  rcases (Nat.dvd_prime hp).mp hkdvd with hk | hk
  · norm_num [CK] at hk
  · have hplt : 1 < CP (CL j) := CP_one_lt _
    have hkpos : 0 < CK := by norm_num [CK]
    have hlt : CK < CA j := by
      calc
        CK = CK * 1 := by simp
        _ < CK * CP (CL j) := Nat.mul_lt_mul_of_pos_left hplt hkpos
        _ = CA j := rfl
    omega

def BF (r : ℕ) : ℕ := if r = 10 then CD else Nat.fermatNumber r

lemma fermatNumber_mod_sixteen {r : ℕ} (hr : 2 ≤ r) :
    Nat.fermatNumber r % 16 = 1 := by
  have hfour : 4 ≤ 2 ^ r := by
    have h := Nat.pow_le_pow_right (by norm_num : 0 < 2) hr
    norm_num at h ⊢
    omega
  have hz : 2 ^ (2 ^ r) ≡ 0 [MOD 16] :=
    two_pow_mod_sixteen_zero hfour
  have h : Nat.fermatNumber r ≡ 1 [MOD 16] := by
    calc
      Nat.fermatNumber r = 2 ^ (2 ^ r) + 1 := rfl
      _ ≡ 0 + 1 [MOD 16] := hz.add (Nat.ModEq.refl 1)
      _ = 1 := by norm_num
  exact h

lemma BF_one_lt (r : ℕ) : 1 < BF r := by
  unfold BF
  split_ifs with h
  · norm_num [CD]
  · have hF : 2 < Nat.fermatNumber r := Nat.two_lt_fermatNumber r
    omega

lemma BF_residue_class (r : ℕ) :
    BF r = 3 ∨ BF r = 5 ∨ BF r % 16 = 1 := by
  by_cases h0 : r = 0
  · subst r
    left
    norm_num [BF, Nat.fermatNumber]
  by_cases h1 : r = 1
  · subst r
    right; left
    norm_num [BF, Nat.fermatNumber]
  have hr : 2 ≤ r := by omega
  right; right
  by_cases h10 : r = 10
  · subst r
    norm_num [BF, CD]
  · simp only [BF, if_neg h10]
    exact fermatNumber_mod_sixteen hr

lemma two_power_residue_class
    {p a b : ℕ} (hb : 0 < b) (hba : b < a)
    (hpclass : p = 3 ∨ p = 5 ∨ p % 16 = 1)
    (hmod : (p + 2 ^ a + 2 ^ b) % 16 = 15) :
    (p = 3 ∧ a = 3 ∧ b = 2) ∨ (p = 5 ∧ a = 3 ∧ b = 1) := by
  rcases lt_or_ge a 4 with ha | ha
  · have hcases :
        (a = 2 ∧ b = 1) ∨ (a = 3 ∧ b = 1) ∨ (a = 3 ∧ b = 2) := by omega
    rcases hcases with h21 | h31 | h32
    · rcases h21 with ⟨rfl, rfl⟩
      rcases hpclass with rfl | rfl | hpmod
      · norm_num at hmod
      · norm_num at hmod
      · simp [Nat.add_mod, hpmod] at hmod
    · rcases h31 with ⟨rfl, rfl⟩
      rcases hpclass with rfl | rfl | hpmod
      · norm_num at hmod
      · exact Or.inr ⟨rfl, rfl, rfl⟩
      · simp [Nat.add_mod, hpmod] at hmod
    · rcases h32 with ⟨rfl, rfl⟩
      rcases hpclass with rfl | rfl | hpmod
      · exact Or.inl ⟨rfl, rfl, rfl⟩
      · norm_num at hmod
      · simp [Nat.add_mod, hpmod] at hmod
  · have hamod : 2 ^ a % 16 = 0 := two_pow_mod_sixteen_zero ha
    have hbclass :
        2 ^ b % 16 = 2 ∨ 2 ^ b % 16 = 4 ∨
        2 ^ b % 16 = 8 ∨ 2 ^ b % 16 = 0 := by
      rcases lt_or_ge b 4 with hb4 | hb4
      · have hbsmall : b = 1 ∨ b = 2 ∨ b = 3 := by omega
        rcases hbsmall with rfl | rfl | rfl
        · exact Or.inl (by norm_num)
        · exact Or.inr (Or.inl (by norm_num))
        · exact Or.inr (Or.inr (Or.inl (by norm_num)))
      · exact Or.inr (Or.inr (Or.inr (two_pow_mod_sixteen_zero hb4)))
    have hpmodclass : p % 16 = 3 ∨ p % 16 = 5 ∨ p % 16 = 1 := by
      rcases hpclass with rfl | rfl | hpmod
      · exact Or.inl (by norm_num)
      · exact Or.inr (Or.inl (by norm_num))
      · exact Or.inr (Or.inr hpmod)
    rcases hpmodclass with hpmod | hpmod | hpmod <;>
      rcases hbclass with hbmod | hbmod | hbmod | hbmod <;>
      simp [Nat.add_mod, hpmod, hamod, hbmod] at hmod


lemma BF_dvd_CP {r n : ℕ} (hr : r < n) : BF r ∣ CP n := by
  by_cases h10 : r = 10
  · subst r
    simp [BF, CP]
  · have hmem : r ∈ (Finset.range n).erase 10 := by
      simp [h10, hr]
    have hdiv :
        Nat.fermatNumber r ∣
          ∏ i ∈ (Finset.range n).erase 10, Nat.fermatNumber i :=
      Finset.dvd_prod_of_mem Nat.fermatNumber hmem
    rcases hdiv with ⟨c, hc⟩
    refine ⟨CD * c, ?_⟩
    simp only [BF, if_neg h10, CP]
    rw [hc]
    ring

lemma fermatNumber_dvd_pow_add_one {r u : ℕ} (hu : Odd u) :
    Nat.fermatNumber r ∣ 2 ^ (2 ^ r * u) + 1 := by
  have h := hu.nat_add_dvd_pow_add_pow (2 ^ (2 ^ r)) 1
  simpa [Nat.fermatNumber, pow_mul] using h

lemma BF_dvd_two_pow_sum
    {a b r u : ℕ} (hba : b ≤ a)
    (hdiff : a - b = 2 ^ r * u) (hu : Odd u) :
    BF r ∣ 2 ^ a + 2 ^ b := by
  have hF : Nat.fermatNumber r ∣ 2 ^ (a - b) + 1 := by
    rw [hdiff]
    exact fermatNumber_dvd_pow_add_one hu
  have hBF : BF r ∣ Nat.fermatNumber r := by
    by_cases h10 : r = 10
    · subst r
      simp only [BF]
      exact ⟨CG, CD_mul_CG.symm⟩
    · simp [BF, h10]
  rcases hBF.trans hF with ⟨c, hc⟩
  refine ⟨2 ^ b * c, ?_⟩
  have hab : a = (a - b) + b := by omega
  rw [hab, pow_add]
  calc
    2 ^ (a - b) * 2 ^ b + 2 ^ b =
        2 ^ b * (2 ^ (a - b) + 1) := by ring
    _ = 2 ^ b * (BF r * c) := by rw [hc]
    _ = BF r * (2 ^ b * c) := by ring


lemma CA_not_prime_plus_two_positive_powers_ordered
    (j a b p : ℕ) (hb : 0 < b) (hba : b ≤ a) (hp : p.Prime) :
    CA j ≠ p + 2 ^ a + 2 ^ b := by
  intro heq
  rcases eq_or_lt_of_le hba with hEq | hLt
  · subst b
    apply CA_not_prime_plus_power j (a + 1) p hp
    calc
      CA j = p + 2 ^ a + 2 ^ a := heq
      _ = p + 2 ^ (a + 1) := by rw [pow_succ]; ring
  · have hp_pos : 0 < p := hp.pos
    have hpb_pos : 0 < 2 ^ b := by positivity
    have hpowA : 2 ^ a < CA j := by omega
    have hpowX : 2 ^ a < 2 ^ (2 ^ CL j) :=
      lt_trans hpowA (CA_lt_power j)
    have haL : a < 2 ^ CL j :=
      (Nat.pow_lt_pow_iff_right (by norm_num : 1 < 2)).mp hpowX
    have hdiff_ne : a - b ≠ 0 := by omega
    obtain ⟨r, u, hu, hdiff⟩ := Nat.exists_eq_two_pow_mul_odd hdiff_ne
    have hupos : 0 < u := hu.pos
    have huone : 1 ≤ u := by omega
    have hpowr_le : 2 ^ r ≤ a - b := by
      calc
        2 ^ r = 2 ^ r * 1 := by simp
        _ ≤ 2 ^ r * u := Nat.mul_le_mul_left (2 ^ r) huone
        _ = a - b := hdiff.symm
    have hpowr_lt : 2 ^ r < 2 ^ CL j :=
      lt_of_le_of_lt (le_trans hpowr_le (Nat.sub_le a b)) haL
    have hrL : r < CL j :=
      (Nat.pow_lt_pow_iff_right (by norm_num : 1 < 2)).mp hpowr_lt
    have hBS : BF r ∣ 2 ^ a + 2 ^ b :=
      BF_dvd_two_pow_sum (Nat.le_of_lt hLt) hdiff hu
    have hBA : BF r ∣ CA j := by
      rcases BF_dvd_CP hrL with ⟨c, hc⟩
      refine ⟨CK * c, ?_⟩
      simp only [CA]
      rw [hc]
      ring
    have hA0 : CA j ≡ 0 [MOD BF r] :=
      Nat.modEq_zero_iff_dvd.mpr hBA
    have hS0 : 2 ^ a + 2 ^ b ≡ 0 [MOD BF r] :=
      Nat.modEq_zero_iff_dvd.mpr hBS
    have hrepr : p + (2 ^ a + 2 ^ b) ≡ 0 [MOD BF r] := by
      calc
        p + (2 ^ a + 2 ^ b) = p + 2 ^ a + 2 ^ b := by ring
        _ = CA j := heq.symm
        _ ≡ 0 [MOD BF r] := hA0
    have hpzero : p ≡ 0 [MOD BF r] := by
      apply Nat.ModEq.add_right_cancel' (2 ^ a + 2 ^ b)
      simpa using hrepr.trans hS0.symm
    have hdiv : BF r ∣ p := Nat.modEq_zero_iff_dvd.mp hpzero
    rcases (Nat.dvd_prime hp).mp hdiv with hbone | hbp
    · have hgt := BF_one_lt r
      omega
    · have hpclass : p = 3 ∨ p = 5 ∨ p % 16 = 1 := by
        simpa [hbp] using BF_residue_class r
      have hmod : (p + 2 ^ a + 2 ^ b) % 16 = 15 := by
        rw [← heq]
        exact CA_mod_sixteen j
      rcases two_power_residue_class hb hLt hpclass hmod with hcase | hcase
      · rcases hcase with ⟨rfl, rfl, rfl⟩
        have hgt := CA_gt_fifteen j
        norm_num at heq
        omega
      · rcases hcase with ⟨rfl, rfl, rfl⟩
        have hgt := CA_gt_fifteen j
        norm_num at heq
        omega

lemma CA_not_prime_plus_two_positive_powers
    (j a b p : ℕ) (ha : 0 < a) (hb : 0 < b) (hp : p.Prime) :
    CA j ≠ p + 2 ^ a + 2 ^ b := by
  intro heq
  rcases le_total b a with hba | hab
  · exact CA_not_prime_plus_two_positive_powers_ordered
      j a b p hb hba hp heq
  · apply CA_not_prime_plus_two_positive_powers_ordered
      j b a p ha hab hp
    calc
      CA j = p + 2 ^ a + 2 ^ b := heq
      _ = p + 2 ^ b + 2 ^ a := by ring


def CN (j : ℕ) : ℕ := CA j + 1

lemma CN_even (j : ℕ) : Even (CN j) := by
  have hmod := CA_mod_sixteen j
  have hdiv := Nat.div_add_mod (CA j) 16
  refine ⟨8 * (CA j / 16) + 8, ?_⟩
  simp only [CN]
  omega

lemma multiset_card_le_three_cases {α : Type*} (s : Multiset α)
    (hs : s.card ≤ 3) :
    s = 0 ∨
      (∃ a, s = {a}) ∨
      (∃ a b, s = {a, b}) ∨
      (∃ a b c, s = {a, b, c}) := by
  have hc : s.card = 0 ∨ s.card = 1 ∨ s.card = 2 ∨ s.card = 3 := by
    omega
  rcases hc with h0 | h1 | h2 | h3
  · exact Or.inl (Multiset.card_eq_zero.mp h0)
  · exact Or.inr (Or.inl (Multiset.card_eq_one.mp h1))
  · exact Or.inr (Or.inr (Or.inl (Multiset.card_eq_two.mp h2)))
  · exact Or.inr (Or.inr (Or.inr (Multiset.card_eq_three.mp h3)))

lemma pow_two_mod_sixteen_cases (a : ℕ) :
    (a = 0 ∧ 2 ^ a % 16 = 1) ∨
    (a = 1 ∧ 2 ^ a % 16 = 2) ∨
    (a = 2 ∧ 2 ^ a % 16 = 4) ∨
    (a = 3 ∧ 2 ^ a % 16 = 8) ∨
    (4 ≤ a ∧ 2 ^ a % 16 = 0) := by
  rcases lt_or_ge a 4 with ha | ha
  · have hsmall : a = 0 ∨ a = 1 ∨ a = 2 ∨ a = 3 := by omega
    rcases hsmall with rfl | rfl | rfl | rfl <;> norm_num
  · exact Or.inr (Or.inr (Or.inr (Or.inr
      ⟨ha, two_pow_mod_sixteen_zero ha⟩)))

lemma one_power_not_mod_sixteen_fourteen (a : ℕ) :
    2 ^ a % 16 ≠ 14 := by
  intro hmod
  rcases pow_two_mod_sixteen_cases a with
      ⟨rfl, ha⟩ | ⟨rfl, ha⟩ | ⟨rfl, ha⟩ | ⟨rfl, ha⟩ | ⟨ha_ge, ha⟩
  · norm_num at hmod
  · norm_num at hmod
  · norm_num at hmod
  · norm_num at hmod
  · omega

lemma two_powers_not_mod_sixteen_fourteen (a b : ℕ) :
    (2 ^ a + 2 ^ b) % 16 ≠ 14 := by
  intro hmod
  rcases pow_two_mod_sixteen_cases a with
      ⟨rfl, ha⟩ | ⟨rfl, ha⟩ | ⟨rfl, ha⟩ | ⟨rfl, ha⟩ | ⟨ha_ge, ha⟩ <;>
    rcases pow_two_mod_sixteen_cases b with
      ⟨rfl, hb⟩ | ⟨rfl, hb⟩ | ⟨rfl, hb⟩ | ⟨rfl, hb⟩ | ⟨hb_ge, hb⟩ <;>
    simp [Nat.add_mod, ha, hb] at hmod

lemma three_powers_mod_sixteen_fourteen
    {a b c : ℕ} (hmod : (2 ^ a + 2 ^ b + 2 ^ c) % 16 = 14) :
    2 ^ a + 2 ^ b + 2 ^ c = 14 := by
  rcases pow_two_mod_sixteen_cases a with
      ⟨rfl, ha⟩ | ⟨rfl, ha⟩ | ⟨rfl, ha⟩ | ⟨rfl, ha⟩ | ⟨ha_ge, ha⟩ <;>
    rcases pow_two_mod_sixteen_cases b with
      ⟨rfl, hb⟩ | ⟨rfl, hb⟩ | ⟨rfl, hb⟩ | ⟨rfl, hb⟩ | ⟨hb_ge, hb⟩ <;>
    rcases pow_two_mod_sixteen_cases c with
      ⟨rfl, hc⟩ | ⟨rfl, hc⟩ | ⟨rfl, hc⟩ | ⟨rfl, hc⟩ | ⟨hc_ge, hc⟩ <;>
    simp [Nat.add_mod, ha, hb, hc] at hmod ⊢


lemma pow_two_eq_two_mul_pre {a : ℕ} (ha : 0 < a) :
    2 ^ a = 2 * 2 ^ (a - 1) := by
  have hsplit : a = 1 + (a - 1) := by omega
  rw [hsplit, pow_add]
  norm_num

lemma mod_two_one_one_pow {c : ℕ} (hc : 0 < c) :
    (1 + 1 + 2 ^ c) % 2 = 0 := by
  rw [pow_two_eq_two_mul_pre hc]
  have h : 1 + 1 + 2 * 2 ^ (c - 1) =
      2 * (1 + 2 ^ (c - 1)) := by ring
  rw [h]
  simp

lemma mod_two_one_pow_one {b : ℕ} (hb : 0 < b) :
    (1 + 2 ^ b + 1) % 2 = 0 := by
  rw [pow_two_eq_two_mul_pre hb]
  have h : 1 + 2 * 2 ^ (b - 1) + 1 =
      2 * (2 ^ (b - 1) + 1) := by ring
  rw [h]
  simp

lemma mod_two_pow_one_one {a : ℕ} (ha : 0 < a) :
    (2 ^ a + 1 + 1) % 2 = 0 := by
  rw [pow_two_eq_two_mul_pre ha]
  have h : 2 * 2 ^ (a - 1) + 1 + 1 =
      2 * (2 ^ (a - 1) + 1) := by ring
  rw [h]
  simp

lemma mod_two_three_positive_pows {a b c : ℕ}
    (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
    (2 ^ a + 2 ^ b + 2 ^ c) % 2 = 0 := by
  rw [pow_two_eq_two_mul_pre ha, pow_two_eq_two_mul_pre hb,
    pow_two_eq_two_mul_pre hc]
  have h :
      2 * 2 ^ (a - 1) + 2 * 2 ^ (b - 1) + 2 * 2 ^ (c - 1) =
        2 * (2 ^ (a - 1) + 2 ^ (b - 1) + 2 ^ (c - 1)) := by ring
  rw [h]
  simp


lemma CN_mod_two (j : ℕ) : CN j % 2 = 0 := by
  rcases CN_even j with ⟨k, hk⟩
  rw [hk]
  omega

lemma CN_mod_sixteen (j : ℕ) : CN j % 16 = 0 := by
  simp [CN, Nat.add_mod, CA_mod_sixteen]

lemma two_pow_mod_two_zero {a : ℕ} (ha : 0 < a) :
    2 ^ a % 2 = 0 := by
  have hsplit : a = 1 + (a - 1) := by omega
  rw [hsplit, pow_add]
  norm_num

lemma prime_mod_two_one {p : ℕ} (hp : p.Prime) (hp2 : p ≠ 2) :
    p % 2 = 1 := by
  have hlt : p % 2 < 2 := Nat.mod_lt _ (by norm_num)
  by_contra hne
  have hz : p % 2 = 0 := by omega
  have hdvd : 2 ∣ p := Nat.dvd_iff_mod_eq_zero.mpr hz
  have heq : 2 = p :=
    (Nat.prime_dvd_prime_iff_eq (by norm_num) hp).mp hdvd
  exact hp2 heq.symm

lemma CN_odd_prime_even_sum_impossible
    (j p s : ℕ) (hpmod : p % 2 = 1) (hsmod : s % 2 = 0)
    (heq : CN j = p + s) : False := by
  have hmod : (p + s) % 2 = 0 := by
    rw [← heq]
    exact CN_mod_two j
  simp [Nat.add_mod, hpmod, hsmod] at hmod

lemma mapped_pow_sum_singleton (a : ℕ) :
    (({a} : Multiset ℕ).map (fun x => 2 ^ x)).sum = 2 ^ a := by
  simp

lemma mapped_pow_sum_pair (a b : ℕ) :
    (({a, b} : Multiset ℕ).map (fun x => 2 ^ x)).sum = 2 ^ a + 2 ^ b := by
  simp

lemma mapped_pow_sum_triple (a b c : ℕ) :
    (({a, b, c} : Multiset ℕ).map (fun x => 2 ^ x)).sum =
      2 ^ a + 2 ^ b + 2 ^ c := by
  simp
  ring

abbrev SumPrimeThreePows : Set ℕ :=
  Erdos10.sumPrimeAndTwoPows 3

lemma CN_not_sumPrimeThreePows (j : ℕ) :
    CN j ∉ SumPrimeThreePows := by
  intro hmem
  rcases hmem with ⟨p, pows, hp, hcard, heq⟩
  have heq' : CN j = p + (pows.map (2 ^ ·)).sum := heq.symm
  rcases multiset_card_le_three_cases pows hcard with
      hzero | ⟨a, hone⟩ | ⟨a, b, htwo⟩ | ⟨a, b, c, hthree⟩
  · subst pows
    simp only [Multiset.map_zero, Multiset.sum_zero, add_zero] at heq'
    by_cases hp2 : p = 2
    · rw [hp2] at heq'
      have hgt := CA_gt_fifteen j
      simp [CN] at heq'
      omega
    · exact CN_odd_prime_even_sum_impossible j p 0
        (prime_mod_two_one hp hp2) (by norm_num) (by simpa using heq')
  · subst pows
    rw [mapped_pow_sum_singleton] at heq'
    by_cases hp2 : p = 2
    · rw [hp2] at heq'
      have hreprmod : (2 + 2 ^ a) % 16 = 0 := by
        rw [← heq']
        exact CN_mod_sixteen j
      have hsumMod : 2 ^ a % 16 = 14 := by
        rw [Nat.add_mod] at hreprmod
        have hlt := Nat.mod_lt (2 ^ a) (by norm_num : 0 < 16)
        omega
      exact one_power_not_mod_sixteen_fourteen a hsumMod
    · have hpmod := prime_mod_two_one hp hp2
      by_cases ha0 : a = 0
      · subst a
        have hA : CA j = p := by
          simp [CN] at heq'
          omega
        have hpA : (CA j).Prime := by simpa [hA] using hp
        exact CA_not_prime j hpA
      · have ha : 0 < a := Nat.pos_of_ne_zero ha0
        exact CN_odd_prime_even_sum_impossible j p (2 ^ a)
          hpmod (two_pow_mod_two_zero ha) heq'
  · subst pows
    rw [mapped_pow_sum_pair] at heq'
    by_cases hp2 : p = 2
    · rw [hp2] at heq'
      have hform : CN j = 2 + 2 ^ a + 2 ^ b := by omega
      have hreprmod : (2 + (2 ^ a + 2 ^ b)) % 16 = 0 := by
        have hform' : CN j = 2 + (2 ^ a + 2 ^ b) := by omega
        exact (congrArg (fun n : ℕ => n % 16) hform'.symm).trans
          (CN_mod_sixteen j)
      have hsumMod : (2 ^ a + 2 ^ b) % 16 = 14 := by
        rw [Nat.add_mod] at hreprmod
        have hlt := Nat.mod_lt (2 ^ a + 2 ^ b) (by norm_num : 0 < 16)
        omega
      exact two_powers_not_mod_sixteen_fourteen a b hsumMod
    · have hpmod := prime_mod_two_one hp hp2
      by_cases ha0 : a = 0
      · subst a
        by_cases hb0 : b = 0
        · subst b
          have hform : CN j = p + 2 := by omega
          exact CN_odd_prime_even_sum_impossible j p 2 hpmod (by norm_num) hform
        · have hb : 0 < b := Nat.pos_of_ne_zero hb0
          have hA : CA j = p + 2 ^ b := by
            simp [CN] at heq'
            omega
          exact CA_not_prime_plus_power j b p hp hA
      · have ha : 0 < a := Nat.pos_of_ne_zero ha0
        by_cases hb0 : b = 0
        · subst b
          have hA : CA j = p + 2 ^ a := by
            simp [CN] at heq'
            omega
          exact CA_not_prime_plus_power j a p hp hA
        · have hb : 0 < b := Nat.pos_of_ne_zero hb0
          have hsmod : (2 ^ a + 2 ^ b) % 2 = 0 := by
            simp [Nat.add_mod, two_pow_mod_two_zero ha,
              two_pow_mod_two_zero hb]
          have hform : CN j = p + (2 ^ a + 2 ^ b) := by omega
          exact CN_odd_prime_even_sum_impossible j p (2 ^ a + 2 ^ b)
            hpmod hsmod hform
  · subst pows
    rw [mapped_pow_sum_triple] at heq'
    by_cases hp2 : p = 2
    · rw [hp2] at heq'
      have hform : CN j = 2 + (2 ^ a + 2 ^ b + 2 ^ c) := by omega
      have hreprmod : (2 + (2 ^ a + 2 ^ b + 2 ^ c)) % 16 = 0 :=
        (congrArg (fun n : ℕ => n % 16) hform.symm).trans
          (CN_mod_sixteen j)
      have hsumMod : (2 ^ a + 2 ^ b + 2 ^ c) % 16 = 14 := by
        rw [Nat.add_mod] at hreprmod
        have hlt := Nat.mod_lt (2 ^ a + 2 ^ b + 2 ^ c)
          (by norm_num : 0 < 16)
        omega
      have hsum := three_powers_mod_sixteen_fourteen hsumMod
      have hgt := CA_gt_fifteen j
      simp [CN] at heq'
      omega
    · have hpmod := prime_mod_two_one hp hp2
      by_cases ha0 : a = 0
      · subst a
        by_cases hb0 : b = 0
        · subst b
          by_cases hc0 : c = 0
          · subst c
            have hA : CA j = p + 2 ^ 1 := by
              simp [CN] at heq'
              omega
            exact CA_not_prime_plus_power j 1 p hp hA
          · have hc : 0 < c := Nat.pos_of_ne_zero hc0
            have hsmod : (1 + 1 + 2 ^ c) % 2 = 0 :=
              mod_two_one_one_pow hc
            have hform : CN j = p + (1 + 1 + 2 ^ c) := by omega
            exact CN_odd_prime_even_sum_impossible j p
              (1 + 1 + 2 ^ c) hpmod hsmod hform
        · have hb : 0 < b := Nat.pos_of_ne_zero hb0
          by_cases hc0 : c = 0
          · subst c
            have hsmod : (1 + 2 ^ b + 1) % 2 = 0 :=
              mod_two_one_pow_one hb
            have hform : CN j = p + (1 + 2 ^ b + 1) := by omega
            exact CN_odd_prime_even_sum_impossible j p
              (1 + 2 ^ b + 1) hpmod hsmod hform
          · have hc : 0 < c := Nat.pos_of_ne_zero hc0
            have hA : CA j = p + 2 ^ b + 2 ^ c := by
              simp [CN] at heq'
              omega
            exact CA_not_prime_plus_two_positive_powers j b c p hb hc hp hA
      · have ha : 0 < a := Nat.pos_of_ne_zero ha0
        by_cases hb0 : b = 0
        · subst b
          by_cases hc0 : c = 0
          · subst c
            have hsmod : (2 ^ a + 1 + 1) % 2 = 0 :=
              mod_two_pow_one_one ha
            have hform : CN j = p + (2 ^ a + 1 + 1) := by omega
            exact CN_odd_prime_even_sum_impossible j p
              (2 ^ a + 1 + 1) hpmod hsmod hform
          · have hc : 0 < c := Nat.pos_of_ne_zero hc0
            have hA : CA j = p + 2 ^ a + 2 ^ c := by
              simp [CN] at heq'
              omega
            exact CA_not_prime_plus_two_positive_powers j a c p ha hc hp hA
        · have hb : 0 < b := Nat.pos_of_ne_zero hb0
          by_cases hc0 : c = 0
          · subst c
            have hA : CA j = p + 2 ^ a + 2 ^ b := by
              simp [CN] at heq'
              omega
            exact CA_not_prime_plus_two_positive_powers j a b p ha hb hp hA
          · have hc : 0 < c := Nat.pos_of_ne_zero hc0
            have hsmod : (2 ^ a + 2 ^ b + 2 ^ c) % 2 = 0 :=
              mod_two_three_positive_pows ha hb hc
            have hform : CN j = p + (2 ^ a + 2 ^ b + 2 ^ c) := by omega
            exact CN_odd_prime_even_sum_impossible j p
              (2 ^ a + 2 ^ b + 2 ^ c) hpmod hsmod hform


lemma CL_strictMono : StrictMono CL := by
  intro a b hab
  simp only [CL]
  omega

lemma outer_power_strictMono :
    StrictMono (fun j : ℕ => 2 ^ (2 ^ CL j)) := by
  intro a b hab
  apply (Nat.pow_lt_pow_iff_right (by norm_num : 1 < 2)).mpr
  apply (Nat.pow_lt_pow_iff_right (by norm_num : 1 < 2)).mpr
  exact CL_strictMono hab

lemma CP_CL_strictMono : StrictMono (fun j : ℕ => CP (CL j)) := by
  intro a b hab
  have hX := outer_power_strictMono hab
  have ha := CP_mul_CG_add_one (CL_gt_ten a)
  have hb := CP_mul_CG_add_one (CL_gt_ten b)
  have hmulAdd : CP (CL a) * CG + 1 < CP (CL b) * CG + 1 := by
    calc
      CP (CL a) * CG + 1 = 2 ^ (2 ^ CL a) := ha
      _ < 2 ^ (2 ^ CL b) := hX
      _ = CP (CL b) * CG + 1 := hb.symm
  have hmul : CP (CL a) * CG < CP (CL b) * CG := by omega
  have hG : 0 < CG := by norm_num [CG]
  exact (Nat.mul_lt_mul_right hG).mp hmul

lemma CA_strictMono : StrictMono CA := by
  intro a b hab
  have hp := CP_CL_strictMono hab
  have hk : 0 < CK := by norm_num [CK]
  exact Nat.mul_lt_mul_of_pos_left hp hk

lemma CN_strictMono : StrictMono CN := by
  intro a b hab
  have hA := CA_strictMono hab
  simp only [CN]
  omega

lemma CN_range_subset :
    Set.range CN ⊆ {n : ℕ | Even n} \ SumPrimeThreePows := by
  rintro n ⟨j, rfl⟩
  exact ⟨CN_even j, CN_not_sumPrimeThreePows j⟩

lemma local_grechuk_target :
    Set.Infinite ({n : ℕ | Even n} \ SumPrimeThreePows) := by
  exact (Set.infinite_range_of_injective CN_strictMono.injective).mono
    CN_range_subset

theorem target :
    fcTypeOfName% "Erdos10.erdos_10.variants.grechuk" := by
  exact local_grechuk_target