Word in reduced form

Stream: new members

[Giacomo Maletto]

Suppose I'm working with an element of free_group α and I want to express "let $v = v_1^{\epsilon_1} \dots v_k^{\epsilon_k}$ be its reduced form". If α has decidable_eq I think I can use the reduce function together with theorem reduce.self, but is it possible to prove a general statement like "a word always admits reduced form"?

[David Wärn]

Yes, every type has decidable equality if you're working classically

[Reid Barton]

And if every word has a reduced form then α must have decidable equality, because given $x$ and $y$ you can look at the reduced form of $xy^{-1}$ to decide whether $x = y$

[Giacomo Maletto]

Interesting, and how do you tell Lean that every type has decidable equality?

[Giacomo Maletto]

That is to say, how can I use that fact in a proof?

[Kevin Buzzard]

Use the classical tactic in your proof