case zero
G : Type u_1
G' : Type ?u.73657
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
⊢ derivedSeries G (Nat.succ Nat.zero) = _root_.commutator G

case succ
G : Type u_1
G' : Type ?u.73657
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
n : ℕ
ih : derivedSeries G (Nat.succ n) = _root_.commutator G
⊢ derivedSeries G (Nat.succ (Nat.succ n)) = _root_.commutator G
G : Type u_1
G' : Type ?u.73657
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
n : ℕ
⊢ derivedSeries G (Nat.succ n) = _root_.commutator G
induction' n with n ih
case succ
G : Type u_1
G' : Type ?u.73657
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
n : ℕ
ih : derivedSeries G (Nat.succ n) = _root_.commutator G
⊢ ⁅⁅⊤, ⊤⁆, ⁅⊤, ⊤⁆⁆ = ⁅⊤, ⊤⁆
case succ
G : Type u_1
G' : Type ?u.73657
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
n : ℕ
ih : derivedSeries G (Nat.succ n) = _root_.commutator G
⊢ derivedSeries G (Nat.succ (Nat.succ n)) = _root_.commutator G
rw [_root_.derivedSeries_succ, ih, _root_.commutator]
case succ.inl
G : Type u_1
G' : Type ?u.73657
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
n : ℕ
ih : derivedSeries G (Nat.succ n) = _root_.commutator G
h : ⁅⊤, ⊤⁆ = ⊥
⊢ ⁅⁅⊤, ⊤⁆, ⁅⊤, ⊤⁆⁆ = ⁅⊤, ⊤⁆

case succ.inr
G : Type u_1
G' : Type ?u.73657
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
n : ℕ
ih : derivedSeries G (Nat.succ n) = _root_.commutator G
h : ⁅⊤, ⊤⁆ = ⊤
⊢ ⁅⁅⊤, ⊤⁆, ⁅⊤, ⊤⁆⁆ = ⁅⊤, ⊤⁆
case succ
G : Type u_1
G' : Type ?u.73657
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
n : ℕ
ih : derivedSeries G (Nat.succ n) = _root_.commutator G
⊢ ⁅⁅⊤, ⊤⁆, ⁅⊤, ⊤⁆⁆ = ⁅⊤, ⊤⁆
cases' (commutator_normal (⊤ : Subgroup G) (⊤ : Subgroup G)).eq_bot_or_eq_top with h h
no goals
case zero
G : Type u_1
G' : Type ?u.73657
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
⊢ derivedSeries G (Nat.succ Nat.zero) = _root_.commutator G
exact derivedSeries_one G
no goals
case succ.inl
G : Type u_1
G' : Type ?u.73657
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
n : ℕ
ih : derivedSeries G (Nat.succ n) = _root_.commutator G
h : ⁅⊤, ⊤⁆ = ⊥
⊢ ⁅⁅⊤, ⊤⁆, ⁅⊤, ⊤⁆⁆ = ⁅⊤, ⊤⁆
rw [h, commutator_bot_left]
no goals
case succ.inr
G : Type u_1
G' : Type ?u.73657
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
n : ℕ
ih : derivedSeries G (Nat.succ n) = _root_.commutator G
h : ⁅⊤, ⊤⁆ = ⊤
⊢ ⁅⁅⊤, ⊤⁆, ⁅⊤, ⊤⁆⁆ = ⁅⊤, ⊤⁆
rwa [h]