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

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

State before:
α : Type u_1
x y : α
xs : List α
ih : length (split xs).fst + length (split xs).snd = length xs
⊢ length (split xs).fst + 1 + (length (split xs).snd + 1) = length xs + 1 + 1
Tactic:
rw [Nat.add_assoc (length xs),
    Nat.add_assoc (length (split xs).1),
    Nat.add_comm 1,
    Nat.add_assoc (length (split xs).2),
    ←Nat.add_assoc (length (split xs).1)]
State after:
α : Type u_1
x y : α
xs : List α
ih : length (split xs).fst + length (split xs).snd = length xs
⊢ length (split xs).fst + length (split xs).snd + (1 + 1) = length xs + (1 + 1)

State before:
α : Type u_1
x y : α
xs : List α
ih : length (split xs).fst + length (split xs).snd = length xs
⊢ length (split xs).fst + length (split xs).snd + (1 + 1) = length xs + (1 + 1)
Tactic:
apply congrArg (λ x => x + (1 + 1))
State after:
α : Type u_1
x y : α
xs : List α
ih : length (split xs).fst + length (split xs).snd = length xs
⊢ length (split xs).fst + length (split xs).snd = length xs

State before:
α : Type u_1
x y : α
xs : List α
ih : length (split xs).fst + length (split xs).snd = length xs
⊢ length (split xs).fst + length (split xs).snd = length xs
Tactic:
exact ih
State after:
no goals