BKLNW.table_10_coverage

lemma table_10_coverage (b₀ y : ℝ) (hb₀ : b₀ ∈ table_10_entries) (hy1 : b₀ ≤ y) (hy2 : y ≤ (K : ℝ)) :  ∃ b ∈ table_10_entries, b₀ ≤ b ∧ b ≤ y ∧ y ≤ table_10_next b := by  let S := table_10_entries.filter (fun b ↦ b₀ ≤ b ∧ b ≤ y)  have h1 : b₀ ∈ S := by    simp only [mem_filter, hb₀, le_refl, hy1, and_self, S]  let b := S.max' ⟨b₀, h1⟩  obtain ⟨h5, h6, h7⟩ : b ∈ table_10_entries ∧ b₀ ≤ b ∧ b ≤ y := by    simpa [S] using show b ∈ S from Finset.max'_mem S ⟨b₀, h1⟩  refine ⟨b, h5, h6, h7, ?_⟩  let S_finset := table_10_bs.filter (b < ·)  have h12 : (K : ℝ) ∈ S_finset := by    simpa [S_finset, table_10_bs] using table_10_entry_lt_K b h5  let m := S_finset.min' ⟨K, h12⟩  have h16 : m ∈ table_10_bs ∧ b < m := by    simpa [S_finset] using (show m ∈ S_finset from Finset.min'_mem S_finset ⟨K, h12⟩)  rw [show table_10_next b = m from table_10_next_eq_min' b ⟨K, h12⟩]  by_contra h19  obtain (h22 | h22) : m ∈ table_10_entries ∨ m = K :=    Or.comm.1 (by simpa [table_10_bs, table_10_entries, K] using h16.1)  · have h28 : m ∈ S := by      simp only [mem_filter, h22, le_trans h6 h16.2.le, (Std.not_le.mp h19).le, and_self, S]    linarith [Finset.le_max' S m h28, h16.2]  · linarith [hy2]