Goldbach.kadiri_lumley_odd_goldbach_finite

@[blueprint  "kl-odd-goldbach-finite"  (title := "Kadiri--Lumley's verification of odd Goldbach for small $n$")  (statement := /-- \cite[Corollary 1.2]{kadiri-lumley}  The odd Goldbach conjecture is verified up to $1966196911 \times 4 \times 10^{18}$. -/)  (proof := /-- Combine Proposition \ref{e-silva-herzog-piranian-even-goldbach-ext},  Proposition \ref{even-to-odd-goldbach-triv}, and Theorem \ref{thm:prime_gaps_KL} with  $x_0 = e^{60}$ and $\Delta = 1966090061$.  (Actually, if one is only allowed to use the  previous results listed here, one first needs to use the values $x_0 = e^{59}$ and  $\Delta = 1946282821$ to cover an intermediate range of values.)-/)  (latexEnv := "proposition")  (discussion := 970)]theorem kadiri_lumley_odd_goldbach_finite : odd_conjecture (1966196911 * 4 * 10 ^ 18) := by  have h1 (x) (hx : x ≥ Real.exp 59) : HasPrimeInInterval (x * (1 - 1 / 1946282821)) (x / 1946282821) := by    obtain ⟨p, hp, hlo, hhi⟩ := KadiriLumley.has_prime_in_interval (Real.exp 59) x      61 4.589e-9 20499925573 0.93 0.4522 1946282821 hx (by        simp only [KadiriLumley.Table_2, Real.log_exp, List.mem_cons, Prod.mk.injEq,          OfNat.ofNat_eq_ofNat, Nat.reduceEqDiff, and_false, and_self, Nat.succ_ne_self,          List.not_mem_nil, or_self, or_false, or_true])    refine ⟨p, hp, hlo, ?_⟩    have heq : x * (1 - 1 / 1946282821) + x / 1946282821 = x := by ring    rw [heq]; exact le_of_lt hhi  have h2 := even_to_odd_goldbach (⌈Real.exp 59⌉₊) (4 * 10 ^ 18 + 4) 1946282821    (fun x hx => h1 x (Nat.le_of_ceil_le hx)) e_silva_herzog_piranian_goldbach_ext  have h3 : ⌈Real.exp 59⌉₊ + 4 ≤ 11325 * 10 ^ 22 := by    have : Real.exp 59 + 4 + 1 ≤ 11325 * 10 ^ 22 := by interval_decide    grw [← Nat.cast_le (α := ℝ), Nat.cast_add, Nat.ceil_lt_add_one (Real.exp_nonneg _)]    grind  have h4 := h2 (odd_conjecture_mono _ (⌈Real.exp 59⌉₊ + 4) helfgott_odd_goldbach_finite h3)  have p1 (x) (hx : x ≥ Real.exp 60) : HasPrimeInInterval (x * (1 - 1 / 1966196911)) (x / 1966196911) := by    obtain ⟨p, hp, hlo, hhi⟩ := KadiriLumley.has_prime_in_interval (Real.exp 60) x      61 4.588e-9 20504393735 0.93 0.4527 1966196911 hx (by        simp only [KadiriLumley.Table_2, Real.log_exp, List.mem_cons, Prod.mk.injEq,          OfNat.ofNat_eq_ofNat, Nat.reduceEqDiff, and_false, and_self, Nat.succ_ne_self,          List.not_mem_nil, or_self, or_false, or_true])    refine ⟨p, hp, hlo, ?_⟩    have heq : x * (1 - 1 / 1966196911) + x / 1966196911 = x := by ring    rw [heq]; exact le_of_lt hhi  have p2 := even_to_odd_goldbach (⌈Real.exp 60⌉₊) (4 * 10 ^ 18 + 4) 1966196911    (fun x hx => p1 x (Nat.le_of_ceil_le hx)) e_silva_herzog_piranian_goldbach_ext  norm_num at *  have p3 : ⌈Real.exp 60⌉₊ + 4 ≤ 7785131284000000000000000004 := by    have : Real.exp 60 + 4 + 1 ≤ 7785131284000000000000000004 := by interval_decide    grw [← Nat.cast_le (α := ℝ), Nat.cast_add, Nat.ceil_lt_add_one (Real.exp_nonneg _)]    grind  exact odd_conjecture_mono _ _    (p2 (odd_conjecture_mono _ (⌈Real.exp 60⌉₊ + 4) h4 p3)) (by grind)