internlm/Lean-Github huggingface dataset:
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.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
Tactic:
rw [AlternatingGroup.of_cycleType_eq]
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)
⊢ (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 α) /
      (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))))
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)
⊢ (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 α) /
      (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 [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)
⊢ (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.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
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))))

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 [Equiv.Perm.card_of_cycleType α 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)
⊢ (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 α) /
      (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.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
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)
⊢ (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 α) /
      (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.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
α : 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)
⊢ 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))) =
    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.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)
⊢ 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
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)
⊢ 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))) =
    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.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)
⊢ 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:
simp only [mul_assoc]
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)
⊢ 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
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)
⊢ 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
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
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 = 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 = 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.482556

α : 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.482554
Theorem: OnCycleFactors.AlternatingGroup.card_of_cycleType
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 = 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.482556

α : 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.482554
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 =
    0
Theorem: OnCycleFactors.AlternatingGroup.card_of_cycleType
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 =
    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) =
    0
Theorem: OnCycleFactors.AlternatingGroup.card_of_cycleType
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) =
    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) =
    0
Theorem: OnCycleFactors.AlternatingGroup.card_of_cycleType
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) =
    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) =
    0
Theorem: OnCycleFactors.AlternatingGroup.card_of_cycleType
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) =
    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) =
    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) =
    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)
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) =
    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) =
    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 = 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) =
    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)
hm' : Even (Multiset.sum m + Multiset.card m)
⊢ (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card = 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) =
    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) =
    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) =
    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)
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) =
    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) =
    0
Tactic:
rw [if_neg]
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) =
    0