RamareSaouter2003.has_prime_in_interval_2

@[blueprint  "thm:ramare_saouter2003-2"  (title := "Ramar\\'e-Saouter 2003 (2)")  (statement := /-- If $x > \exp(53)$, then there is a prime in the interval  \[ \left( x\left(1 - \frac{1}{204879661}\right), x \right]. \]  -/)  (latexEnv := "theorem")]theorem has_prime_in_interval_2 (x : ℝ) (hx : x > exp 53) :    HasPrimeInInterval (x*(1-1/204879661)) (x/204879661) := by  have hrow : (log (exp 53), (48:ℝ), (4.088e-9:ℝ), (18290358817:ℝ), (0.93:ℝ),      (0.4301:ℝ), (1524171138:ℝ)) ∈ KadiriLumley.Table_2 := by    rw [log_exp]; simp only [KadiriLumley.Table_2, List.mem_cons, Prod.mk.injEq,      List.mem_nil_iff, or_false]; norm_num  obtain ⟨p, hp, hlo, hhi⟩ := KadiriLumley.has_prime_in_interval (exp 53) x 48 4.088e-9    18290358817 0.93 0.4301 1524171138 hx.le hrow  refine ⟨p, hp, ?_, ?_⟩  · have hxpos : 0 < x := lt_trans (exp_pos _) hx    have : x * (1 - 1 / 204879661) ≤ x * (1 - 1 / 1524171138) := by      apply mul_le_mul_of_nonneg_left _ hxpos.le      apply sub_le_sub_left      exact one_div_le_one_div_of_le (by norm_num) (by norm_num : (204879661:ℝ) ≤ 1524171138)    exact lt_of_le_of_lt this hlo  · have heq : x * (1 - 1 / 204879661) + x / 204879661 = x := by ring    rw [heq]    exact le_of_lt hhi