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

State before:
α : Type u_1
⊢ ∀ {x : α} {xs ys zs : List α},
    ys ++ zs = x :: xs → ys = [] ∧ zs = x :: xs ∨ ∃ ys', ∃ (_ : ys = x :: ys'), ys' ++ zs = xs
Tactic:
intro x xs ys zs H
State after:
α : Type u_1
x : α
xs ys zs : List α
H : ys ++ zs = x :: xs
⊢ ys = [] ∧ zs = x :: xs ∨ ∃ ys', ∃ (_ : ys = x :: ys'), ys' ++ zs = xs

State before:
case nil
α : Type u_1
x : α
xs zs : List α
H : [] ++ zs = x :: xs
⊢ [] = [] ∧ zs = x :: xs ∨ ∃ ys', ∃ (_ : [] = x :: ys'), ys' ++ zs = xs
Tactic:
apply Or.inl
State after:
case nil.h
α : Type u_1
x : α
xs zs : List α
H : [] ++ zs = x :: xs
⊢ [] = [] ∧ zs = x :: xs

State before:
case nil.h
α : Type u_1
x : α
xs zs : List α
H : [] ++ zs = x :: xs
⊢ [] = [] ∧ zs = x :: xs
Tactic:
apply And.intro
State after:
case nil.h.left
α : Type u_1
x : α
xs zs : List α
H : [] ++ zs = x :: xs
⊢ [] = []

case nil.h.right
α : Type u_1
x : α
xs zs : List α
H : [] ++ zs = x :: xs
⊢ zs = x :: xs

State before:
case nil.h.left
α : Type u_1
x : α
xs zs : List α
H : [] ++ zs = x :: xs
⊢ [] = []
Tactic:
rfl
State after:
no goals

State before:
case nil.h.right
α : Type u_1
x : α
xs zs : List α
H : [] ++ zs = x :: xs
⊢ zs = x :: xs
Tactic:
simp only [nil_append] at H
State after:
case nil.h.right
α : Type u_1
x : α
xs zs : List α
H : zs = x :: xs
⊢ zs = x :: xs

State before:
case nil.h.right
α : Type u_1
x : α
xs zs : List α
H : zs = x :: xs
⊢ zs = x :: xs
Tactic:
assumption
State after:
no goals

State before:
case cons
α : Type u_1
x : α
xs zs : List α
y_ : α
ys_ : List α
H : y_ :: ys_ ++ zs = x :: xs
⊢ y_ :: ys_ = [] ∧ zs = x :: xs ∨ ∃ ys', ∃ (_ : y_ :: ys_ = x :: ys'), ys' ++ zs = xs
Tactic:
apply Or.inr
State after:
case cons.h
α : Type u_1
x : α
xs zs : List α
y_ : α
ys_ : List α
H : y_ :: ys_ ++ zs = x :: xs
⊢ ∃ ys', ∃ (_ : y_ :: ys_ = x :: ys'), ys' ++ zs = xs

State before:
case cons.h
α : Type u_1
x : α
xs zs : List α
y_ : α
ys_ : List α
H : y_ :: ys_ ++ zs = x :: xs
⊢ ∃ ys', ∃ (_ : y_ :: ys_ = x :: ys'), ys' ++ zs = xs
Tactic:
have H' := list_cons_eq.mp H
State after:
case cons.h
α : Type u_1
x : α
xs zs : List α
y_ : α
ys_ : List α
H : y_ :: ys_ ++ zs = x :: xs
H' : y_ = x ∧ List.append ys_ zs = xs
⊢ ∃ ys', ∃ (_ : y_ :: ys_ = x :: ys'), ys' ++ zs = xs

State before:
case cons.h
α : Type u_1
x : α
xs zs : List α
y_ : α
ys_ : List α
H : y_ :: ys_ ++ zs = x :: xs
H' : y_ = x ∧ List.append ys_ zs = xs
⊢ ∃ ys', ∃ (_ : y_ :: ys_ = x :: ys'), ys' ++ zs = xs
Tactic:
have HR := H'.right
State after:
case cons.h
α : Type u_1
x : α
xs zs : List α
y_ : α
ys_ : List α
H : y_ :: ys_ ++ zs = x :: xs
H' : y_ = x ∧ List.append ys_ zs = xs
HR : List.append ys_ zs = xs
⊢ ∃ ys', ∃ (_ : y_ :: ys_ = x :: ys'), ys' ++ zs = xs

