internlm/Lean-Github huggingface dataset:
Theorem: OnCycleFactors.Equiv.Perm.card_of_cycleType_mul_eq
Proof state before:
case pos.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
hg : g ∈ Equiv.permWithCycleType α m
h : Equiv.Perm α
⊢ Equiv.Perm.cycleType h = m ↔ Equiv.Perm.cycleType h = Equiv.Perm.cycleType g
Tactic:
simp only [Equiv.permWithCycleType, Finset.mem_filter] at hg
Proof state after:
case pos.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g h : Equiv.Perm α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ Equiv.Perm.cycleType h = m ↔ Equiv.Perm.cycleType h = Equiv.Perm.cycleType g
Theorem: OnCycleFactors.Equiv.Perm.card_of_cycleType_mul_eq
Proof state before:
case pos.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g h : Equiv.Perm α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ Equiv.Perm.cycleType h = m ↔ Equiv.Perm.cycleType h = Equiv.Perm.cycleType g
Tactic:
rw [hg.2]
Proof state after:
no goals
Theorem: OnCycleFactors.Equiv.Perm.card_of_cycleType_mul_eq
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
hg : g ∈ Equiv.permWithCycleType α m
this : Finset.filter (fun h => Equiv.Perm.cycleType h = m) Finset.univ = Finset.filter (fun h => IsConj g h) Finset.univ
⊢ (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 α)
Tactic:
rw [this, ← Equiv.Perm.conj_class_card_mul_eq g]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
hg : g ∈ Equiv.permWithCycleType α m
this : Finset.filter (fun h => Equiv.Perm.cycleType h = m) Finset.univ = Finset.filter (fun h => IsConj g h) Finset.univ
⊢ (Finset.filter (fun h => IsConj g h) 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))) =
    Fintype.card ↑{h | IsConj g h} * Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) *
        Multiset.prod (Equiv.Perm.cycleType g) *
      Multiset.prod
        (Multiset.map (fun n => Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g)))
          (Multiset.dedup (Equiv.Perm.cycleType g)))
Theorem: OnCycleFactors.Equiv.Perm.card_of_cycleType_mul_eq
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
hg : g ∈ Equiv.permWithCycleType α m
this : Finset.filter (fun h => Equiv.Perm.cycleType h = m) Finset.univ = Finset.filter (fun h => IsConj g h) Finset.univ
⊢ (Finset.filter (fun h => IsConj g h) 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))) =
    Fintype.card ↑{h | IsConj g h} * Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) *
        Multiset.prod (Equiv.Perm.cycleType g) *
      Multiset.prod
        (Multiset.map (fun n => Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g)))
          (Multiset.dedup (Equiv.Perm.cycleType g)))
Tactic:
simp only [Fintype.card_coe, ← Set.toFinset_card, mul_assoc]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
hg : g ∈ Equiv.permWithCycleType α m
this : Finset.filter (fun h => Equiv.Perm.cycleType h = m) Finset.univ = Finset.filter (fun h => IsConj g h) Finset.univ
⊢ (Finset.filter (fun h => IsConj g h) 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)))) =
    (Set.toFinset {h | IsConj g h}).card *
      (Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) *
        (Multiset.prod (Equiv.Perm.cycleType g) *
          Multiset.prod
            (Multiset.map (fun n => Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g)))
              (Multiset.dedup (Equiv.Perm.cycleType g)))))
Theorem: OnCycleFactors.Equiv.Perm.card_of_cycleType_mul_eq
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
hg : g ∈ Equiv.permWithCycleType α m
this : Finset.filter (fun h => Equiv.Perm.cycleType h = m) Finset.univ = Finset.filter (fun h => IsConj g h) Finset.univ
⊢ (Finset.filter (fun h => IsConj g h) 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)))) =
    (Set.toFinset {h | IsConj g h}).card *
      (Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) *
        (Multiset.prod (Equiv.Perm.cycleType g) *
          Multiset.prod
            (Multiset.map (fun n => Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g)))
              (Multiset.dedup (Equiv.Perm.cycleType g)))))
