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

State before:
α : Type u_1
x y : α
xs ys : List α
⊢ x :: xs = y :: ys ↔ x = y ∧ xs = ys
Tactic:
apply Iff.intro
State after:
case mp
α : Type u_1
x y : α
xs ys : List α
⊢ x :: xs = y :: ys → x = y ∧ xs = ys

case mpr
α : Type u_1
x y : α
xs ys : List α
⊢ x = y ∧ xs = ys → x :: xs = y :: ys

State before:
case mp
α : Type u_1
x y : α
xs ys : List α
⊢ x :: xs = y :: ys → x = y ∧ xs = ys
Tactic:
intro h
State after:
case mp
α : Type u_1
x y : α
xs ys : List α
h : x :: xs = y :: ys
⊢ x = y ∧ xs = ys

State before:
case mp
α : Type u_1
x y : α
xs ys : List α
h : x :: xs = y :: ys
⊢ x = y ∧ xs = ys
Tactic:
apply And.intro
State after:
case mp.left
α : Type u_1
x y : α
xs ys : List α
h : x :: xs = y :: ys
⊢ x = y

case mp.right
α : Type u_1
x y : α
xs ys : List α
h : x :: xs = y :: ys
⊢ xs = ys

State before:
case mp.left
α : Type u_1
x y : α
xs ys : List α
h : x :: xs = y :: ys
⊢ x = y
Tactic:
injections
State after:
no goals

State before:
case mp.right
α : Type u_1
x y : α
xs ys : List α
h : x :: xs = y :: ys
⊢ xs = ys
Tactic:
injections
State after:
no goals

State before:
case mpr
α : Type u_1
x y : α
xs ys : List α
⊢ x = y ∧ xs = ys → x :: xs = y :: ys
Tactic:
intro h
State after:
case mpr
α : Type u_1
x y : α
xs ys : List α
h : x = y ∧ xs = ys
⊢ x :: xs = y :: ys

State before:
case mpr
α : Type u_1
x y : α
xs ys : List α
h : x = y ∧ xs = ys
⊢ x :: xs = y :: ys
Tactic:
congr
State after:
case mpr.e_head
α : Type u_1
x y : α
xs ys : List α
h : x = y ∧ xs = ys
⊢ x = y

case mpr.e_tail
α : Type u_1
x y : α
xs ys : List α
h : x = y ∧ xs = ys
⊢ xs = ys

State before:
case mpr.e_head
α : Type u_1
x y : α
xs ys : List α
h : x = y ∧ xs = ys
⊢ x = y
Tactic:
exact h.left
State after:
no goals

State before:
case mpr.e_tail
α : Type u_1
x y : α
xs ys : List α
h : x = y ∧ xs = ys
⊢ xs = ys
Tactic:
exact h.right
State after:
no goals