Relatively simple identities that take long to prove

Question

Can someone give examples of identities, that is, universally quantified equations, that are relatively simple but is very lengthy and/or difficult to prove? I want examples from algebraic structures, not just the standard groups, rings, and fields, but more exotic algebras, like lattices, Boolean algebras, etc. I managed to prove a simple identity myself which required a page of lemmas and algebraic manipulations. That is why I am asking if there are other examples of relatively simple identities which require pages of algebra to prove.

Answer 1

Let $G$ be a finitely generated group of exponent $2^n$ and $a$ be an element in $G$ of order 2, then for every $x\in G$ we have $$[...[x,\underbrace {a],a],...,a]}_{n+1}=1.$$

This identity requires quite a few pages of proof. Even simpler looking formula: if $G$ is a finite $m$-generator group of prime exponent $p$ then the $G$ is nilpotent of class at most

$$\underbrace{m^{m^{...{m}}}}_{3^p}$$

The article by Vaughan-Lee and Zelmanov proving it has about 10 pages but it relies on some heavy results.