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

State before:
α : Type u_1
a : α
xs ys : List α
⊢ [a] = xs ++ ys → xs = [] ∧ ys = [a] ∨ xs = [a] ∧ ys = []
Tactic:
intro H
State after:
α : Type u_1
a : α
xs ys : List α
H : [a] = xs ++ ys
⊢ xs = [] ∧ ys = [a] ∨ xs = [a] ∧ ys = []

State before:
α : Type u_1
a : α
xs ys : List α
H : [a] = xs ++ ys
⊢ xs = [] ∧ ys = [a] ∨ xs = [a] ∧ ys = []
Tactic:
apply list_app_eq_unit
State after:
case a
α : Type u_1
a : α
xs ys : List α
H : [a] = xs ++ ys
⊢ xs ++ ys = [a]

State before:
case a
α : Type u_1
a : α
xs ys : List α
H : [a] = xs ++ ys
⊢ xs ++ ys = [a]
Tactic:
apply Eq.symm
State after:
case a.h
α : Type u_1
a : α
xs ys : List α
H : [a] = xs ++ ys
⊢ [a] = xs ++ ys

State before:
case a.h
α : Type u_1
a : α
xs ys : List α
H : [a] = xs ++ ys
⊢ [a] = xs ++ ys
Tactic:
assumption
State after:
no goals