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

State before:
β : Type ?u.4463
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
g : ↥(alternatingGroup α)
hg : IsThreeCycle ↑g
⊢ g ∈ _root_.commutator ↥(alternatingGroup α)
Tactic:
rw [commutator_eq_closure]
State after:
β : Type ?u.4463
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
g : ↥(alternatingGroup α)
hg : IsThreeCycle ↑g
⊢ g ∈ closure (commutatorSet ↥(alternatingGroup α))

State before:
β : Type ?u.4463
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
g : ↥(alternatingGroup α)
hg : IsThreeCycle ↑g
⊢ g ∈ closure (commutatorSet ↥(alternatingGroup α))
Tactic:
apply Subgroup.subset_closure
State after:
case a
β : Type ?u.4463
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
g : ↥(alternatingGroup α)
hg : IsThreeCycle ↑g
⊢ g ∈ commutatorSet ↥(alternatingGroup α)

State before:
case a
β : Type ?u.4463
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
g : ↥(alternatingGroup α)
hg : IsThreeCycle ↑g
⊢ g ∈ commutatorSet ↥(alternatingGroup α)
Tactic:
exact three_cycle_is_commutator h5 hg
State after:
no goals