rw [ih₁, ih₂]
α : Type u_1
cmp : α → α → Ordering
x y : α
xs : List α
term₁ : Nat.succ (length (split xs).fst) < Nat.succ (Nat.succ (length xs))
term₂ : Nat.succ (length (split xs).snd) < Nat.succ (Nat.succ (length xs))
ih₁ : length (mergeSortWith cmp (x :: (split xs).fst)) = length (x :: (split xs).fst)
ih₂ : length (mergeSortWith cmp (y :: (split xs).snd)) = length (y :: (split xs).snd)
⊢ length (mergeSortWith cmp (x :: (split xs).fst)) + length (mergeSortWith cmp (y :: (split xs).snd)) =
    length xs + 1 + 1
α : Type u_1
cmp : α → α → Ordering
x y : α
xs : List α
term₁ : Nat.succ (length (split xs).fst) < Nat.succ (Nat.succ (length xs))
term₂ : Nat.succ (length (split xs).snd) < Nat.succ (Nat.succ (length xs))
ih₁ : length (mergeSortWith cmp (x :: (split xs).fst)) = length (x :: (split xs).fst)
ih₂ : length (mergeSortWith cmp (y :: (split xs).snd)) = length (y :: (split xs).snd)
⊢ length (x :: (split xs).fst) + length (y :: (split xs).snd) = length xs + 1 + 1