cases l with
| nil => contradiction
| cons x l =>
  induction l generalizing a x with
  | nil =>
    intro n hn
    simp at *
    apply And.intro <;> linarith
  | cons y l h =>
    rw [List.chain_cons] at hl_mono
    rw [List.chain_cons] at hl_slow
    simp at hb
    specialize @h x y hl_mono.right hl_slow.right (List.cons_ne_nil y l) hb
    intro n hn
    specialize h n
    have : ∀ lᵢ, lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l := by simp
    simp_rw [this]
    simp only [or_and_right]
    rw [exists_or]
    cases le_or_lt x n with
    | inl hx =>
      apply Or.inr
      simp only [Set.mem_Ico] at *
      specialize h (And.intro hx hn.right)
      exact h
    | inr hx =>
      apply Or.inl
      simp at *
      apply And.intro <;> linarith
a b : ℕ
l : List ℕ
hl_mono : List.Chain (fun u v => u < v) a l
hl_slow : List.Chain (fun u v => v ≤ 2 * u) a l
hl_cons : l ≠ []
hb : b < List.getLast l hl_cons
⊢ ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ l ∧ lᵢ ∈ Set.Ioc n (2 * n)
no goals