The Ore conjecture: every element of a finite nonabelian simple group is a commutator

Problem statement

Notes: This is Theorem 1 of the cited paper.

Source: Martin W. Liebeck, E. A. O'Brien, Aner Shalev, and Pham Huu Tiep, *The Ore conjecture*, Journal of the European Mathematical Society 12 (2010), no. 4, 939–1008, Theorem 1, https://doi.org/10.4171/JEMS/220; https://ems.press/journals/jems/articles/3979.

Informal solution: See the cited paper for the proof.

theorem declaration uses `sorry`ore_conjecture (G : Type*) [Group G] [Finite G] [IsSimpleGroup G]
    (hG : ¬ IsMulCommutative G) :
    commutatorSet G = Set.univ := byG:Type u_1inst✝²:Group Ginst✝¹:Finite Ginst✝:IsSimpleGroup GhG:¬IsMulCommutative G⊢ commutatorSet G = Set.univ
  sorryAll goals completed! 🐙