-- Mathlib/GroupTheory/Perm/Centralizer.lean
theorem card_of_cycleType_mul_eq (m : Multiset ℕ) :
    ({g | g.cycleType = m} : Finset (Perm α)).card *
      ((Fintype.card α - m.sum)! * m.prod * (∏ n ∈ m.toFinset, (m.count n)!)) =
      if (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) then (Fintype.card α)! else 0

Proof state:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hm : g.cycleType.sum ≤ Fintype.card α ∧ ∀ a ∈ g.cycleType, 2 ≤ a
⊢ (Finset.filter (fun g_1 => g_1.cycleType = g.cycleType) Finset.univ).card = Nat.card ↑{h | IsConj g h}

Tactic:
simp_rw [Set.coe_setOf, Nat.card_eq_fintype_card, ← Fintype.card_coe, Finset.mem_filter,
  Finset.mem_univ, true_and, ← isConj_iff_cycleType_eq, isConj_comm (g := g)]

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hm : m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
⊢ (Finset.filter (fun g => g.cycleType = m) Finset.univ).card *
      ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) =
    (Fintype.card α)!

Tactic:
obtain ⟨g, rfl⟩ := (exists_with_cycleType_iff α).mpr hm

Result:
case pos.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hm : g.cycleType.sum ≤ Fintype.card α ∧ ∀ a ∈ g.cycleType, 2 ≤ a
⊢ (Finset.filter (fun g_1 => g_1.cycleType = g.cycleType) Finset.univ).card *
      ((Fintype.card α - g.cycleType.sum)! * g.cycleType.prod *
        ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!) =
    (Fintype.card α)!

Proof state:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hm : ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ (Finset.filter (fun g => g.cycleType = m) Finset.univ).card = 0

Tactic:
exact (card_of_cycleType_eq_zero_iff α).mpr hm

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hm : ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ (Finset.filter (fun g => g.cycleType = m) Finset.univ).card *
      ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) =
    0

Tactic:
convert MulZeroClass.zero_mul _

Result:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hm : ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ (Finset.filter (fun g => g.cycleType = m) Finset.univ).card = 0

Proof state:
case pos.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hm : g.cycleType.sum ≤ Fintype.card α ∧ ∀ a ∈ g.cycleType, 2 ≤ a
⊢ (Finset.filter (fun g_1 => g_1.cycleType = g.cycleType) Finset.univ).card *
      ((Fintype.card α - g.cycleType.sum)! * g.cycleType.prod *
        ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!) =
    (Fintype.card α)!

Tactic:
convert card_isConj_mul_eq g

Result:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
hm : g.cycleType.sum ≤ Fintype.card α ∧ ∀ a ∈ g.cycleType, 2 ≤ a
⊢ (Finset.filter (fun g_1 => g_1.cycleType = g.cycleType) Finset.univ).card = Nat.card ↑{h | IsConj g h}

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
⊢ (Finset.filter (fun g => g.cycleType = m) Finset.univ).card *
      ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) =
    if m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then (Fintype.card α)! else 0

Tactic:
split_ifs with hm

Result:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hm : m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
⊢ (Finset.filter (fun g => g.cycleType = m) Finset.univ).card *
      ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) =
    (Fintype.card α)!

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hm : ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ (Finset.filter (fun g => g.cycleType = m) Finset.univ).card *
      ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) =
    0

Proof state:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
hm : m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
⊢ (Finset.filter (fun g => g.cycleType = m) Finset.univ).card *
      ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) =
    (Fintype.card α)!

Tactic:
classical
obtain ⟨g, rfl⟩ := (exists_with_cycleType_iff α).mpr hm
convert card_isConj_mul_eq g
simp_rw [Set.coe_setOf, Nat.card_eq_fintype_card, ← Fintype.card_coe, Finset.mem_filter,
  Finset.mem_univ, true_and, ← isConj_iff_cycleType_eq, isConj_comm (g := g)]

Result:
no goals