-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem eq_append_cons_of_mem {a : α} {xs : List α} (h : a ∈ xs) :
    ∃ as bs, xs = as ++ a :: bs ∧ a ∉ as

Proof state:
case neg.intro.intro.intro
α : Type u_1
a x : α
h' : ¬a = x
as bs : List α
h✝ : ¬a ∈ as
ih : a ∈ as ++ a :: bs → ∃ as_1 bs_1, as ++ a :: bs = as_1 ++ a :: bs_1 ∧ ¬a ∈ as_1
h : a ∈ as ++ a :: bs
⊢ ∃ as_1 bs_1, x :: (as ++ a :: bs) = as_1 ++ a :: bs_1 ∧ ¬a ∈ as_1

Tactic:
exact ⟨x :: as, bs, rfl, by simp_all⟩

Result:
no goals

Proof state:
case cons.inr
α : Type u_1
a x : α
xs : List α
ih : a ∈ xs → ∃ as bs, xs = as ++ a :: bs ∧ ¬a ∈ as
h : a ∈ xs
⊢ ∃ as bs, x :: xs = as ++ a :: bs ∧ ¬a ∈ as

Tactic:
by_cases h' : a = x

Result:
case pos
α : Type u_1
a x : α
xs : List α
ih : a ∈ xs → ∃ as bs, xs = as ++ a :: bs ∧ ¬a ∈ as
h : a ∈ xs
h' : a = x
⊢ ∃ as bs, x :: xs = as ++ a :: bs ∧ ¬a ∈ as

case neg
α : Type u_1
a x : α
xs : List α
ih : a ∈ xs → ∃ as bs, xs = as ++ a :: bs ∧ ¬a ∈ as
h : a ∈ xs
h' : ¬a = x
⊢ ∃ as bs, x :: xs = as ++ a :: bs ∧ ¬a ∈ as

Proof state:
case neg
α : Type u_1
a x : α
xs : List α
ih : a ∈ xs → ∃ as bs, xs = as ++ a :: bs ∧ ¬a ∈ as
h : a ∈ xs
h' : ¬a = x
⊢ ∃ as bs, x :: xs = as ++ a :: bs ∧ ¬a ∈ as

Tactic:
obtain ⟨as, bs, rfl, h⟩ := ih h

Result:
case neg.intro.intro.intro
α : Type u_1
a x : α
h' : ¬a = x
as bs : List α
h✝ : ¬a ∈ as
ih : a ∈ as ++ a :: bs → ∃ as_1 bs_1, as ++ a :: bs = as_1 ++ a :: bs_1 ∧ ¬a ∈ as_1
h : a ∈ as ++ a :: bs
⊢ ∃ as_1 bs_1, x :: (as ++ a :: bs) = as_1 ++ a :: bs_1 ∧ ¬a ∈ as_1

Proof state:
case pos
α : Type u_1
a : α
xs : List α
ih : a ∈ xs → ∃ as bs, xs = as ++ a :: bs ∧ ¬a ∈ as
h : a ∈ xs
⊢ ∃ as bs, a :: xs = as ++ a :: bs ∧ ¬a ∈ as

Tactic:
exact ⟨[], xs, by simp⟩

Result:
no goals

Proof state:
case cons
α : Type u_1
a x : α
xs : List α
ih : a ∈ xs → ∃ as bs, xs = as ++ a :: bs ∧ ¬a ∈ as
h : a ∈ x :: xs
⊢ ∃ as bs, x :: xs = as ++ a :: bs ∧ ¬a ∈ as

Tactic:
simp at h

Result:
case cons
α : Type u_1
a x : α
xs : List α
ih : a ∈ xs → ∃ as bs, xs = as ++ a :: bs ∧ ¬a ∈ as
h : a = x ∨ a ∈ xs
⊢ ∃ as bs, x :: xs = as ++ a :: bs ∧ ¬a ∈ as

Proof state:
α : Type u_1
a x : α
xs : List α
ih : a ∈ xs → ∃ as bs, xs = as ++ a :: bs ∧ ¬a ∈ as
h : a = x
⊢ x :: xs = [] ++ a :: xs ∧ ¬a ∈ []

Tactic:
simp_all

Result:
no goals

Proof state:
case cons.inl
α : Type u_1
a x : α
xs : List α
ih : a ∈ xs → ∃ as bs, xs = as ++ a :: bs ∧ ¬a ∈ as
h : a = x
⊢ ∃ as bs, x :: xs = as ++ a :: bs ∧ ¬a ∈ as

Tactic:
exact ⟨[], xs, by simp_all⟩

Result:
no goals

Proof state:
α : Type u_1
a x : α
h' : ¬a = x
as bs : List α
h✝ : ¬a ∈ as
ih : a ∈ as ++ a :: bs → ∃ as_1 bs_1, as ++ a :: bs = as_1 ++ a :: bs_1 ∧ ¬a ∈ as_1
h : a ∈ as ++ a :: bs
⊢ ¬a ∈ x :: as

Tactic:
simp_all

Result:
no goals

Proof state:
case nil
α : Type u_1
a : α
h : a ∈ []
⊢ ∃ as bs, [] = as ++ a :: bs ∧ ¬a ∈ as

Tactic:
cases h

Result:
no goals

Proof state:
α : Type u_1
a : α
xs : List α
ih : a ∈ xs → ∃ as bs, xs = as ++ a :: bs ∧ ¬a ∈ as
h : a ∈ xs
⊢ a :: xs = [] ++ a :: xs ∧ ¬a ∈ []

Tactic:
simp

Result:
no goals

Proof state:
case pos
α : Type u_1
a x : α
xs : List α
ih : a ∈ xs → ∃ as bs, xs = as ++ a :: bs ∧ ¬a ∈ as
h : a ∈ xs
h' : a = x
⊢ ∃ as bs, x :: xs = as ++ a :: bs ∧ ¬a ∈ as

Tactic:
subst h'

Result:
case pos
α : Type u_1
a : α
xs : List α
ih : a ∈ xs → ∃ as bs, xs = as ++ a :: bs ∧ ¬a ∈ as
h : a ∈ xs
⊢ ∃ as bs, a :: xs = as ++ a :: bs ∧ ¬a ∈ as