[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
n : ℕ
⊢ Normal (derivedSeries G n)
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
⊢ Normal (derivedSeries G Nat.zero)
[PROOFSTEP]
exact (⊤ : Subgroup G).normal_of_characteristic
[GOAL]
case succ
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
n : ℕ
ih : Normal (derivedSeries G n)
⊢ Normal (derivedSeries G (Nat.succ n))
[PROOFSTEP]
exact @Subgroup.commutator_normal G _ (derivedSeries G n) (derivedSeries G n) ih ih
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
n : ℕ
⊢ map f (derivedSeries G n) ≤ derivedSeries G' n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
⊢ map f (derivedSeries G Nat.zero) ≤ derivedSeries G' Nat.zero
[PROOFSTEP]
exact le_top
[GOAL]
case succ
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
n : ℕ
ih : map f (derivedSeries G n) ≤ derivedSeries G' n
⊢ map f (derivedSeries G (Nat.succ n)) ≤ derivedSeries G' (Nat.succ n)
[PROOFSTEP]
simp only [derivedSeries_succ, map_commutator, commutator_mono, ih]
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ↑f
n : ℕ
⊢ derivedSeries G' n ≤ map f (derivedSeries G n)
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ↑f
⊢ derivedSeries G' Nat.zero ≤ map f (derivedSeries G Nat.zero)
[PROOFSTEP]
exact (map_top_of_surjective f hf).ge
[GOAL]
case succ
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ↑f
n : ℕ
ih : derivedSeries G' n ≤ map f (derivedSeries G n)
⊢ derivedSeries G' (Nat.succ n) ≤ map f (derivedSeries G (Nat.succ n))
[PROOFSTEP]
exact commutator_le_map_commutator ih ih
[GOAL]
G✝ : Type u_1
G' : Type u_2
inst✝¹ : Group G✝
inst✝ : Group G'
f : G✝ →* G'
G : Type u_3
hG : Group G
h : ∀ (a b : G), a * b = b * a
⊢ IsSolvable G
[PROOFSTEP]
letI hG' : CommGroup G := { hG with mul_comm := h }
[GOAL]
G✝ : Type u_1
G' : Type u_2
inst✝¹ : Group G✝
inst✝ : Group G'
f : G✝ →* G'
G : Type u_3
hG : Group G
h : ∀ (a b : G), a * b = b * a
hG' : CommGroup G := CommGroup.mk h
⊢ IsSolvable G
[PROOFSTEP]
cases hG
[GOAL]
case mk
G✝ : Type u_1
G' : Type u_2
inst✝¹ : Group G✝
inst✝ : Group G'
f : G✝ →* G'
G : Type u_3
toDivInvMonoid✝ : DivInvMonoid G
mul_left_inv✝ : ∀ (a : G), a⁻¹ * a = 1
h : ∀ (a b : G), a * b = b * a
hG' : CommGroup G := CommGroup.mk h
⊢ IsSolvable G
[PROOFSTEP]
exact CommGroup.isSolvable
[GOAL]
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : Subsingleton G
⊢ ⊤ = ⊥
[PROOFSTEP]
simp
[GOAL]
G : Type u_1
G'✝ : Type u_2
inst✝³ : Group G
inst✝² : Group G'✝
f✝ : G →* G'✝
G' : Type u_3
G'' : Type u_4
inst✝¹ : Group G'
inst✝ : Group G''
f : G' →* G
g : G →* G''
hfg : MonoidHom.ker g ≤ MonoidHom.range f
hG' : IsSolvable G'
hG'' : IsSolvable G''
⊢ IsSolvable G
[PROOFSTEP]
obtain ⟨n, hn⟩ := id hG''
[GOAL]
case mk.intro
G : Type u_1
G'✝ : Type u_2
inst✝³ : Group G
inst✝² : Group G'✝
f✝ : G →* G'✝
G' : Type u_3
G'' : Type u_4
inst✝¹ : Group G'
inst✝ : Group G''
f : G' →* G
g : G →* G''
hfg : MonoidHom.ker g ≤ MonoidHom.range f
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : derivedSeries G'' n = ⊥
⊢ IsSolvable G
[PROOFSTEP]
obtain ⟨m, hm⟩ := id hG'
[GOAL]
case mk.intro.mk.intro
G : Type u_1
G'✝ : Type u_2
inst✝³ : Group G
inst✝² : Group G'✝
f✝ : G →* G'✝
G' : Type u_3
G'' : Type u_4
inst✝¹ : Group G'
inst✝ : Group G''
f : G' →* G
g : G →* G''
hfg : MonoidHom.ker g ≤ MonoidHom.range f
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : derivedSeries G'' n = ⊥
m : ℕ
hm : derivedSeries G' m = ⊥
⊢ IsSolvable G
[PROOFSTEP]
refine' ⟨⟨n + m, le_bot_iff.mp (map_bot f ▸ hm ▸ _)⟩⟩
[GOAL]
case mk.intro.mk.intro
G : Type u_1
G'✝ : Type u_2
inst✝³ : Group G
inst✝² : Group G'✝
f✝ : G →* G'✝
G' : Type u_3
G'' : Type u_4
inst✝¹ : Group G'
inst✝ : Group G''
f : G' →* G
g : G →* G''
hfg : MonoidHom.ker g ≤ MonoidHom.range f
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : derivedSeries G'' n = ⊥
m : ℕ
hm : derivedSeries G' m = ⊥
⊢ derivedSeries G (n + m) ≤ map f (derivedSeries G' m)
[PROOFSTEP]
clear hm
[GOAL]
case mk.intro.mk.intro
G : Type u_1
G'✝ : Type u_2
inst✝³ : Group G
inst✝² : Group G'✝
f✝ : G →* G'✝
G' : Type u_3
G'' : Type u_4
inst✝¹ : Group G'
inst✝ : Group G''
f : G' →* G
g : G →* G''
hfg : MonoidHom.ker g ≤ MonoidHom.range f
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : derivedSeries G'' n = ⊥
m : ℕ
⊢ derivedSeries G (n + m) ≤ map f (derivedSeries G' m)
[PROOFSTEP]
induction' m with m hm
[GOAL]
case mk.intro.mk.intro.zero
G : Type u_1
G'✝ : Type u_2
inst✝³ : Group G
inst✝² : Group G'✝
f✝ : G →* G'✝
G' : Type u_3
G'' : Type u_4
inst✝¹ : Group G'
inst✝ : Group G''
f : G' →* G
g : G →* G''
hfg : MonoidHom.ker g ≤ MonoidHom.range f
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : derivedSeries G'' n = ⊥
⊢ derivedSeries G (n + Nat.zero) ≤ map f (derivedSeries G' Nat.zero)
[PROOFSTEP]
exact
  f.range_eq_map ▸
    ((derivedSeries G n).map_eq_bot_iff.mp (le_bot_iff.mp ((map_derivedSeries_le_derivedSeries g n).trans hn.le))).trans
      hfg
[GOAL]
case mk.intro.mk.intro.succ
G : Type u_1
G'✝ : Type u_2
inst✝³ : Group G
inst✝² : Group G'✝
f✝ : G →* G'✝
G' : Type u_3
G'' : Type u_4
inst✝¹ : Group G'
inst✝ : Group G''
f : G' →* G
g : G →* G''
hfg : MonoidHom.ker g ≤ MonoidHom.range f
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : derivedSeries G'' n = ⊥
m : ℕ
hm : derivedSeries G (n + m) ≤ map f (derivedSeries G' m)
⊢ derivedSeries G (n + Nat.succ m) ≤ map f (derivedSeries G' (Nat.succ m))
[PROOFSTEP]
exact commutator_le_map_commutator hm hm
[GOAL]
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
n : ℕ
⊢ derivedSeries G (Nat.succ n) = _root_.commutator G
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
⊢ derivedSeries G (Nat.succ Nat.zero) = _root_.commutator G
[PROOFSTEP]
exact derivedSeries_one G
[GOAL]
case succ
G : Type u_1
G' : Type u_2
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
[PROOFSTEP]
rw [_root_.derivedSeries_succ, ih, _root_.commutator]
[GOAL]
case succ
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
n : ℕ
ih : derivedSeries G (Nat.succ n) = _root_.commutator G
⊢ ⁅⁅⊤, ⊤⁆, ⁅⊤, ⊤⁆⁆ = ⁅⊤, ⊤⁆
[PROOFSTEP]
cases' (commutator_normal (⊤ : Subgroup G) (⊤ : Subgroup G)).eq_bot_or_eq_top with h h
[GOAL]
case succ.inl
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
n : ℕ
ih : derivedSeries G (Nat.succ n) = _root_.commutator G
h : ⁅⊤, ⊤⁆ = ⊥
⊢ ⁅⁅⊤, ⊤⁆, ⁅⊤, ⊤⁆⁆ = ⁅⊤, ⊤⁆
[PROOFSTEP]
rw [h, commutator_bot_left]
[GOAL]
case succ.inr
G : Type u_1
G' : Type u_2
inst✝² : Group G
inst✝¹ : Group G'
f : G →* G'
inst✝ : IsSimpleGroup G
n : ℕ
ih : derivedSeries G (Nat.succ n) = _root_.commutator G
h : ⁅⊤, ⊤⁆ = ⊤
⊢ ⁅⁅⊤, ⊤⁆, ⁅⊤, ⊤⁆⁆ = ⁅⊤, ⊤⁆
[PROOFSTEP]
rwa [h]
[GOAL]
G : Type u_1
G' : Type u_2
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
[PROOFSTEP]
cases n
[GOAL]
case zero
G : Type u_1
G' : Type u_2
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
[PROOFSTEP]
intro a b
[GOAL]
case zero
G : Type u_1
G' : Type u_2
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
[PROOFSTEP]
refine' (mem_bot.1 _).trans (mem_bot.1 _).symm
[GOAL]
case zero.refine'_1
G : Type u_1
G' : Type u_2
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 ∈ ⊥
[PROOFSTEP]
rw [← hn]
[GOAL]
case zero.refine'_1
G : Type u_1
G' : Type u_2
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 ∈ derivedSeries G Nat.zero
[PROOFSTEP]
exact mem_top _
[GOAL]
case zero.refine'_2
G : Type u_1
G' : Type u_2
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 ∈ ⊥
[PROOFSTEP]
rw [← hn]
[GOAL]
case zero.refine'_2
G : Type u_1
G' : Type u_2
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
[PROOFSTEP]
exact mem_top _
[GOAL]
case succ
G : Type u_1
G' : Type u_2
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
[PROOFSTEP]
rw [IsSimpleGroup.derivedSeries_succ] at hn 
[GOAL]
case succ
G : Type u_1
G' : Type u_2
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
[PROOFSTEP]
intro a b
[GOAL]
case succ
G : Type u_1
G' : Type u_2
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
[PROOFSTEP]
rw [← mul_inv_eq_one, mul_inv_rev, ← mul_assoc, ← mem_bot, ← hn, commutator_eq_closure]
[GOAL]
case succ
G : Type u_1
G' : Type u_2
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)
[PROOFSTEP]
exact subset_closure ⟨a, b, rfl⟩
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
⊢ ¬IsSolvable (Perm (Fin 5))
[PROOFSTEP]
let x : Equiv.Perm (Fin 5) := ⟨![1, 2, 0, 3, 4], ![2, 0, 1, 3, 4], by decide, by decide⟩
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
⊢ Function.LeftInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]
[PROOFSTEP]
decide
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
⊢ Function.RightInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]
[PROOFSTEP]
decide
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
x : Perm (Fin 5) :=
  { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4],
    left_inv := (_ : Function.LeftInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]),
    right_inv := (_ : Function.RightInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]) }
