simp at *
case cons.cons.inr.h
b y : ℕ
l : List ℕ
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 (y :: l) (_ : ¬y :: l = [])
n : ℕ
hn : n ∈ Set.Icc a b
h : n ∈ Set.Icc x b → ∃ lᵢ, lᵢ ∈ y :: l ∧ lᵢ ∈ Set.Ioc n (2 * n)
this : ∀ (lᵢ : ℕ), lᵢ ∈ x :: y :: l ↔ lᵢ = x ∨ lᵢ ∈ y :: l
hx : n < x
⊢ ∃ x_1, x_1 = x ∧ x_1 ∈ Set.Ioc n (2 * n)
case cons.cons.inr.h
b y : ℕ
l : List ℕ
a x : ℕ
hb : b < List.getLast (y :: l) (_ : ¬y :: l = [])
n : ℕ
hx : n < x
hl_mono : a < x ∧ x < y ∧ List.Chain (fun u v => u < v) y l
hl_slow : x ≤ 2 * a ∧ y ≤ 2 * x ∧ List.Chain (fun u v => v ≤ 2 * u) y l
hl_cons : True
hn : a ≤ n ∧ n ≤ b
h : x ≤ n → n ≤ b → n < y ∧ y ≤ 2 * n ∨ ∃ a, a ∈ l ∧ n < a ∧ a ≤ 2 * n
this : True
⊢ n < x ∧ x ≤ 2 * n