Theorem: alternatingGroup.commutator_group_eq (Jordan/Mathlib/Alternating.lean)

State before:
β : Type ?u.9373
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
⊢ _root_.commutator (Perm α) = alternatingGroup α
Tactic:
apply le_antisymm alternatingGroup.commutator_group_le
State after:
β : Type ?u.9373
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
⊢ alternatingGroup α ≤ _root_.commutator (Perm α)

State before:
β : Type ?u.9373
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
⊢ alternatingGroup α ≤ _root_.commutator (Perm α)
Tactic:
rw [← alternatingGroup_is_perfect' h5]
State after:
β : Type ?u.9373
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
⊢ ⁅alternatingGroup α, alternatingGroup α⁆ ≤ _root_.commutator (Perm α)

State before:
β : Type ?u.9373
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
⊢ ⁅alternatingGroup α, alternatingGroup α⁆ ≤ _root_.commutator (Perm α)
Tactic:
exact commutator_mono le_top le_top
State after:
no goals