⊢ ¬IsSolvable (Perm (Fin 5))
[PROOFSTEP]
let y : Equiv.Perm (Fin 5) := ⟨![3, 4, 2, 0, 1], ![3, 4, 2, 0, 1], by decide, by decide⟩
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
x : Perm (Fin 5) :=
  { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4],
    left_inv := (_ : Function.LeftInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]),
    right_inv := (_ : Function.RightInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]) }
⊢ Function.LeftInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]
[PROOFSTEP]
decide
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
x : Perm (Fin 5) :=
  { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4],
    left_inv := (_ : Function.LeftInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]),
    right_inv := (_ : Function.RightInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]) }
⊢ Function.RightInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]
[PROOFSTEP]
decide
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
x : Perm (Fin 5) :=
  { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4],
    left_inv := (_ : Function.LeftInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]),
    right_inv := (_ : Function.RightInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]) }
y : Perm (Fin 5) :=
  { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1],
    left_inv := (_ : Function.LeftInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]),
    right_inv := (_ : Function.RightInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]) }
⊢ ¬IsSolvable (Perm (Fin 5))
[PROOFSTEP]
let z : Equiv.Perm (Fin 5) := ⟨![0, 3, 2, 1, 4], ![0, 3, 2, 1, 4], by decide, by decide⟩
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
x : Perm (Fin 5) :=
  { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4],
    left_inv := (_ : Function.LeftInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]),
    right_inv := (_ : Function.RightInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]) }
