induction lst with
| nil =>
  simp [splitList]
| cons x xs ih =>
  simp [splitList]
  cases ih
  constructor
  case left =>
    apply Nat.succ_le_succ
    assumption
  case right =>
    apply Nat.le_succ_of_le
    assumption
α : Type u_1
lst : List α
⊢ List.length (splitList lst).fst ≤ List.length lst ∧ List.length (splitList lst).snd ≤ List.length lst
no goals