-- Mathlib/GroupTheory/SpecificGroups/Alternating/Centralizer.lean
theorem card_of_cycleType (m : Multiset ℕ) :
    (Finset.univ.filter fun g : alternatingGroup α => (g : Equiv.Perm α).cycleType = m).card =
      if (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + Multiset.card m) then
        (Fintype.card α)! /
          ((Fintype.card α - m.sum)! *
            (m.prod * (∏ n ∈ m.toFinset, (m.count n)!)))
      else 0

Proof state:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬((m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card))
⊢ #(filter (fun g => (↑g).cycleType = m) univ) = 0

Tactic:
rw [← Finset.card_map, map_subtype_of_cycleType]

Result:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬((m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card))
⊢ #(if Even (m.sum + m.card) then filter (fun g => g.cycleType = m) univ else ∅) = 0

Proof state:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬((m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card))
⊢ (if Even (m.sum + m.card) then #(filter (fun g => g.cycleType = m) univ) else 0) = 0

Tactic:
split_ifs with hm'

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

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬((m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card))
hm' : ¬Even (m.sum + m.card)
⊢ 0 = 0

Proof state:
case pos.hnc.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm✝ : ¬((m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card))
hm' : Even (m.sum + m.card)
hm : ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)

Tactic:
exact hm

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬((m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card))
hm' : ¬Even (m.sum + m.card)
⊢ 0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card)
⊢ (if m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then
      (Fintype.card α)! / ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
    else 0) =
    (Fintype.card α)! / ((Fintype.card α - m.sum)! * (m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!))

Tactic:
rw [if_pos hm.1, mul_assoc]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬((m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card))
⊢ #(if Even (m.sum + m.card) then filter (fun g => g.cycleType = m) univ else ∅) = 0

Tactic:
rw [apply_ite Finset.card, Finset.card_empty]

Result:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬((m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card))
⊢ (if Even (m.sum + m.card) then #(filter (fun g => g.cycleType = m) univ) else 0) = 0

Proof state:
case pos.hnc
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬((m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card))
hm' : Even (m.sum + m.card)
⊢ ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)

Tactic:
cases' not_and_or.mp hm with hm hm

Result:
case pos.hnc.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm✝ : ¬((m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card))
hm' : Even (m.sum + m.card)
hm : ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)

case pos.hnc.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm✝ : ¬((m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card))
hm' : Even (m.sum + m.card)
hm : ¬Even (m.sum + m.card)
⊢ ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)

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

Tactic:
rw [← Finset.card_map, map_subtype_of_cycleType, if_pos hm.2,
Equiv.Perm.card_of_cycleType α m]

Result:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card)
⊢ (if m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then
      (Fintype.card α)! / ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
    else 0) =
    (Fintype.card α)! / ((Fintype.card α - m.sum)! * (m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!))

Proof state:
case pos.hnc.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm✝ : ¬((m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card))
hm' : Even (m.sum + m.card)
hm : ¬Even (m.sum + m.card)
⊢ ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)

Tactic:
contradiction

Result:
no goals

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

Tactic:
split_ifs with hm

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

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬((m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card))
⊢ #(filter (fun g => (↑g).cycleType = m) univ) = 0

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

Tactic:
rw [Equiv.Perm.card_of_cycleType, if_neg]

Result:
case pos.hnc
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
m : Multiset ℕ
hm : ¬((m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card))
hm' : Even (m.sum + m.card)
⊢ ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)