Theorem: splitList_shorter_le (Fpil/Chap10/Sec04.lean)

State before:
α : Type u_1
lst : List α
⊢ List.length (splitList lst).fst ≤ List.length lst ∧ List.length (splitList lst).snd ≤ List.length lst
Tactic:
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
State after:
no goals

State before:
case nil
α : Type u_1
⊢ List.length (splitList []).fst ≤ List.length [] ∧ List.length (splitList []).snd ≤ List.length []
Tactic:
simp [splitList]
State after:
no goals

State before:
case cons
α : Type u_1
x : α
xs : List α
ih : List.length (splitList xs).fst ≤ List.length xs ∧ List.length (splitList xs).snd ≤ List.length xs
⊢ List.length (splitList (x :: xs)).fst ≤ List.length (x :: xs) ∧
    List.length (splitList (x :: xs)).snd ≤ List.length (x :: xs)
Tactic:
simp [splitList]
State after:
case cons
α : Type u_1
x : α
xs : List α
ih : List.length (splitList xs).fst ≤ List.length xs ∧ List.length (splitList xs).snd ≤ List.length xs
⊢ Nat.succ (List.length (splitList xs).snd) ≤ Nat.succ (List.length xs) ∧
    List.length (splitList xs).fst ≤ Nat.succ (List.length xs)

State before:
case cons
α : Type u_1
x : α
xs : List α
ih : List.length (splitList xs).fst ≤ List.length xs ∧ List.length (splitList xs).snd ≤ List.length xs
⊢ Nat.succ (List.length (splitList xs).snd) ≤ Nat.succ (List.length xs) ∧
    List.length (splitList xs).fst ≤ Nat.succ (List.length xs)
Tactic:
cases ih
State after:
case cons.intro
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ Nat.succ (List.length (splitList xs).snd) ≤ Nat.succ (List.length xs) ∧
    List.length (splitList xs).fst ≤ Nat.succ (List.length xs)

State before:
case cons.intro
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ Nat.succ (List.length (splitList xs).snd) ≤ Nat.succ (List.length xs) ∧
    List.length (splitList xs).fst ≤ Nat.succ (List.length xs)
Tactic:
constructor
State after:
case cons.intro.left
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ Nat.succ (List.length (splitList xs).snd) ≤ Nat.succ (List.length xs)

case cons.intro.right
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ List.length (splitList xs).fst ≤ Nat.succ (List.length xs)

State before:
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ Nat.succ (List.length (splitList xs).snd) ≤ Nat.succ (List.length xs)
Tactic:
case left =>
  apply Nat.succ_le_succ
  assumption
State after:
no goals

State before:
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ List.length (splitList xs).fst ≤ Nat.succ (List.length xs)
Tactic:
case right =>
  apply Nat.le_succ_of_le
  assumption
State after:
no goals

State before:
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ Nat.succ (List.length (splitList xs).snd) ≤ Nat.succ (List.length xs)
Tactic:
apply Nat.succ_le_succ
State after:
case a
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ List.length (splitList xs).snd ≤ List.length xs

State before:
case a
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ List.length (splitList xs).snd ≤ List.length xs
Tactic:
assumption
State after:
no goals

State before:
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ List.length (splitList xs).fst ≤ Nat.succ (List.length xs)
Tactic:
apply Nat.le_succ_of_le
State after:
case h
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ List.length (splitList xs).fst ≤ List.length xs

State before:
case h
α : Type u_1
x : α
xs : List α
left✝ : List.length (splitList xs).fst ≤ List.length xs
right✝ : List.length (splitList xs).snd ≤ List.length xs
⊢ List.length (splitList xs).fst ≤ List.length xs
Tactic:
assumption
State after:
no goals