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

State before:
β : Type ?u.44
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
g : ↥(alternatingGroup α)
hg : IsThreeCycle ↑g
⊢ g ∈ commutatorSet ↥(alternatingGroup α)
Tactic:
apply mem_commutatorSet_of_isConj_sq
State after:
case hg
β : Type ?u.44
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
g : ↥(alternatingGroup α)
hg : IsThreeCycle ↑g
⊢ IsConj g (g ^ 2)

State before:
case hg
β : Type ?u.44
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
g : ↥(alternatingGroup α)
hg : IsThreeCycle ↑g
⊢ IsConj g (g ^ 2)
Tactic:
apply alternatingGroup.isThreeCycle_isConj h5 hg
State after:
case hg
β : Type ?u.44
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
g : ↥(alternatingGroup α)
hg : IsThreeCycle ↑g
⊢ IsThreeCycle ↑(g ^ 2)

State before:
case hg
β : Type ?u.44
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Fintype.card α
g : ↥(alternatingGroup α)
hg : IsThreeCycle ↑g
⊢ IsThreeCycle ↑(g ^ 2)
Tactic:
exact hg.isThreeCycle_sq
State after:
no goals