Tactic:
simp only [Equiv.permWithCycleType, Finset.mem_filter] at hg
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
this : Finset.filter (fun h => Equiv.Perm.cycleType h = m) Finset.univ = Finset.filter (fun h => IsConj g h) Finset.univ
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ (Finset.filter (fun h => IsConj g h) 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)))) =
    (Set.toFinset {h | IsConj g h}).card *
      (Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) *
        (Multiset.prod (Equiv.Perm.cycleType g) *
          Multiset.prod
            (Multiset.map (fun n => Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g)))
              (Multiset.dedup (Equiv.Perm.cycleType g)))))
Theorem: OnCycleFactors.Equiv.Perm.card_of_cycleType_mul_eq
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
this : Finset.filter (fun h => Equiv.Perm.cycleType h = m) Finset.univ = Finset.filter (fun h => IsConj g h) Finset.univ
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ (Finset.filter (fun h => IsConj g h) 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)))) =
    (Set.toFinset {h | IsConj g h}).card *
      (Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) *
        (Multiset.prod (Equiv.Perm.cycleType g) *
          Multiset.prod
            (Multiset.map (fun n => Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g)))
              (Multiset.dedup (Equiv.Perm.cycleType g)))))
Tactic:
rw [hg.2]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
this : Finset.filter (fun h => Equiv.Perm.cycleType h = m) Finset.univ = Finset.filter (fun h => IsConj g h) Finset.univ
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ (Finset.filter (fun h => IsConj g h) 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)))) =
    (Set.toFinset {h | IsConj g h}).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.Equiv.Perm.card_of_cycleType_mul_eq
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
this : Finset.filter (fun h => Equiv.Perm.cycleType h = m) Finset.univ = Finset.filter (fun h => IsConj g h) Finset.univ
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ (Finset.filter (fun h => IsConj g h) 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)))) =
    (Set.toFinset {h | IsConj g h}).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:
apply congr_arg₂ _ _ rfl
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
this : Finset.filter (fun h => Equiv.Perm.cycleType h = m) Finset.univ = Finset.filter (fun h => IsConj g h) Finset.univ
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ (Finset.filter (fun h => IsConj g h) Finset.univ).card = (Set.toFinset {h | IsConj g h}).card
Theorem: OnCycleFactors.Equiv.Perm.card_of_cycleType_mul_eq
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
this : Finset.filter (fun h => Equiv.Perm.cycleType h = m) Finset.univ = Finset.filter (fun h => IsConj g h) Finset.univ
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ (Finset.filter (fun h => IsConj g h) Finset.univ).card = (Set.toFinset {h | IsConj g h}).card
Tactic:
apply congr_arg
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
this : Finset.filter (fun h => Equiv.Perm.cycleType h = m) Finset.univ = Finset.filter (fun h => IsConj g h) Finset.univ
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ Finset.filter (fun h => IsConj g h) Finset.univ = Set.toFinset {h | IsConj g h}
Theorem: OnCycleFactors.Equiv.Perm.card_of_cycleType_mul_eq
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
this : Finset.filter (fun h => Equiv.Perm.cycleType h = m) Finset.univ = Finset.filter (fun h => IsConj g h) Finset.univ
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ Finset.filter (fun h => IsConj g h) Finset.univ = Set.toFinset {h | IsConj g h}
Tactic:
ext σ
Proof state after:
case h.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
this : Finset.filter (fun h => Equiv.Perm.cycleType h = m) Finset.univ = Finset.filter (fun h => IsConj g h) Finset.univ
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
σ : Equiv.Perm α
⊢ σ ∈ Finset.filter (fun h => IsConj g h) Finset.univ ↔ σ ∈ Set.toFinset {h | IsConj g h}
Theorem: OnCycleFactors.Equiv.Perm.card_of_cycleType_mul_eq
Proof state before:
case h.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
this : Finset.filter (fun h => Equiv.Perm.cycleType h = m) Finset.univ = Finset.filter (fun h => IsConj g h) Finset.univ
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
σ : Equiv.Perm α
⊢ σ ∈ Finset.filter (fun h => IsConj g h) Finset.univ ↔ σ ∈ Set.toFinset {h | IsConj g h}
Tactic:
simp only [isConj_iff, Finset.mem_univ, forall_true_left, Finset.univ_filter_exists,
  Finset.mem_image, true_and, Set.toFinset_setOf]
