obtain ⟨l₁, h₀₁, h₁₂, hn⟩ := hl'.exists_intermediate (hl₀.length_eq.trans_le h₀) h₂
case intro.intro
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
h₀ : l₀.length ≤ n
h₂ : n ≤ l₂.length
l₀' : List α
hl₀ : l₀' ~ l₀
hl' : l₀' <+ l₂
⊢ ∃ l₁, l₀ <+~ l₁ ∧ l₁ <+~ l₂ ∧ l₁.length = n
case intro.intro.intro.intro.intro
α : Type u_1
l l' l₀ l₁✝ l₂ : List α
a b : α
m n : ℕ
h₀ : l₀.length ≤ n
h₂ : n ≤ l₂.length
l₀' : List α
hl₀ : l₀' ~ l₀
hl' : l₀' <+ l₂
l₁ : List α
h₀₁ : l₀' <+ l₁
h₁₂ : l₁ <+ l₂
hn : l₁.length = n
⊢ ∃ l₁, l₀ <+~ l₁ ∧ l₁ <+~ l₂ ∧ l₁.length = n