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
case cons
a b x : ℕ
l : List ℕ
hl_mono : List.Chain (fun u v => u < v) a (x :: l)
hl_slow : List.Chain (fun u v => v ≤ 2 * u) a (x :: l)
hl_cons : x :: l ≠ []
hb : b < List.getLast (x :: l) hl_cons
⊢ ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
no goals