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

State before:
α : Type u_1
⊢ ∀ (xs ys zs : List α), xs ++ ys = zs → length xs ≤ length zs
Tactic:
intro xs ys zs xsyszs
State after:
α : Type u_1
xs ys zs : List α
xsyszs : xs ++ ys = zs
⊢ length xs ≤ length zs

State before:
α : Type u_1
xs ys zs : List α
xsyszs : xs ++ ys = zs
⊢ length xs ≤ length zs
Tactic:
apply (list_prefix_leq_length zs xs ys)
State after:
α : Type u_1
xs ys zs : List α
xsyszs : xs ++ ys = zs
⊢ zs = xs ++ ys

State before:
α : Type u_1
xs ys zs : List α
xsyszs : xs ++ ys = zs
⊢ zs = xs ++ ys
Tactic:
apply Eq.symm
State after:
case h
α : Type u_1
xs ys zs : List α
xsyszs : xs ++ ys = zs
⊢ xs ++ ys = zs

State before:
case h
α : Type u_1
xs ys zs : List α
xsyszs : xs ++ ys = zs
⊢ xs ++ ys = zs
Tactic:
exact xsyszs
State after:
no goals