-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
set set₁ : Nat.card.{u_1} ↥(MonoidHom.range (toPermHom g)) = ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
set₂ :
  let sc : (c : ↥g.cycleFactorsFinset) → ℕ := fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support;
  ∀ (hsc : sc = fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support),
    Nat.card.{u_1} ↥(MonoidHom.range (toPermHom g)) = ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
set₃ :
  let sc : (c : ↥g.cycleFactorsFinset) → ℕ := fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support;
  ∀ (hsc : sc = fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support),
    Fintype.card.{u_1} ↥(MonoidHom.range (toPermHom g)) =
      Fintype.card.{u_1}
        (↑{k : Perm ↥g.cycleFactorsFinset | sc ∘ (⇑k : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) = sc} :
          Type u_1)
set₄ :
  let sc : (c : ↥g.cycleFactorsFinset) → ℕ := fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support;
  ∀ (hsc : sc = fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support),
    Nat.card.{u_1} ↥(MonoidHom.range (toPermHom g)) =
      Nat.card.{u_1}
        (↑{k : Perm ↥g.cycleFactorsFinset | sc ∘ (⇑k : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) = sc} :
          Type u_1)
e_α :
  let sc : (c : ↥g.cycleFactorsFinset) → ℕ := fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support;
  ∀ (hsc : sc = fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support),
    Eq.{u_1 + 1} (α := Perm ↥g.cycleFactorsFinset → Prop)
      (fun (x : Perm ↥g.cycleFactorsFinset) ↦
        Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (MonoidHom.range (toPermHom g)) x)
      fun (x : Perm ↥g.cycleFactorsFinset) ↦
      Membership.mem (γ := Set (Perm ↥g.cycleFactorsFinset))
        {k : Perm ↥g.cycleFactorsFinset | sc ∘ (⇑k : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) = sc} x
e_α₁ :
  let sc : (c : ↥g.cycleFactorsFinset) → ℕ := fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support;
  ∀ (hsc : sc = fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support) (x : Perm ↥g.cycleFactorsFinset),
    Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (MonoidHom.range (toPermHom g)) x ↔
      Membership.mem (γ := Set (Perm ↥g.cycleFactorsFinset))
        {k : Perm ↥g.cycleFactorsFinset | sc ∘ (⇑k : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) = sc} x
⊢ Nat.card.{u_1} ↥(MonoidHom.range (toPermHom g)) = ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!

Tactic:
classical
  set sc := fun (c : g.cycleFactorsFinset) ↦ #c.val.support with hsc
  suffices Fintype.card (toPermHom g).range =
    Fintype.card { k : Perm g.cycleFactorsFinset | sc ∘ k = sc } by
    simp only [Nat.card_eq_fintype_card, this, Set.coe_setOf, DomMulAct.stabilizer_card', hsc,
      Finset.univ_eq_attach]
    simp_rw [← CycleType.count_def]
    apply Finset.prod_congr _ (fun _ _ => rfl)
    ext n
    simp only [Finset.mem_image, Finset.mem_attach,
        true_and, Subtype.exists, exists_prop, Multiset.mem_toFinset]
    simp only [cycleType_def, Function.comp_apply, Multiset.mem_map, Finset.mem_val]
  simp only [Fintype.card_eq_nat_card]
  congr
  ext
  rw [mem_range_toPermHom_iff', Set.mem_setOf_eq]

Premises used: Equiv.Perm.support, Equiv.Perm.OnCycleFactors.mem_range_toPermHom_iff', Set.mem_setOf_eq, Finset.card, Subtype.val, Fintype.card_eq_nat_card