State before:
case cons.h
α : Type u_1
x : α
xs zs : List α
y_ : α
ys_ : List α
H : y_ :: ys_ ++ zs = x :: xs
H' : y_ = x ∧ List.append ys_ zs = xs
HR : List.append ys_ zs = xs
⊢ ∃ ys', ∃ (_ : y_ :: ys_ = x :: ys'), ys' ++ zs = xs
Tactic:
have HL := H'.left
State after:
case cons.h
α : Type u_1
x : α
xs zs : List α
y_ : α
ys_ : List α
H : y_ :: ys_ ++ zs = x :: xs
H' : y_ = x ∧ List.append ys_ zs = xs
HR : List.append ys_ zs = xs
HL : y_ = x
⊢ ∃ ys', ∃ (_ : y_ :: ys_ = x :: ys'), ys' ++ zs = xs

State before:
case cons.h
α : Type u_1
x : α
xs zs : List α
y_ : α
ys_ : List α
H : y_ :: ys_ ++ zs = x :: xs
H' : y_ = x ∧ List.append ys_ zs = xs
HR : List.append ys_ zs = xs
HL : y_ = x
⊢ ∃ ys', ∃ (_ : y_ :: ys_ = x :: ys'), ys' ++ zs = xs
Tactic:
apply Exists.intro ys_
State after:
case cons.h
α : Type u_1
x : α
xs zs : List α
y_ : α
ys_ : List α
H : y_ :: ys_ ++ zs = x :: xs
H' : y_ = x ∧ List.append ys_ zs = xs
HR : List.append ys_ zs = xs
HL : y_ = x
⊢ ∃ (_ : y_ :: ys_ = x :: ys_), ys_ ++ zs = xs

State before:
case cons.h
α : Type u_1
x : α
xs zs : List α
y_ : α
ys_ : List α
H : y_ :: ys_ ++ zs = x :: xs
H' : y_ = x ∧ List.append ys_ zs = xs
HR : List.append ys_ zs = xs
HL : y_ = x
⊢ ∃ (_ : y_ :: ys_ = x :: ys_), ys_ ++ zs = xs
Tactic:
rw [HL]
State after:
case cons.h
α : Type u_1
x : α
xs zs : List α
y_ : α
ys_ : List α
H : y_ :: ys_ ++ zs = x :: xs
H' : y_ = x ∧ List.append ys_ zs = xs
HR : List.append ys_ zs = xs
HL : y_ = x
⊢ ∃ (_ : x :: ys_ = x :: ys_), ys_ ++ zs = xs

State before:
case cons.h
α : Type u_1
x : α
xs zs : List α
y_ : α
ys_ : List α
H : y_ :: ys_ ++ zs = x :: xs
H' : y_ = x ∧ List.append ys_ zs = xs
HR : List.append ys_ zs = xs
HL : y_ = x
⊢ ∃ (_ : x :: ys_ = x :: ys_), ys_ ++ zs = xs
Tactic:
apply Exists.intro rfl
State after:
case cons.h
α : Type u_1
x : α
xs zs : List α
y_ : α
ys_ : List α
H : y_ :: ys_ ++ zs = x :: xs
H' : y_ = x ∧ List.append ys_ zs = xs
HR : List.append ys_ zs = xs
HL : y_ = x
⊢ ys_ ++ zs = xs

State before:
case cons.h
α : Type u_1
x : α
xs zs : List α
y_ : α
ys_ : List α
H : y_ :: ys_ ++ zs = x :: xs
H' : y_ = x ∧ List.append ys_ zs = xs
HR : List.append ys_ zs = xs
HL : y_ = x
⊢ ys_ ++ zs = xs
Tactic:
exact HR
State after:
no goals