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

State before:
α : Type u_1
xs ys : List α
x y : α
⊢ xs ++ [x] = ys ++ [y] → xs = ys ∧ x = y
Tactic:
revert ys
State after:
α : Type u_1
xs : List α
x y : α
⊢ ∀ {ys : List α}, xs ++ [x] = ys ++ [y] → xs = ys ∧ x = y

State before:
α : Type u_1
xs : List α
x y : α
⊢ ∀ {ys : List α}, xs ++ [x] = ys ++ [y] → xs = ys ∧ x = y
Tactic:
induction xs with
| nil =>
  intro ys h'
  simp only [nil_append] at h'
  have h3: (ys = [] /\ [y] = [x]) \/ (ys = [x] /\ [y] = []) := list_app_eq_unit (Eq.symm h')
  cases h3 with | inl left =>
    cases left with
    | intro empty xy =>
      simp only [cons.injEq, and_true] at xy
      rw [empty, xy]
      apply And.intro <;> rfl
  | inr right =>
    cases right with
    | intro empty ysx =>
      contradiction
| cons headx tailx ihx =>
  intro ys
  cases ys with
  | nil =>
    intro h'
    simp only [cons_append, nil_append, cons.injEq, append_eq_nil, and_false] at h'
  | cons heady taily =>
    intro h'
    simp only [cons_append, cons.injEq] at h'
    cases h' with
    | intro heads tails =>
      rw [heads]
      have h: tailx = taily ∧ x = y := (ihx tails)
      cases h with
      | intro tailxy xy =>
        rw [tailxy]
        rw [xy]
        apply And.intro <;> rfl
State after:
no goals

State before:
case nil
α : Type u_1
x y : α
⊢ ∀ {ys : List α}, [] ++ [x] = ys ++ [y] → [] = ys ∧ x = y
Tactic:
intro ys h'
State after:
case nil
α : Type u_1
x y : α
ys : List α
h' : [] ++ [x] = ys ++ [y]
⊢ [] = ys ∧ x = y

State before:
case nil
α : Type u_1
x y : α
ys : List α
h' : [] ++ [x] = ys ++ [y]
⊢ [] = ys ∧ x = y
Tactic:
simp only [nil_append] at h'
State after:
case nil
α : Type u_1
x y : α
ys : List α
h' : [x] = ys ++ [y]
⊢ [] = ys ∧ x = y

State before:
case nil
α : Type u_1
x y : α
ys : List α
h' : [x] = ys ++ [y]
⊢ [] = ys ∧ x = y
Tactic:
have h3: (ys = [] /\ [y] = [x]) \/ (ys = [x] /\ [y] = []) := list_app_eq_unit (Eq.symm h')
State after:
case nil
α : Type u_1
x y : α
ys : List α
h' : [x] = ys ++ [y]
h3 : ys = [] ∧ [y] = [x] ∨ ys = [x] ∧ [y] = []
⊢ [] = ys ∧ x = y

State before:
case nil
α : Type u_1
x y : α
ys : List α
h' : [x] = ys ++ [y]
h3 : ys = [] ∧ [y] = [x] ∨ ys = [x] ∧ [y] = []
⊢ [] = ys ∧ x = y
Tactic:
cases h3 with | inl left =>
  cases left with
  | intro empty xy =>
    simp only [cons.injEq, and_true] at xy
    rw [empty, xy]
    apply And.intro <;> rfl
| inr right =>
  cases right with
  | intro empty ysx =>
    contradiction
State after:
no goals

State before:
case nil.inl
α : Type u_1
x y : α
ys : List α
h' : [x] = ys ++ [y]
left : ys = [] ∧ [y] = [x]
⊢ [] = ys ∧ x = y
Tactic:
cases left with
| intro empty xy =>
  simp only [cons.injEq, and_true] at xy
  rw [empty, xy]
  apply And.intro <;> rfl
State after:
no goals

State before:
case nil.inl.intro
α : Type u_1
x y : α
ys : List α
h' : [x] = ys ++ [y]
empty : ys = []
xy : [y] = [x]
⊢ [] = ys ∧ x = y
Tactic:
simp only [cons.injEq, and_true] at xy
State after:
case nil.inl.intro
α : Type u_1
x y : α
ys : List α
h' : [x] = ys ++ [y]
empty : ys = []
xy : y = x
⊢ [] = ys ∧ x = y

State before:
case nil.inl.intro
α : Type u_1
x y : α
ys : List α
h' : [x] = ys ++ [y]
empty : ys = []
xy : y = x
⊢ [] = ys ∧ x = y
Tactic:
rw [empty, xy]
State after:
case nil.inl.intro
α : Type u_1
x y : α
ys : List α
h' : [x] = ys ++ [y]
empty : ys = []
xy : y = x
⊢ [] = [] ∧ x = x

State before:
case nil.inl.intro
α : Type u_1
x y : α
ys : List α
h' : [x] = ys ++ [y]
empty : ys = []
xy : y = x
⊢ [] = [] ∧ x = x
Tactic:
apply And.intro <;> rfl
State after:
no goals

State before:
case nil.inr
α : Type u_1
x y : α
ys : List α
h' : [x] = ys ++ [y]
right : ys = [x] ∧ [y] = []
⊢ [] = ys ∧ x = y
Tactic:
cases right with
| intro empty ysx =>
  contradiction
State after:
no goals

State before:
case nil.inr.intro
α : Type u_1
x y : α
ys : List α
h' : [x] = ys ++ [y]
empty : ys = [x]
ysx : [y] = []
⊢ [] = ys ∧ x = y
Tactic:
contradiction
State after:
no goals

State before:
case cons
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
⊢ ∀ {ys : List α}, headx :: tailx ++ [x] = ys ++ [y] → headx :: tailx = ys ∧ x = y
Tactic:
intro ys
State after:
case cons
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
ys : List α
⊢ headx :: tailx ++ [x] = ys ++ [y] → headx :: tailx = ys ∧ x = y

State before:
case cons
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
ys : List α
⊢ headx :: tailx ++ [x] = ys ++ [y] → headx :: tailx = ys ∧ x = y
Tactic:
cases ys with
| nil =>
  intro h'
  simp only [cons_append, nil_append, cons.injEq, append_eq_nil, and_false] at h'
| cons heady taily =>
  intro h'
  simp only [cons_append, cons.injEq] at h'
  cases h' with
  | intro heads tails =>
    rw [heads]
    have h: tailx = taily ∧ x = y := (ihx tails)
    cases h with
    | intro tailxy xy =>
      rw [tailxy]
      rw [xy]
      apply And.intro <;> rfl
State after:
no goals

State before:
case cons.nil
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
⊢ headx :: tailx ++ [x] = [] ++ [y] → headx :: tailx = [] ∧ x = y
Tactic:
intro h'
State after:
case cons.nil
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
h' : headx :: tailx ++ [x] = [] ++ [y]
⊢ headx :: tailx = [] ∧ x = y

State before:
case cons.nil
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
h' : headx :: tailx ++ [x] = [] ++ [y]
⊢ headx :: tailx = [] ∧ x = y
Tactic:
simp only [cons_append, nil_append, cons.injEq, append_eq_nil, and_false] at h'
State after:
no goals

State before:
case cons.cons
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
heady : α
taily : List α
⊢ headx :: tailx ++ [x] = heady :: taily ++ [y] → headx :: tailx = heady :: taily ∧ x = y
Tactic:
intro h'
State after:
case cons.cons
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
heady : α
taily : List α
h' : headx :: tailx ++ [x] = heady :: taily ++ [y]
⊢ headx :: tailx = heady :: taily ∧ x = y

State before:
case cons.cons
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
heady : α
taily : List α
h' : headx :: tailx ++ [x] = heady :: taily ++ [y]
⊢ headx :: tailx = heady :: taily ∧ x = y
Tactic:
simp only [cons_append, cons.injEq] at h'
State after:
case cons.cons
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
heady : α
taily : List α
h' : headx = heady ∧ tailx ++ [x] = taily ++ [y]
⊢ headx :: tailx = heady :: taily ∧ x = y

State before:
case cons.cons
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
heady : α
taily : List α
h' : headx = heady ∧ tailx ++ [x] = taily ++ [y]
⊢ headx :: tailx = heady :: taily ∧ x = y
Tactic:
cases h' with
| intro heads tails =>
  rw [heads]
  have h: tailx = taily ∧ x = y := (ihx tails)
  cases h with
  | intro tailxy xy =>
    rw [tailxy]
    rw [xy]
    apply And.intro <;> rfl
State after:
no goals

State before:
case cons.cons.intro
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
heady : α
taily : List α
heads : headx = heady
tails : tailx ++ [x] = taily ++ [y]
⊢ headx :: tailx = heady :: taily ∧ x = y
Tactic:
rw [heads]
State after:
case cons.cons.intro
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
heady : α
taily : List α
heads : headx = heady
tails : tailx ++ [x] = taily ++ [y]
⊢ heady :: tailx = heady :: taily ∧ x = y

State before:
case cons.cons.intro
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
heady : α
taily : List α
heads : headx = heady
tails : tailx ++ [x] = taily ++ [y]
⊢ heady :: tailx = heady :: taily ∧ x = y
Tactic:
have h: tailx = taily ∧ x = y := (ihx tails)
State after:
case cons.cons.intro
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
heady : α
taily : List α
heads : headx = heady
tails : tailx ++ [x] = taily ++ [y]
h : tailx = taily ∧ x = y
⊢ heady :: tailx = heady :: taily ∧ x = y

State before:
case cons.cons.intro
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
heady : α
taily : List α
heads : headx = heady
tails : tailx ++ [x] = taily ++ [y]
h : tailx = taily ∧ x = y
⊢ heady :: tailx = heady :: taily ∧ x = y
Tactic:
cases h with
| intro tailxy xy =>
  rw [tailxy]
  rw [xy]
  apply And.intro <;> rfl
State after:
no goals

State before:
case cons.cons.intro.intro
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
heady : α
taily : List α
heads : headx = heady
tails : tailx ++ [x] = taily ++ [y]
tailxy : tailx = taily
xy : x = y
⊢ heady :: tailx = heady :: taily ∧ x = y
Tactic:
rw [tailxy]
State after:
case cons.cons.intro.intro
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
heady : α
taily : List α
heads : headx = heady
tails : tailx ++ [x] = taily ++ [y]
tailxy : tailx = taily
xy : x = y
⊢ heady :: taily = heady :: taily ∧ x = y

State before:
case cons.cons.intro.intro
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
heady : α
taily : List α
heads : headx = heady
tails : tailx ++ [x] = taily ++ [y]
tailxy : tailx = taily
xy : x = y
⊢ heady :: taily = heady :: taily ∧ x = y
Tactic:
rw [xy]
State after:
case cons.cons.intro.intro
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
heady : α
taily : List α
heads : headx = heady
tails : tailx ++ [x] = taily ++ [y]
tailxy : tailx = taily
xy : x = y
⊢ heady :: taily = heady :: taily ∧ y = y

State before:
case cons.cons.intro.intro
α : Type u_1
x y headx : α
tailx : List α
ihx : ∀ {ys : List α}, tailx ++ [x] = ys ++ [y] → tailx = ys ∧ x = y
heady : α
taily : List α
heads : headx = heady
tails : tailx ++ [x] = taily ++ [y]
tailxy : tailx = taily
xy : x = y
⊢ heady :: taily = heady :: taily ∧ y = y
Tactic:
apply And.intro <;> rfl
State after:
no goals