y : Perm (Fin 5) :=
  { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1],
    left_inv := (_ : Function.LeftInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]),
    right_inv := (_ : Function.RightInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]) }
⊢ Function.LeftInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]
[PROOFSTEP]
decide
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
x : Perm (Fin 5) :=
  { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4],
    left_inv := (_ : Function.LeftInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]),
    right_inv := (_ : Function.RightInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]) }
y : Perm (Fin 5) :=
  { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1],
    left_inv := (_ : Function.LeftInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]),
    right_inv := (_ : Function.RightInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]) }
⊢ Function.RightInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]
[PROOFSTEP]
decide
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
x : Perm (Fin 5) :=
  { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4],
    left_inv := (_ : Function.LeftInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]),
    right_inv := (_ : Function.RightInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]) }
y : Perm (Fin 5) :=
  { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1],
    left_inv := (_ : Function.LeftInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]),
    right_inv := (_ : Function.RightInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]) }
z : Perm (Fin 5) :=
  { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4],
    left_inv := (_ : Function.LeftInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]),
    right_inv := (_ : Function.RightInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]) }
⊢ ¬IsSolvable (Perm (Fin 5))
[PROOFSTEP]
have key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹ := by decide
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
x : Perm (Fin 5) :=
  { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4],
    left_inv := (_ : Function.LeftInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]),
    right_inv := (_ : Function.RightInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]) }
