Theorem: Word.eps_mul (FormalSystems/Preliminaries/Word.lean)

State before:
α✝ : Type u_1
w : Word α✝
⊢ ε * w = w
Tactic:
simp
State after:
α✝ : Type u_1
w : Word α✝
⊢ ε = 1

State before:
α✝ : Type u_1
w : Word α✝
⊢ ε = 1
Tactic:
rfl
State after:
no goals