simp only [length]
case gt
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + length (x :: xs)
⊢ length
      (match Ordering.gt with
      | Ordering.gt => y :: mergeWith cmp (ys, x :: xs)
      | x_1 => x :: mergeWith cmp (y :: ys, xs)) =
    length (x :: xs) + length (y :: ys)
case gt
α : Type u_1
cmp : α → α → Ordering
x : α
xs : List α
y : α
ys : List α
ih₁ : length (mergeWith cmp (y :: ys, xs)) = length (y :: ys) + length xs
ih₂ : length (mergeWith cmp (ys, x :: xs)) = length ys + length (x :: xs)
⊢ length (mergeWith cmp (ys, x :: xs)) + 1 = length xs + 1 + (length ys + 1)