Theorem: list_length_split (Katydid/Std/Lists.lean)

State before:
α : Type u_1
xs ys : List α
⊢ length (xs ++ ys) = length xs + length ys
Tactic:
simp only [length_append]
State after:
no goals