Theorem: Word.mul_eps (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