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

State before:
α : Type u_1
a : α
xs ys : List α
⊢ xs ++ ys = [a] → xs = [] ∧ ys = [a] ∨ xs = [a] ∧ ys = []
Tactic:
cases xs with
| nil =>
  intro hy
  simp only [nil_append] at hy
  apply Or.intro_left
  apply And.intro
  case left => rfl
  case right => assumption
| cons head tail =>
  intro hy
  simp only [cons_append, cons.injEq, append_eq_nil] at hy
  apply Or.intro_right
  cases hy with
  | intro h1 h2 =>
    rw [h1]
    cases h2 with
    | intro h4 h5 =>
      rw [h4, h5]
      apply And.intro <;> rfl
State after:
no goals

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

State before:
case nil
α : Type u_1
a : α
ys : List α
hy : [] ++ ys = [a]
⊢ [] = [] ∧ ys = [a] ∨ [] = [a] ∧ ys = []
Tactic:
simp only [nil_append] at hy
State after:
case nil
α : Type u_1
a : α
ys : List α
hy : ys = [a]
⊢ [] = [] ∧ ys = [a] ∨ [] = [a] ∧ ys = []

State before:
case nil
α : Type u_1
a : α
ys : List α
hy : ys = [a]
⊢ [] = [] ∧ ys = [a] ∨ [] = [a] ∧ ys = []
Tactic:
apply Or.intro_left
State after:
case nil.h
α : Type u_1
a : α
ys : List α
hy : ys = [a]
⊢ [] = [] ∧ ys = [a]

State before:
case nil.h
α : Type u_1
a : α
ys : List α
hy : ys = [a]
⊢ [] = [] ∧ ys = [a]
Tactic:
apply And.intro
State after:
case nil.h.left
α : Type u_1
a : α
ys : List α
hy : ys = [a]
⊢ [] = []

case nil.h.right
α : Type u_1
a : α
ys : List α
hy : ys = [a]
⊢ ys = [a]

State before:
α : Type u_1
a : α
ys : List α
hy : ys = [a]
⊢ [] = []
Tactic:
case left => rfl
State after:
no goals

State before:
α : Type u_1
a : α
ys : List α
hy : ys = [a]
⊢ ys = [a]
Tactic:
case right => assumption
State after:
no goals

State before:
α : Type u_1
a : α
ys : List α
hy : ys = [a]
⊢ [] = []
Tactic:
rfl
State after:
no goals

State before:
α : Type u_1
a : α
ys : List α
hy : ys = [a]
⊢ ys = [a]
Tactic:
assumption
State after:
no goals

State before:
case cons
α : Type u_1
a : α
ys : List α
head : α
tail : List α
⊢ head :: tail ++ ys = [a] → head :: tail = [] ∧ ys = [a] ∨ head :: tail = [a] ∧ ys = []
Tactic:
intro hy
State after:
case cons
α : Type u_1
a : α
ys : List α
head : α
tail : List α
hy : head :: tail ++ ys = [a]
⊢ head :: tail = [] ∧ ys = [a] ∨ head :: tail = [a] ∧ ys = []

State before:
case cons
α : Type u_1
a : α
ys : List α
head : α
tail : List α
hy : head :: tail ++ ys = [a]
⊢ head :: tail = [] ∧ ys = [a] ∨ head :: tail = [a] ∧ ys = []
Tactic:
simp only [cons_append, cons.injEq, append_eq_nil] at hy
State after:
case cons
α : Type u_1
a : α
ys : List α
head : α
tail : List α
hy : head = a ∧ tail = [] ∧ ys = []
⊢ head :: tail = [] ∧ ys = [a] ∨ head :: tail = [a] ∧ ys = []

State before:
case cons
α : Type u_1
a : α
ys : List α
head : α
tail : List α
hy : head = a ∧ tail = [] ∧ ys = []
⊢ head :: tail = [] ∧ ys = [a] ∨ head :: tail = [a] ∧ ys = []
Tactic:
apply Or.intro_right
State after:
case cons.h
α : Type u_1
a : α
ys : List α
head : α
tail : List α
hy : head = a ∧ tail = [] ∧ ys = []
⊢ head :: tail = [a] ∧ ys = []

State before:
case cons.h
α : Type u_1
a : α
ys : List α
head : α
tail : List α
hy : head = a ∧ tail = [] ∧ ys = []
⊢ head :: tail = [a] ∧ ys = []
Tactic:
cases hy with
| intro h1 h2 =>
  rw [h1]
  cases h2 with
  | intro h4 h5 =>
    rw [h4, h5]
    apply And.intro <;> rfl
State after:
no goals

State before:
case cons.h.intro
α : Type u_1
a : α
ys : List α
head : α
tail : List α
h1 : head = a
h2 : tail = [] ∧ ys = []
⊢ head :: tail = [a] ∧ ys = []
Tactic:
rw [h1]
State after:
case cons.h.intro
α : Type u_1
a : α
ys : List α
head : α
tail : List α
h1 : head = a
h2 : tail = [] ∧ ys = []
⊢ a :: tail = [a] ∧ ys = []

State before:
case cons.h.intro
α : Type u_1
a : α
ys : List α
head : α
tail : List α
h1 : head = a
h2 : tail = [] ∧ ys = []
⊢ a :: tail = [a] ∧ ys = []
Tactic:
cases h2 with
| intro h4 h5 =>
  rw [h4, h5]
  apply And.intro <;> rfl
State after:
no goals

State before:
case cons.h.intro.intro
α : Type u_1
a : α
ys : List α
head : α
tail : List α
h1 : head = a
h4 : tail = []
h5 : ys = []
⊢ a :: tail = [a] ∧ ys = []
Tactic:
rw [h4, h5]
State after:
case cons.h.intro.intro
α : Type u_1
a : α
ys : List α
head : α
tail : List α
h1 : head = a
h4 : tail = []
h5 : ys = []
⊢ [a] = [a] ∧ [] = []

State before:
case cons.h.intro.intro
α : Type u_1
a : α
ys : List α
head : α
tail : List α
h1 : head = a
h4 : tail = []
h5 : ys = []
⊢ [a] = [a] ∧ [] = []
Tactic:
apply And.intro <;> rfl
State after:
no goals