English
If two words represent the same element in the free group (mk L1 = mk L2), then their maximal reductions coincide: reduce L1 = reduce L2.
Русский
Если mk L1 = mk L2, то их максимальные редукции совпадают: reduce L1 = reduce L2.
LaTeX
$$$$\text{If } \operatorname{mk}L_1 = \operatorname{mk}L_2, \; \operatorname{reduce}L_1 = \operatorname{reduce}L_2.$$$$
Lean4
/-- If two words correspond to the same element in the free group, then they
have a common maximal reduction. This is the proof that the function that sends
an element of the free group to its maximal reduction is well-defined. -/
@[to_additive /-- If two words correspond to the same element in the additive free group, then they
have a common maximal reduction. This is the proof that the function that sends an element of the
free group to its maximal reduction is well-defined. -/
]
theorem sound (H : mk L₁ = mk L₂) : reduce L₁ = reduce L₂ :=
let ⟨_L₃, H13, H23⟩ := Red.exact.1 H
(reduce.eq_of_red H13).trans (reduce.eq_of_red H23).symm
