rw [List.chain_cons] at hl_slow
case cons.cons
b y : ℕ
l : List ℕ
h :
  ∀ {a : ℕ} (x : ℕ),
    List.Chain (fun u v => u < v) a (x :: l) →
      List.Chain (fun u v => v ≤ 2 * u) a (x :: l) →
        ∀ (hl_cons : x :: l ≠ []),
          b < List.getLast (x :: l) hl_cons → ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : List.Chain (fun u v => v ≤ 2 * u) a (x :: y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (x :: y :: l) hl_cons
⊢ ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
case cons.cons
b y : ℕ
l : List ℕ
h :
  ∀ {a : ℕ} (x : ℕ),
    List.Chain (fun u v => u < v) a (x :: l) →
      List.Chain (fun u v => v ≤ 2 * u) a (x :: l) →
        ∀ (hl_cons : x :: l ≠ []),
          b < List.getLast (x :: l) hl_cons → ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
a x : ℕ
hl_mono : a < x ∧ List.Chain (fun u v => u < v) x (y :: l)
hl_slow : x ≤ 2 * a ∧ List.Chain (fun u v => v ≤ 2 * u) x (y :: l)
hl_cons : x :: y :: l ≠ []
hb : b < List.getLast (x :: y :: l) hl_cons
⊢ ∀ (n : ℕ), n ∈ Set.Icc a b → ∃ lᵢ, lᵢ ∈ x :: y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)