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

State before:
α : Type
inst✝ : DecidableEq α
g : FreeGroup α
⊢ mk (reducedWord g) = g
Tactic:
apply Quot.ind (β := fun g ↦ mk (reducedWord g) = g )
State after:
case mk
α : Type
inst✝ : DecidableEq α
g : FreeGroup α
⊢ ∀ (a : List (α × Bool)), mk (reducedWord (Quot.mk Step a)) = Quot.mk Step a

State before:
case mk
α : Type
inst✝ : DecidableEq α
g : FreeGroup α
⊢ ∀ (a : List (α × Bool)), mk (reducedWord (Quot.mk Step a)) = Quot.mk Step a
Tactic:
intro word
State after:
case mk
α : Type
inst✝ : DecidableEq α
g : FreeGroup α
word : List (α × Bool)
⊢ mk (reducedWord (Quot.mk Step word)) = Quot.mk Step word

State before:
case mk
α : Type
inst✝ : DecidableEq α
g : FreeGroup α
word : List (α × Bool)
⊢ mk (reducedWord (Quot.mk Step word)) = Quot.mk Step word
Tactic:
simp [finalVertex_homotopic_append [], ←finalVertexOnFreeGroup_natural]
State after:
case mk
α : Type
inst✝ : DecidableEq α
g : FreeGroup α
word : List (α × Bool)
⊢ mk (finalVertex [] word) = mk word

State before:
case mk
α : Type
inst✝ : DecidableEq α
g : FreeGroup α
word : List (α × Bool)
⊢ mk (finalVertex [] word) = mk word
Tactic:
simp [←finalVertex_homotopic_append]
State after:
no goals