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

State before:
α : Type
inst✝ : DecidableEq α
start : List (α × Bool)
nonnil : start ≠ []
letter : α × Bool
neq : List.getLast start nonnil ≠ letter⁻¹
⊢ start :+ letter = List.concat start letter
Tactic:
simp [nextVertex,  neq, if_neg, nonnil]
State after:
no goals