∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (g : Equiv.Perm α),
  Nat.card ↥(Subgroup.centralizer {g}) =
    (Fintype.card α - g.cycleType.sum).factorial * g.cycleType.prod *
      ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType).factorial