Ore's conjecture on commutators in finite non-abelian simple groups

Let $G$ be a finite non-abelian simple group, and let $g\in G$. A commutator is an element of the form $xyx^{-1}y^{-1}$ for some $x,y\in G$. Ore's conjecture. Every element $g\in G$ is a commutator; that is, there exist $x,y\in G$ such that

$$g=xyx^{-1}y^{-1}.$$

The conjecture concerns the surjectivity of the commutator map on finite non-abelian simple groups and is presented here as an example of a machine-assisted proof. Its resolution status is not specified in the supplied text.