-- Mathlib/GroupTheory/Solvable.lean
theorem IsSimpleGroup.comm_iff_isSolvable : (∀ a b : G, a * b = b * a) ↔ IsSolvable G :=
  ⟨isSolvable_of_comm, fun ⟨⟨n, hn⟩⟩ => by
    cases n
    · intro a b
      refine (mem_bot.1 ?_).trans (mem_bot.1 ?_).symm <;>
        · rw [← hn]
          exact mem_top _
    · rw [IsSimpleGroup.derivedSeries_succ] at hn
      intro a b
      rw [← mul_inv_eq_one, mul_inv_rev, ← mul_assoc, ← mem_bot, ← hn, commutator_eq_closure]
      exact subset_closure ⟨a, b, rfl⟩⟩

Proof state:
case succ
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
n✝ : ℕ
hn : _root_.commutator G = ⊥
a b : G
⊢ a * b * a⁻¹ * b⁻¹ ∈ closure (commutatorSet G)

Tactic:
exact subset_closure ⟨a, b, rfl⟩

Result:
no goals

Proof state:
case zero.refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
hn : derivedSeries G 0 = ⊥
a b : G
⊢ b * a ∈ ⊥

Tactic:
rw [← hn]

Result:
case zero.refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
hn : derivedSeries G 0 = ⊥
a b : G
⊢ b * a ∈ derivedSeries G 0

Proof state:
case succ
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
n✝ : ℕ
hn : _root_.commutator G = ⊥
a b : G
⊢ a * b = b * a

Tactic:
rw [← mul_inv_eq_one, mul_inv_rev, ← mul_assoc, ← mem_bot, ← hn, commutator_eq_closure]

Result:
case succ
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
n✝ : ℕ
hn : _root_.commutator G = ⊥
a b : G
⊢ a * b * a⁻¹ * b⁻¹ ∈ closure (commutatorSet G)

Proof state:
case succ
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
n✝ : ℕ
hn : derivedSeries G (n✝ + 1) = ⊥
⊢ ∀ (a b : G), a * b = b * a

Tactic:
rw [IsSimpleGroup.derivedSeries_succ] at hn

Result:
case succ
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
n✝ : ℕ
hn : _root_.commutator G = ⊥
⊢ ∀ (a b : G), a * b = b * a

Proof state:
case zero.refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
hn : derivedSeries G 0 = ⊥
a b : G
⊢ b * a ∈ derivedSeries G 0

Tactic:
exact mem_top _

Result:
no goals

Proof state:
case succ
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
n✝ : ℕ
hn : _root_.commutator G = ⊥
⊢ ∀ (a b : G), a * b = b * a

Tactic:
intro a b

Result:
case succ
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
n✝ : ℕ
hn : _root_.commutator G = ⊥
a b : G
⊢ a * b = b * a

Proof state:
case zero
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
hn : derivedSeries G 0 = ⊥
⊢ ∀ (a b : G), a * b = b * a

Tactic:
intro a b

Result:
case zero
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
hn : derivedSeries G 0 = ⊥
a b : G
⊢ a * b = b * a

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
n : ℕ
hn : derivedSeries G n = ⊥
⊢ ∀ (a b : G), a * b = b * a

Tactic:
cases n

Result:
case zero
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
hn : derivedSeries G 0 = ⊥
⊢ ∀ (a b : G), a * b = b * a

case succ
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
n✝ : ℕ
hn : derivedSeries G (n✝ + 1) = ⊥
⊢ ∀ (a b : G), a * b = b * a