Theorem: split_drop (GroupComp/WordProblem/FreeGroup.lean)

State before:
α : Type
inst✝ : DecidableEq α
β : Type u_1
l : List β
p : l ≠ []
⊢ List.dropLast l ++ [List.getLast l p] = l
Tactic:
match l with
| cancP :: t =>
match t with 
| [] =>  simp [p] at *
| h' :: t' =>
  simp [List.dropLast, List.getLast, split_drop]
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
β : Type u_1
l : List β
cancP : β
t : List β
p : cancP :: t ≠ []
⊢ List.dropLast (cancP :: t) ++ [List.getLast (cancP :: t) p] = cancP :: t
Tactic:
match t with 
| [] =>  simp [p] at *
| h' :: t' =>
  simp [List.dropLast, List.getLast, split_drop]
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
β : Type u_1
l : List β
cancP : β
t : List β
p : [cancP] ≠ []
⊢ List.dropLast [cancP] ++ [List.getLast [cancP] p] = [cancP]
Tactic:
simp [p] at *
State after:
no goals

State before:
α : Type
inst✝ : DecidableEq α
β : Type u_1
l : List β
cancP : β
t : List β
h' : β
t' : List β
p : cancP :: h' :: t' ≠ []
⊢ List.dropLast (cancP :: h' :: t') ++ [List.getLast (cancP :: h' :: t') p] = cancP :: h' :: t'
Tactic:
simp [List.dropLast, List.getLast, split_drop]
State after:
no goals