case zero
G : Type u_1
G' : Type ?u.84178
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
hn : derivedSeries G Nat.zero = ⊥
⊢ ∀ (a b : G), a * b = b * a

case succ
G : Type u_1
G' : Type ?u.84178
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
n✝ : ℕ
hn : derivedSeries G (Nat.succ n✝) = ⊥
⊢ ∀ (a b : G), a * b = b * a
G : Type u_1
G' : Type ?u.84178
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
n : ℕ
hn : derivedSeries G n = ⊥
⊢ ∀ (a b : G), a * b = b * a
cases n
case zero
G : Type u_1
G' : Type ?u.84178
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
hn : derivedSeries G Nat.zero = ⊥
a b : G
⊢ a * b = b * a
case zero
G : Type u_1
G' : Type ?u.84178
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
hn : derivedSeries G Nat.zero = ⊥
⊢ ∀ (a b : G), a * b = b * a
intro a b
case zero.refine'_2
G : Type u_1
G' : Type ?u.84178
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
hn : derivedSeries G Nat.zero = ⊥
a b : G
⊢ b * a ∈ derivedSeries G Nat.zero
case zero.refine'_2
G : Type u_1
G' : Type ?u.84178
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
hn : derivedSeries G Nat.zero = ⊥
a b : G
⊢ b * a ∈ ⊥
rw [← hn]
no goals
case zero.refine'_2
G : Type u_1
G' : Type ?u.84178
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
hn : derivedSeries G Nat.zero = ⊥
a b : G
⊢ b * a ∈ derivedSeries G Nat.zero
exact mem_top _
case succ
G : Type u_1
G' : Type ?u.84178
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
n✝ : ℕ
hn : _root_.commutator G = ⊥
⊢ ∀ (a b : G), a * b = b * a
case succ
G : Type u_1
G' : Type ?u.84178
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
n✝ : ℕ
hn : derivedSeries G (Nat.succ n✝) = ⊥
⊢ ∀ (a b : G), a * b = b * a
rw [IsSimpleGroup.derivedSeries_succ] at hn
case succ
G : Type u_1
G' : Type ?u.84178
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
n✝ : ℕ
hn : _root_.commutator G = ⊥
a b : G
⊢ a * b = b * a
case succ
G : Type u_1
G' : Type ?u.84178
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
n✝ : ℕ
hn : _root_.commutator G = ⊥
⊢ ∀ (a b : G), a * b = b * a
intro a b
case succ
G : Type u_1
G' : Type ?u.84178
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
n✝ : ℕ
hn : _root_.commutator G = ⊥
a b : G
⊢ a * b * a⁻¹ * b⁻¹ ∈ closure (commutatorSet G)
case succ
G : Type u_1
G' : Type ?u.84178
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
n✝ : ℕ
hn : _root_.commutator G = ⊥
a b : G
⊢ a * b = b * a
rw [← mul_inv_eq_one, mul_inv_rev, ← mul_assoc, ← mem_bot, ← hn, commutator_eq_closure]
no goals
case succ
G : Type u_1
G' : Type ?u.84178
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
x✝ : IsSolvable G
n✝ : ℕ
hn : _root_.commutator G = ⊥
a b : G
⊢ a * b * a⁻¹ * b⁻¹ ∈ closure (commutatorSet G)
exact subset_closure ⟨a, b, rfl⟩