cases cmp x y with
| lt =>
  simp only
  have h₁ : length (x :: mergeWith cmp (y :: ys, xs)) =
            length (mergeWith cmp (y :: ys, xs)) + 1 := rfl
  have h₂ : length (x :: xs) = length xs + 1 := rfl
  rw [h₁, h₂, Nat.add_comm (length xs + 1), ←Nat.add_assoc]
  apply congrArg (λ x => x + 1)
  exact ih₁
| eq =>
  simp only
  have h₁ : length (x :: mergeWith cmp (y :: ys, xs)) =
            length (mergeWith cmp (y :: ys, xs)) + 1 := rfl
  have h₂ : length (x :: xs) = length xs + 1 := rfl
  rw [h₁, h₂, Nat.add_comm (length xs + 1), ←Nat.add_assoc]
  apply congrArg (λ x => x + 1)
  exact ih₁
| gt =>
  simp only [length]
  simp only [length] at ih₂
  rw [←Nat.add_assoc]
  apply congrArg (λ x => x + 1)
  rw [Nat.add_comm]
  exact ih₂
α : 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 cmp x y with
      | Ordering.gt => y :: mergeWith cmp (ys, x :: xs)
      | x_1 => x :: mergeWith cmp (y :: ys, xs)) =
    length (x :: xs) + length (y :: ys)
no goals