obtain ⟨l₀', hl₀, hl'⟩ := hl
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
hl : l₀ <+~ l₂
h₀ : l₀.length ≤ n
h₂ : n ≤ l₂.length
⊢ ∃ l₁, l₀ <+~ l₁ ∧ l₁ <+~ l₂ ∧ l₁.length = n
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