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

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

State before:
α : Type u_1
x₁ x₂ : α
xs : List α
ih : length (split xs).fst ≤ length xs
⊢ length (split xs).fst + 1 ≤ length xs + 1 + 1
Tactic:
apply Nat.le.step
State after:
case a
α : Type u_1
x₁ x₂ : α
xs : List α
ih : length (split xs).fst ≤ length xs
⊢ Nat.le (length (split xs).fst + 1) (length xs + 1)

State before:
case a
α : Type u_1
x₁ x₂ : α
xs : List α
ih : length (split xs).fst ≤ length xs
⊢ Nat.le (length (split xs).fst + 1) (length xs + 1)
Tactic:
apply Nat.succ_le_succ
State after:
case a.a
α : Type u_1
x₁ x₂ : α
xs : List α
ih : length (split xs).fst ≤ length xs
⊢ length (split xs).fst ≤ length xs

State before:
case a.a
α : Type u_1
x₁ x₂ : α
xs : List α
ih : length (split xs).fst ≤ length xs
⊢ length (split xs).fst ≤ length xs
Tactic:
apply ih
State after:
no goals