Theorem: List.split_length_fst (Table/BuiltinExtensions.lean)

State before:
α : Type u_1
x₁ x₂ x x' : α
xs : List α
ih : length (x :: x' :: xs) ≤ 1 ∨ length (split (x :: x' :: xs)).fst < length (x :: x' :: xs)
⊢ length (x₁ :: x₂ :: x :: x' :: xs) ≤ 1 ∨
    length (split (x₁ :: x₂ :: x :: x' :: xs)).fst < length (x₁ :: x₂ :: x :: x' :: xs)
Tactic:
simp only [split, length]
State after:
α : Type u_1
x₁ x₂ x x' : α
xs : List α
ih : length (x :: x' :: xs) ≤ 1 ∨ length (split (x :: x' :: xs)).fst < length (x :: x' :: xs)
⊢ length xs + 1 + 1 + 1 + 1 ≤ 1 ∨ length (split xs).fst + 1 + 1 < length xs + 1 + 1 + 1 + 1

State before:
α : Type u_1
x₁ x₂ x x' : α
xs : List α
ih : length (x :: x' :: xs) ≤ 1 ∨ length (split (x :: x' :: xs)).fst < length (x :: x' :: xs)
⊢ length xs + 1 + 1 + 1 + 1 ≤ 1 ∨ length (split xs).fst + 1 + 1 < length xs + 1 + 1 + 1 + 1
Tactic:
apply Or.intro_right
State after:
case h
α : Type u_1
x₁ x₂ x x' : α
xs : List α
ih : length (x :: x' :: xs) ≤ 1 ∨ length (split (x :: x' :: xs)).fst < length (x :: x' :: xs)
⊢ length (split xs).fst + 1 + 1 < length xs + 1 + 1 + 1 + 1

State before:
case h
α : Type u_1
x₁ x₂ x x' : α
xs : List α
ih : length (x :: x' :: xs) ≤ 1 ∨ length (split (x :: x' :: xs)).fst < length (x :: x' :: xs)
⊢ length (split xs).fst + 1 + 1 < length xs + 1 + 1 + 1 + 1
Tactic:
apply Nat.succ_lt_succ
State after:
case h.a
α : Type u_1
x₁ x₂ x x' : α
xs : List α
ih : length (x :: x' :: xs) ≤ 1 ∨ length (split (x :: x' :: xs)).fst < length (x :: x' :: xs)
⊢ length (split xs).fst + 1 < length xs + 3

State before:
case h.a
α : Type u_1
x₁ x₂ x x' : α
xs : List α
ih : length (x :: x' :: xs) ≤ 1 ∨ length (split (x :: x' :: xs)).fst < length (x :: x' :: xs)
⊢ length (split xs).fst + 1 < length xs + 3
Tactic:
simp [length, Nat.add] at ih
State after:
case h.a
α : Type u_1
x₁ x₂ x x' : α
xs : List α
ih : length xs + 1 + 1 ≤ 1 ∨ length (split xs).fst + 1 < length xs + 1 + 1
⊢ length (split xs).fst + 1 < length xs + 3

State before:
case h.a
α : Type u_1
x₁ x₂ x x' : α
xs : List α
ih : length xs + 1 + 1 ≤ 1 ∨ length (split xs).fst + 1 < length xs + 1 + 1
⊢ length (split xs).fst + 1 < length xs + 3
Tactic:
apply Nat.lt.step
State after:
case h.a.a
α : Type u_1
x₁ x₂ x x' : α
xs : List α
ih : length xs + 1 + 1 ≤ 1 ∨ length (split xs).fst + 1 < length xs + 1 + 1
⊢ length (split xs).fst + 1 < length xs + 2

State before:
case h.a.a
α : Type u_1
x₁ x₂ x x' : α
xs : List α
ih : length xs + 1 + 1 ≤ 1 ∨ length (split xs).fst + 1 < length xs + 1 + 1
⊢ length (split xs).fst + 1 < length xs + 2
Tactic:
cases ih with
| inl _ => contradiction
| inr h => apply h
State after:
no goals

State before:
case h.a.a.inl
α : Type u_1
x₁ x₂ x x' : α
xs : List α
h✝ : length xs + 1 + 1 ≤ 1
⊢ length (split xs).fst + 1 < length xs + 2
Tactic:
contradiction
State after:
no goals

State before:
case h.a.a.inr
α : Type u_1
x₁ x₂ x x' : α
xs : List α
h : length (split xs).fst + 1 < length xs + 1 + 1
⊢ length (split xs).fst + 1 < length xs + 2
Tactic:
apply h
State after:
no goals