Theorem: Equiv.Perm.commute_of_mem_cycleFactorsFinset_commute (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k g : Perm α
hk : ∀ c ∈ cycleFactorsFinset g, Commute k c
⊢ Commute k g
Tactic:
rw [← Equiv.Perm.cycleFactorsFinset_noncommProd g (Equiv.Perm.cycleFactorsFinset_mem_commute g)]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k g : Perm α
hk : ∀ c ∈ cycleFactorsFinset g, Commute k c
⊢ Commute k (Finset.noncommProd (cycleFactorsFinset g) id ⋯)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k g : Perm α
hk : ∀ c ∈ cycleFactorsFinset g, Commute k c
⊢ Commute k (Finset.noncommProd (cycleFactorsFinset g) id ⋯)
Tactic:
apply Finset.noncommProd_commute
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k g : Perm α
hk : ∀ c ∈ cycleFactorsFinset g, Commute k c
⊢ ∀ x ∈ cycleFactorsFinset g, Commute k (id x)

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k g : Perm α
hk : ∀ c ∈ cycleFactorsFinset g, Commute k c
⊢ ∀ x ∈ cycleFactorsFinset g, Commute k (id x)
Tactic:
simp only [id.def]
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k g : Perm α
hk : ∀ c ∈ cycleFactorsFinset g, Commute k c
⊢ ∀ x ∈ cycleFactorsFinset g, Commute k x

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k g : Perm α
hk : ∀ c ∈ cycleFactorsFinset g, Commute k c
⊢ ∀ x ∈ cycleFactorsFinset g, Commute k x
Tactic:
exact hk
State after:
no goals