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)
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
Tactic:
rw [Equiv.Perm.card_of_cycleType]
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 Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then
        Nat.factorial (Fintype.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)))
      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 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
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)
⊢ 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 pos.hnc
α : 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)
⊢ ¬(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)
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
Tactic:
exact MulZeroClass.zero_mul _
Proof state after:
case pos.hnc
α : 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)
⊢ ¬(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)
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
Theorem: OnCycleFactors.AlternatingGroup.card_of_cycleType_mul_eq
Proof state before:
case pos.hnc
α : 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)
⊢ ¬(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)
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
Tactic:
cases' hm with hm hm
Proof state after:
case pos.hnc.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm' : Even (Multiset.sum m + Multiset.card m)
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)

case pos.hnc.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm' : Even (Multiset.sum m + Multiset.card m)
hm : ¬Even (Multiset.sum m + Multiset.card m)
⊢ ¬(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)
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
Theorem: OnCycleFactors.AlternatingGroup.card_of_cycleType_mul_eq
Proof state before:
case pos.hnc.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm' : Even (Multiset.sum m + Multiset.card m)
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)

case pos.hnc.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm' : Even (Multiset.sum m + Multiset.card m)
hm : ¬Even (Multiset.sum m + Multiset.card m)
⊢ ¬(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)
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
Tactic:
exact hm
Proof state after:
case pos.hnc.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm' : Even (Multiset.sum m + Multiset.card m)
hm : ¬Even (Multiset.sum m + Multiset.card m)
⊢ ¬(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)
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
Theorem: OnCycleFactors.AlternatingGroup.card_of_cycleType_mul_eq
Proof state before:
case pos.hnc.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm' : Even (Multiset.sum m + Multiset.card m)
hm : ¬Even (Multiset.sum m + Multiset.card m)
⊢ ¬(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)
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
Tactic:
exfalso
Proof state after:
case pos.hnc.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm' : Even (Multiset.sum m + Multiset.card m)
hm : ¬Even (Multiset.sum m + Multiset.card m)
⊢ False

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
Theorem: OnCycleFactors.AlternatingGroup.card_of_cycleType_mul_eq
Proof state before:
case pos.hnc.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm' : Even (Multiset.sum m + Multiset.card m)
hm : ¬Even (Multiset.sum m + Multiset.card m)
⊢ False

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
Tactic:
exact hm hm'
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)
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
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)
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
Tactic:
exact 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)
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 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_neg]
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)
hm' : ¬Even (Multiset.sum m + Multiset.card m)
⊢ 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.hnc
α : 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)
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)
hm' : ¬Even (Multiset.sum m + Multiset.card m)
⊢ 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.hnc
α : 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)
Tactic:
exact MulZeroClass.zero_mul _
Proof state after:
case neg.hnc
α : 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)
Theorem: OnCycleFactors.AlternatingGroup.card_of_cycleType_mul_eq
Proof state before:
case neg.hnc
α : 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)
Tactic:
exact hm'
Proof state after:
no goals
Theorem: OnCycleFactors.AlternatingGroup.card_of_cycleType
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
⊢ (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ).card =
    if (Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m) then
      Nat.factorial (Fintype.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))))
    else 0
Tactic:
split_ifs with hm
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)
⊢ (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ).card =
    Nat.factorial (Fintype.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))))

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 = 0
Theorem: OnCycleFactors.AlternatingGroup.card_of_cycleType
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 α) /
      (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))))
Tactic:
rw [← Finset.card_map]
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)
⊢ (Finset.map ?pos✝ (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ)).card =
    Nat.factorial (Fintype.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))))

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)
⊢ ↥(alternatingGroup α) ↪ ?m.482132

α : 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.482130