Theorem: alternatingGroup_is_perfect (Jordan/Mathlib/Alternating.lean)

State before:
β : Type ?u.5450
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
⊢ _root_.commutator ↥(alternatingGroup α) = ⊤
Tactic:
suffices closure {b : alternatingGroup α | (b : Perm α).IsThreeCycle} = ⊤ by
  rw [eq_top_iff, ← this, Subgroup.closure_le]
  intro b hb
  exact three_cycle_mem_commutator h5 hb
State after:
β : Type ?u.5450
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
⊢ closure {b | IsThreeCycle ↑b} = ⊤

State before:
β : Type ?u.5450
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
⊢ closure {b | IsThreeCycle ↑b} = ⊤
Tactic:
apply Subgroup.closure_closure_coe_preimage
State after:
no goals

State before:
β : Type ?u.5450
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
this : closure {b | IsThreeCycle ↑b} = ⊤
⊢ _root_.commutator ↥(alternatingGroup α) = ⊤
Tactic:
rw [eq_top_iff, ← this, Subgroup.closure_le]
State after:
β : Type ?u.5450
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
this : closure {b | IsThreeCycle ↑b} = ⊤
⊢ {b | IsThreeCycle ↑b} ⊆ ↑(_root_.commutator ↥(alternatingGroup α))

State before:
β : Type ?u.5450
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
this : closure {b | IsThreeCycle ↑b} = ⊤
⊢ {b | IsThreeCycle ↑b} ⊆ ↑(_root_.commutator ↥(alternatingGroup α))
Tactic:
intro b hb
State after:
β : Type ?u.5450
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
this : closure {b | IsThreeCycle ↑b} = ⊤
b : ↥(alternatingGroup α)
hb : b ∈ {b | IsThreeCycle ↑b}
⊢ b ∈ ↑(_root_.commutator ↥(alternatingGroup α))

State before:
β : Type ?u.5450
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
this : closure {b | IsThreeCycle ↑b} = ⊤
b : ↥(alternatingGroup α)
hb : b ∈ {b | IsThreeCycle ↑b}
⊢ b ∈ ↑(_root_.commutator ↥(alternatingGroup α))
Tactic:
exact three_cycle_mem_commutator h5 hb
State after:
no goals