case mk
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
x : FreeGroup α
L : List (α × Bool)
⊢ toWord (Quot.mk Red.Step L)⁻¹ = invRev (toWord (Quot.mk Red.Step L))
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
x : FreeGroup α
⊢ toWord x⁻¹ = invRev (toWord x)
rcases x with ⟨L⟩
no goals
case mk
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : DecidableEq α
x : FreeGroup α
L : List (α × Bool)
⊢ toWord (Quot.mk Red.Step L)⁻¹ = invRev (toWord (Quot.mk Red.Step L))
rw [quot_mk_eq_mk, inv_mk, toWord_mk, toWord_mk, reduce_invRev]