obtain ⟨l₁, h₀₁, h₁₂, rfl⟩ := ih sorry (Nat.succ_le_succ_iff.1 h₀) (Nat.le_of_succ_le h₂)
case cons.succ.cons
α : Type u_1
l l' l₁ : List α
a✝ b✝ : α
m : ℕ
a : α
l₀ : List α
ih : ∀ {l₂ : List α} {n : ℕ}, l₀ <+ l₂ → l₀.length ≤ n → n ≤ l₂.length → ∃ l₁, l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
n✝ : ℕ
h₀ : (a :: l₀).length ≤ n✝ + 1
b : α
l₂ : List α
hl : a :: l₀ <+ b :: l₂
h₂ : n✝ + 1 ≤ (b :: l₂).length
⊢ ∃ l₁, a :: l₀ <+ l₁ ∧ l₁ <+ b :: l₂ ∧ l₁.length = n✝ + 1
case cons.succ.cons.intro.intro.intro
α : Type u_1
l l' l₁✝ : List α
a✝ b✝ : α
m : ℕ
a : α
l₀ : List α
ih : ∀ {l₂ : List α} {n : ℕ}, l₀ <+ l₂ → l₀.length ≤ n → n ≤ l₂.length → ∃ l₁, l₀ <+ l₁ ∧ l₁ <+ l₂ ∧ l₁.length = n
b : α
l₂ : List α
hl : a :: l₀ <+ b :: l₂
l₁ : List α
h₀₁ : l₀ <+ l₁
h₁₂ : l₁ <+ b :: l₂
h₀ : (a :: l₀).length ≤ l₁.length + 1
h₂ : l₁.length + 1 ≤ (b :: l₂).length
⊢ ∃ l₁_1, a :: l₀ <+ l₁_1 ∧ l₁_1 <+ b :: l₂ ∧ l₁_1.length = l₁.length + 1