y : Perm (Fin 5) :=
  { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1],
    left_inv := (_ : Function.LeftInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]),
    right_inv := (_ : Function.RightInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]) }
z : Perm (Fin 5) :=
  { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4],
    left_inv := (_ : Function.LeftInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]),
    right_inv := (_ : Function.RightInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]) }
⊢ x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹
[PROOFSTEP]
decide
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
x : Perm (Fin 5) :=
  { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4],
    left_inv := (_ : Function.LeftInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]),
    right_inv := (_ : Function.RightInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]) }
y : Perm (Fin 5) :=
  { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1],
    left_inv := (_ : Function.LeftInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]),
    right_inv := (_ : Function.RightInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]) }
z : Perm (Fin 5) :=
  { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4],
    left_inv := (_ : Function.LeftInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]),
    right_inv := (_ : Function.RightInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]) }
key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹
⊢ ¬IsSolvable (Perm (Fin 5))
[PROOFSTEP]
refine' not_solvable_of_mem_derivedSeries (show x ≠ 1 by decide) fun n => _
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
x : Perm (Fin 5) :=
  { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4],
    left_inv := (_ : Function.LeftInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]),
    right_inv := (_ : Function.RightInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]) }
y : Perm (Fin 5) :=
  { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1],
    left_inv := (_ : Function.LeftInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]),
    right_inv := (_ : Function.RightInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]) }
z : Perm (Fin 5) :=
  { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4],
    left_inv := (_ : Function.LeftInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]),
    right_inv := (_ : Function.RightInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]) }
key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹
⊢ x ≠ 1
[PROOFSTEP]
decide
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
x : Perm (Fin 5) :=
  { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4],
    left_inv := (_ : Function.LeftInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]),
    right_inv := (_ : Function.RightInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]) }
y : Perm (Fin 5) :=
  { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1],
    left_inv := (_ : Function.LeftInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]),
    right_inv := (_ : Function.RightInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]) }
z : Perm (Fin 5) :=
  { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4],
    left_inv := (_ : Function.LeftInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]),
    right_inv := (_ : Function.RightInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]) }