Proof state after:
no goals
Theorem: OnCycleFactors.Equiv.Perm.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)
⊢ (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:
convert MulZeroClass.zero_mul _
Proof state after:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card = 0
Theorem: OnCycleFactors.Equiv.Perm.card_of_cycleType_mul_eq
Proof state before:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card = 0
Tactic:
rw [Finset.card_eq_zero]
Proof state after:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ = ∅
Theorem: OnCycleFactors.Equiv.Perm.card_of_cycleType_mul_eq
Proof state before:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ = ∅
Tactic:
rw [← Finset.isEmpty_coe_sort]
Proof state after:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ IsEmpty { x // x ∈ Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ }
Theorem: OnCycleFactors.Equiv.Perm.card_of_cycleType_mul_eq
Proof state before:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ IsEmpty { x // x ∈ Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ }
Tactic:
rw [← not_nonempty_iff]
Proof state after:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ ¬Nonempty { x // x ∈ Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ }
Theorem: OnCycleFactors.Equiv.Perm.card_of_cycleType_mul_eq
Proof state before:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ ¬Nonempty { x // x ∈ Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ }
Tactic:
intro h
Proof state after:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
h : Nonempty { x // x ∈ Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ }
⊢ False
Theorem: OnCycleFactors.Equiv.Perm.card_of_cycleType_mul_eq
Proof state before:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
h : Nonempty { x // x ∈ Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ }
⊢ False
Tactic:
apply hm
Proof state after:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
h : Nonempty { x // x ∈ Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ }
⊢ Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
Theorem: OnCycleFactors.Equiv.Perm.card_of_cycleType_mul_eq
Proof state before:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
h : Nonempty { x // x ∈ Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ }
⊢ Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
Tactic:
simp only [Finset.nonempty_coe_sort] at h
Proof state after:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
h : (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).Nonempty
⊢ Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
Theorem: OnCycleFactors.Equiv.Perm.card_of_cycleType_mul_eq
Proof state before:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
h : (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).Nonempty
⊢ Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
Tactic:
rw [← Equiv.permWithCycleType_nonempty_iff]
Proof state after:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
h : (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).Nonempty
⊢ (Equiv.permWithCycleType α m).Nonempty
Theorem: OnCycleFactors.Equiv.Perm.card_of_cycleType_mul_eq
Proof state before:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
h : (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).Nonempty
⊢ (Equiv.permWithCycleType α m).Nonempty
Tactic:
exact h
Proof state after:
no goals
Theorem: OnCycleFactors.Equiv.Perm.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 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
⊢ (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)
⊢ (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card = 0
Theorem: OnCycleFactors.Equiv.Perm.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
⊢ (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:
obtain ⟨g, hg⟩ := Equiv.permWithCycleType_nonempty_iff.mpr hm
Proof state after:
case pos.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
hg : g ∈ Equiv.permWithCycleType α 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)))
Theorem: OnCycleFactors.Equiv.Perm.card_of_cycleType
Proof state before:
case pos.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
hg : g ∈ Equiv.permWithCycleType α 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:
simp only [Equiv.permWithCycleType, Finset.mem_filter] at hg
Proof state after:
case pos.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = 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)))
Theorem: OnCycleFactors.Equiv.Perm.card_of_cycleType
Proof state before:
case pos.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = 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 [← Equiv.Perm.conj_class_card_mul_eq g]
Proof state after:
case pos.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card =
    Fintype.card ↑{h | IsConj g h} * Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) *
          Multiset.prod (Equiv.Perm.cycleType g) *
        Multiset.prod
          (Multiset.map (fun n => Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g)))
            (Multiset.dedup (Equiv.Perm.cycleType g))) /
      (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)))