-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
rw :
  Nat.card.{u_1} ↥(MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (OnCycleFactors.toPermHom g)) *
      (MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (OnCycleFactors.toPermHom g)).index =
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod * ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
rw₁ :
  Nat.card.{u_1} ↥(MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (OnCycleFactors.toPermHom g)) *
      Nat.card.{u_1} ↥(MonoidHom.range (OnCycleFactors.toPermHom g)) =
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod * ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
rw₂ :
  Nat.card.{u_1} ↥(MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (OnCycleFactors.toPermHom g)) *
      ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)! =
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod * ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
rw₃ :
  Nat.card.{u_1} ↥(MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (OnCycleFactors.toPermHom g)) *
      ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)! =
    Fintype.card.{u_1}
        ↥(MonoidHom.range (G :=
            Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
              ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))))
            (kerParam g)) *
      ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
rw₄ :
  Nat.card.{u_1} ↥(MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (OnCycleFactors.toPermHom g)) *
      ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)! =
    Nat.card.{u_1}
        ↥(MonoidHom.range (G :=
            Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
              ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))))
            (kerParam g)) *
      ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
rw₅ :
  Nat.card.{u_1} ↥(MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (OnCycleFactors.toPermHom g)) *
      ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)! =
    Nat.card.{u_1}
        ↥(map (Subgroup.subtype (centralizer {g}))
            (MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (OnCycleFactors.toPermHom g))) *
      ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
rw₆ rw₇ :
  Nat.card.{u_1} ↥(MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (OnCycleFactors.toPermHom g)) *
      ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)! =
    Nat.card.{u_1} ↥(MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (OnCycleFactors.toPermHom g)) *
      ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
⊢ Nat.card.{u_1} ↥(centralizer {g}) =
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod * ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!

Tactic:
rw [← (toPermHom g).ker.card_mul_index, index_ker, nat_card_range_toPermHom,
    ← kerParam_range_card, ← Nat.card_eq_fintype_card, kerParam_range_eq, card_subtype]

Premises used: Equiv.Perm.OnCycleFactors.kerParam_range_card, Equiv.Perm.OnCycleFactors.nat_card_range_toPermHom, Subgroup.index_ker, MonoidHom.ker, Equiv.Perm.OnCycleFactors.toPermHom, Subgroup.card_subtype, Subgroup.card_mul_index, Equiv.Perm.OnCycleFactors.kerParam_range_eq, Nat.card_eq_fintype_card