key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹
n : ℕ
⊢ x ∈ derivedSeries (Perm (Fin 5)) n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
x : Perm (Fin 5) :=
  { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4],
    left_inv := (_ : Function.LeftInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]),
    right_inv := (_ : Function.RightInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]) }
y : Perm (Fin 5) :=
  { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1],
    left_inv := (_ : Function.LeftInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]),
    right_inv := (_ : Function.RightInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]) }
z : Perm (Fin 5) :=
  { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4],
    left_inv := (_ : Function.LeftInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]),
    right_inv := (_ : Function.RightInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]) }
key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹
⊢ x ∈ derivedSeries (Perm (Fin 5)) Nat.zero
[PROOFSTEP]
exact mem_top x
[GOAL]
case succ
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
x : Perm (Fin 5) :=
  { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4],
    left_inv := (_ : Function.LeftInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]),
    right_inv := (_ : Function.RightInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]) }
y : Perm (Fin 5) :=
  { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1],
    left_inv := (_ : Function.LeftInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]),
    right_inv := (_ : Function.RightInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]) }
z : Perm (Fin 5) :=
  { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4],
    left_inv := (_ : Function.LeftInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]),
    right_inv := (_ : Function.RightInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]) }
key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹
n : ℕ
ih : x ∈ derivedSeries (Perm (Fin 5)) n
⊢ x ∈ derivedSeries (Perm (Fin 5)) (Nat.succ n)
[PROOFSTEP]
rw [key, (derivedSeries_normal _ _).mem_comm_iff, inv_mul_cancel_left]
[GOAL]
case succ
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
x : Perm (Fin 5) :=
  { toFun := ![1, 2, 0, 3, 4], invFun := ![2, 0, 1, 3, 4],
    left_inv := (_ : Function.LeftInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]),
    right_inv := (_ : Function.RightInverse ![2, 0, 1, 3, 4] ![1, 2, 0, 3, 4]) }
y : Perm (Fin 5) :=
  { toFun := ![3, 4, 2, 0, 1], invFun := ![3, 4, 2, 0, 1],
    left_inv := (_ : Function.LeftInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]),
    right_inv := (_ : Function.RightInverse ![3, 4, 2, 0, 1] ![3, 4, 2, 0, 1]) }
z : Perm (Fin 5) :=
  { toFun := ![0, 3, 2, 1, 4], invFun := ![0, 3, 2, 1, 4],
    left_inv := (_ : Function.LeftInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]),
    right_inv := (_ : Function.RightInverse ![0, 3, 2, 1, 4] ![0, 3, 2, 1, 4]) }
key : x = z * ⁅x, y * x * y⁻¹⁆ * z⁻¹
n : ℕ
ih : x ∈ derivedSeries (Perm (Fin 5)) n
⊢ ⁅x, y * x * y⁻¹⁆ ∈ derivedSeries (Perm (Fin 5)) (Nat.succ n)
[PROOFSTEP]
exact commutator_mem_commutator ih ((derivedSeries_normal _ _).conj_mem _ ih _)
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
X : Type u_3
hX : 5 ≤ Cardinal.mk X
⊢ ¬IsSolvable (Perm X)
[PROOFSTEP]
intro h
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
X : Type u_3
hX : 5 ≤ Cardinal.mk X
h : IsSolvable (Perm X)
⊢ False
[PROOFSTEP]
have key : Nonempty (Fin 5 ↪ X) := by
  rwa [← Cardinal.lift_mk_le, Cardinal.mk_fin, Cardinal.lift_natCast, Cardinal.lift_id]
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
X : Type u_3
hX : 5 ≤ Cardinal.mk X
h : IsSolvable (Perm X)
⊢ Nonempty (Fin 5 ↪ X)
[PROOFSTEP]
rwa [← Cardinal.lift_mk_le, Cardinal.mk_fin, Cardinal.lift_natCast, Cardinal.lift_id]
[GOAL]
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
X : Type u_3
hX : 5 ≤ Cardinal.mk X
h : IsSolvable (Perm X)
key : Nonempty (Fin 5 ↪ X)
⊢ False
[PROOFSTEP]
exact
  Equiv.Perm.fin_5_not_solvable
    (solvable_of_solvable_injective (Equiv.Perm.viaEmbeddingHom_injective (Nonempty.some key)))
