internlm/Lean-Github huggingface dataset:
Theorem: OnCycleFactors.AlternatingGroup.card_of_cycleType_mul_eq
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : (Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m)
⊢ (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    Nat.factorial (Fintype.card α)

case pos.hc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : (Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m)
⊢ Even (Multiset.sum m + Multiset.card m)
Tactic:
have := Equiv.Perm.card_of_cycleType_mul_eq α m
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : (Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m)
this :
  (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) * Multiset.prod m *
        Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m))) =
    if Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then Nat.factorial (Fintype.card α) else 0
⊢ (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    Nat.factorial (Fintype.card α)

case pos.hc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : (Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m)
⊢ Even (Multiset.sum m + Multiset.card m)
Theorem: OnCycleFactors.AlternatingGroup.card_of_cycleType_mul_eq
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : (Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m)
this :
  (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) * Multiset.prod m *
        Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m))) =
    if Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then Nat.factorial (Fintype.card α) else 0
⊢ (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    Nat.factorial (Fintype.card α)

case pos.hc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : (Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m)
⊢ Even (Multiset.sum m + Multiset.card m)
Tactic:
simp only [mul_assoc] at this
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : (Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m)
this :
  (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    if Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then Nat.factorial (Fintype.card α) else 0
⊢ (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    Nat.factorial (Fintype.card α)

case pos.hc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : (Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m)
⊢ Even (Multiset.sum m + Multiset.card m)
Theorem: OnCycleFactors.AlternatingGroup.card_of_cycleType_mul_eq
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : (Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m)
this :
  (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    if Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then Nat.factorial (Fintype.card α) else 0
⊢ (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    Nat.factorial (Fintype.card α)

case pos.hc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : (Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m)
⊢ Even (Multiset.sum m + Multiset.card m)
Tactic:
rw [this]
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : (Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m)
this :
  (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    if Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then Nat.factorial (Fintype.card α) else 0
⊢ (if Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then Nat.factorial (Fintype.card α) else 0) =
    Nat.factorial (Fintype.card α)

case pos.hc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : (Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m)
⊢ Even (Multiset.sum m + Multiset.card m)
Theorem: OnCycleFactors.AlternatingGroup.card_of_cycleType_mul_eq
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : (Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m)
this :
  (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    if Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then Nat.factorial (Fintype.card α) else 0
⊢ (if Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then Nat.factorial (Fintype.card α) else 0) =
    Nat.factorial (Fintype.card α)

case pos.hc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : (Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m)
⊢ Even (Multiset.sum m + Multiset.card m)
Tactic:
rw [if_pos]
Proof state after:
case pos.hc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : (Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m)
this :
  (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    if Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then Nat.factorial (Fintype.card α) else 0
⊢ Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a

case pos.hc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : (Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m)
⊢ Even (Multiset.sum m + Multiset.card m)
Theorem: OnCycleFactors.AlternatingGroup.card_of_cycleType_mul_eq
Proof state before:
case pos.hc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : (Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m)
this :
  (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    if Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then Nat.factorial (Fintype.card α) else 0
⊢ Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a

case pos.hc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : (Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m)
⊢ Even (Multiset.sum m + Multiset.card m)
Tactic:
exact hm.1
Proof state after:
case pos.hc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : (Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m)
⊢ Even (Multiset.sum m + Multiset.card m)
Theorem: OnCycleFactors.AlternatingGroup.card_of_cycleType_mul_eq
Proof state before:
case pos.hc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : (Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m)
⊢ Even (Multiset.sum m + Multiset.card m)
Tactic:
exact hm.2
Proof state after:
no goals
Theorem: OnCycleFactors.AlternatingGroup.card_of_cycleType_mul_eq
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬((Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m))
⊢ (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    0
Tactic:
rw [← Finset.card_map]
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬((Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m))
⊢ (Finset.map ?neg✝ (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ)).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    0

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬((Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m))
⊢ ↥(alternatingGroup α) ↪ ?m.477900

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬((Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m))
⊢ Type ?u.477898
Theorem: OnCycleFactors.AlternatingGroup.card_of_cycleType_mul_eq
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬((Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m))
⊢ (Finset.map ?neg✝ (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ)).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    0

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬((Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m))
⊢ ↥(alternatingGroup α) ↪ ?m.477900

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬((Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m))
⊢ Type ?u.477898
Tactic:
rw [AlternatingGroup.of_cycleType_eq]
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬((Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m))
⊢ (if Even (Multiset.sum m + Multiset.card m) then Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ
        else ∅).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    0
Theorem: OnCycleFactors.AlternatingGroup.card_of_cycleType_mul_eq
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬((Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m))
⊢ (if Even (Multiset.sum m + Multiset.card m) then Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ
        else ∅).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    0
Tactic:
rw [apply_ite Finset.card]
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬((Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m))
⊢ (if Even (Multiset.sum m + Multiset.card m) then
        (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card
      else ∅.card) *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    0
Theorem: OnCycleFactors.AlternatingGroup.card_of_cycleType_mul_eq
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬((Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m))
⊢ (if Even (Multiset.sum m + Multiset.card m) then
        (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card
      else ∅.card) *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    0
Tactic:
rw [Finset.card_empty]
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬((Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m))
⊢ (if Even (Multiset.sum m + Multiset.card m) then
        (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card
      else 0) *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    0
Theorem: OnCycleFactors.AlternatingGroup.card_of_cycleType_mul_eq
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬((Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m))
⊢ (if Even (Multiset.sum m + Multiset.card m) then
        (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card
      else 0) *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    0
Tactic:
rw [not_and_or] at hm
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∨ ¬Even (Multiset.sum m + Multiset.card m)
⊢ (if Even (Multiset.sum m + Multiset.card m) then
        (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card
      else 0) *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    0
Theorem: OnCycleFactors.AlternatingGroup.card_of_cycleType_mul_eq
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∨ ¬Even (Multiset.sum m + Multiset.card m)
⊢ (if Even (Multiset.sum m + Multiset.card m) then
        (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card
      else 0) *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    0
Tactic:
by_cases hm' : Even (m.sum + Multiset.card m)
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∨ ¬Even (Multiset.sum m + Multiset.card m)
hm' : Even (Multiset.sum m + Multiset.card m)
⊢ (if Even (Multiset.sum m + Multiset.card m) then
        (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card
      else 0) *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    0

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∨ ¬Even (Multiset.sum m + Multiset.card m)
hm' : ¬Even (Multiset.sum m + Multiset.card m)
⊢ (if Even (Multiset.sum m + Multiset.card m) then
        (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card
      else 0) *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    0
Theorem: OnCycleFactors.AlternatingGroup.card_of_cycleType_mul_eq
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∨ ¬Even (Multiset.sum m + Multiset.card m)
hm' : Even (Multiset.sum m + Multiset.card m)
⊢ (if Even (Multiset.sum m + Multiset.card m) then
        (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card
      else 0) *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    0

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∨ ¬Even (Multiset.sum m + Multiset.card m)
hm' : ¬Even (Multiset.sum m + Multiset.card m)
⊢ (if Even (Multiset.sum m + Multiset.card m) then
        (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card
      else 0) *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    0
Tactic:
rw [if_pos]
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∨ ¬Even (Multiset.sum m + Multiset.card m)
hm' : Even (Multiset.sum m + Multiset.card m)
⊢ (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    0

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

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∨ ¬Even (Multiset.sum m + Multiset.card m)
hm' : ¬Even (Multiset.sum m + Multiset.card m)
⊢ (if Even (Multiset.sum m + Multiset.card m) then
        (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card
      else 0) *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    0