ι : Type ?u.2756283
α : Type u_1
β : Type ?u.2756289
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h : cycleFactorsFinset f = cycleFactorsFinset g
⊢ f = g
ι : Type ?u.2756283
α : Type u_1
β : Type ?u.2756289
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ Injective cycleFactorsFinset
intro f g h
ι : Type ?u.2756283
α : Type u_1
β : Type ?u.2756289
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h : cycleFactorsFinset f = cycleFactorsFinset g
⊢ noncommProd (cycleFactorsFinset f) id (_ : Set.Pairwise (↑(cycleFactorsFinset f)) _root_.Commute) = g
ι : Type ?u.2756283
α : Type u_1
β : Type ?u.2756289
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h : cycleFactorsFinset f = cycleFactorsFinset g
⊢ f = g
rw [← cycleFactorsFinset_noncommProd f]
no goals
ι : Type ?u.2756283
α : Type u_1
β : Type ?u.2756289
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ f g : Perm α
h : cycleFactorsFinset f = cycleFactorsFinset g
⊢ noncommProd (cycleFactorsFinset f) id (_ : Set.Pairwise (↑(cycleFactorsFinset f)) _root_.Commute) = g
simpa [h] using cycleFactorsFinset_noncommProd g