FKS2.Eπ_le_on_two_e

lemma Eπ_le_on_two_e {x : ℝ} (hx2 : 2 ≤ x) (hxe : x < Real.exp 1) : Eπ x ≤ 0.4298 := by  have hxpos : (0:ℝ) < x := by linarith  have hlogx : (0:ℝ) < Real.log x := Real.log_pos (by linarith)  have hpi  := pi_eq_one_lt_e hx2 hxe  have hLi0 := Li_nonneg_two hx2  have hLi2 := Li_le_two_lt_e hx2 hxe  have habs : |pi x - Li x| ≤ 1 := by rw [hpi, abs_le]; constructor <;> linarith  have hloge : Real.log x ≤ x / Real.exp 1 := by    have h := Real.log_le_sub_one_of_pos (show 0 < x / Real.exp 1 by positivity)    rwa [Real.log_div (ne_of_gt hxpos) (ne_of_gt (Real.exp_pos 1)),         Real.log_exp, sub_le_sub_iff_right] at h  have he9 : (2.7182818283:ℝ) < Real.exp 1 := Real.exp_one_gt_d9  have hxlogx : (2.7182818283:ℝ) ≤ x / Real.log x := by    rw [le_div_iff₀ hlogx]    have hcleared : Real.log x * Real.exp 1 ≤ x := by      rwa [le_div_iff₀ (Real.exp_pos 1)] at hloge    nlinarith [hcleared, he9, hlogx]  unfold Eπ  rw [div_le_iff₀ (by positivity)]  calc |pi x - Li x| ≤ 1 := habs    _ ≤ 0.4298 * (x / Real.log x) := by nlinarith [hxlogx]