Chebyshev.E_nu_eq_one

@[blueprint  "cheby-E-1"  (title := "$E$ initially constant")  (statement := /-- One has $E(x)=1$ for $1 \leq x < 6$. -/)  (proof := /-- This follows from direct computation. -/)  (latexEnv := "lemma")  (discussion := 835)]theorem E_nu_eq_one (x : ℝ) (hx : x ∈ Set.Ico 1 6) : E ν x = 1 := by  obtain ⟨h1, h6⟩ := hx  have hx0 : (0 : ℝ) ≤ x := by linarith  simp only [E_nu_expand, Nat.floor_eq_zero.mpr (by linarith : x / 30 < 1)]  have hflb : 1 ≤ ⌊x⌋₊ := by rwa [Nat.one_le_floor_iff]  have hfub : ⌊x⌋₊ ≤ 5 := Nat.lt_succ_iff.mp (Nat.floor_lt' (by grind) |>.mpr h6)  have h2 := floor_div_bounds hx0 (k := 2) (by norm_num)  have h3 := floor_div_bounds hx0 (k := 3) (by norm_num)  have h5 := floor_div_bounds hx0 (k := 5) (by norm_num)  push_cast at h2 h3 h5  rw [show ⌊x⌋₊ = ⌊x / 2⌋₊ + ⌊x / 3⌋₊ + ⌊x / 5⌋₊ + 1 by omega]  grind