internlm/Lean-Github huggingface dataset:
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 =
    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)))
Tactic:
simp only [mul_assoc]
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))))
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 =
    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))))
Tactic:
simp only [Fintype.card_coe, ← Set.toFinset_card, mul_assoc]
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 =
    (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))))) /
      (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 =
    (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))))) /
      (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 [Nat.div_eq_of_eq_mul_left _]
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
⊢ (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))))) =
    (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))))

α : 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
⊢ 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)))
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
⊢ (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))))) =
    (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))))

α : 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
⊢ 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)))
Tactic:
apply congr_arg₂
Proof state after:
case pos.intro.hx
α : 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
⊢ (Set.toFinset {h | IsConj g h}).card = (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card

case pos.intro.hy
α : 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
⊢ 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)))

α : 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
⊢ 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)))
Theorem: OnCycleFactors.Equiv.Perm.card_of_cycleType
Proof state before:
case pos.intro.hy
α : 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
⊢ 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)))

α : 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
⊢ 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)))
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 α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = 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)))
Theorem: OnCycleFactors.Equiv.Perm.card_of_cycleType
Proof state before:
case pos.intro.hx
α : 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
⊢ (Set.toFinset {h | IsConj g h}).card = (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card
Tactic:
apply congr_arg
Proof state after:
case pos.intro.hx.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 α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ Set.toFinset {h | IsConj g h} = Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ
Theorem: OnCycleFactors.Equiv.Perm.card_of_cycleType
Proof state before:
case pos.intro.hx.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 α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ Set.toFinset {h | IsConj g h} = Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ
Tactic:
ext h
Proof state after:
case pos.intro.hx.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 α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
h : Equiv.Perm α
⊢ h ∈ Set.toFinset {h | IsConj g h} ↔ h ∈ Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ
Theorem: OnCycleFactors.Equiv.Perm.card_of_cycleType
Proof state before:
case pos.intro.hx.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 α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
h : Equiv.Perm α
⊢ h ∈ Set.toFinset {h | IsConj g h} ↔ h ∈ Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ
Tactic:
simp only [Set.toFinset_setOf, Finset.mem_univ, forall_true_left,
  Finset.univ_filter_exists, Finset.mem_image, true_and, Finset.mem_filter]
Proof state after:
case pos.intro.hx.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 α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
h : Equiv.Perm α
⊢ IsConj g h ↔ Equiv.Perm.cycleType h = m
Theorem: OnCycleFactors.Equiv.Perm.card_of_cycleType
Proof state before:
case pos.intro.hx.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 α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
h : Equiv.Perm α
⊢ IsConj g h ↔ Equiv.Perm.cycleType h = m
Tactic:
rw [isConj_comm, Equiv.Perm.isConj_iff_cycleType_eq, hg.2]
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 ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = 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)))
Tactic:
apply Nat.mul_pos
Proof state after:
case ha
α : 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
⊢ Nat.factorial (Fintype.card α - Multiset.sum m) > 0

case hb
α : 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
⊢ Multiset.prod m * Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)) > 0
Theorem: OnCycleFactors.Equiv.Perm.card_of_cycleType
Proof state before:
case ha
α : 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
⊢ Nat.factorial (Fintype.card α - Multiset.sum m) > 0

case hb
α : 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
⊢ Multiset.prod m * Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)) > 0
Tactic:
exact Nat.factorial_pos (Fintype.card α - Multiset.sum m)
Proof state after:
case hb
α : 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
⊢ Multiset.prod m * Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)) > 0
Theorem: OnCycleFactors.Equiv.Perm.card_of_cycleType
Proof state before:
case hb
α : 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
⊢ Multiset.prod m * Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)) > 0
Tactic:
apply Nat.mul_pos
Proof state after:
case hb.ha
α : 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
⊢ Multiset.prod m > 0

case hb.hb
α : 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
⊢ Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)) > 0
Theorem: OnCycleFactors.Equiv.Perm.card_of_cycleType
Proof state before:
case hb.ha
α : 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
⊢ Multiset.prod m > 0
Tactic:
apply Multiset.prod_pos
Proof state after:
case hb.ha.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 α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ ∀ a ∈ m, 0 < a
Theorem: OnCycleFactors.Equiv.Perm.card_of_cycleType
Proof state before:
case hb.ha.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 α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ ∀ a ∈ m, 0 < a
Tactic:
intro a ha
Proof state after:
case hb.ha.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 α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
a : ℕ
ha : a ∈ m
⊢ 0 < a
Theorem: OnCycleFactors.Equiv.Perm.card_of_cycleType
Proof state before:
case hb.ha.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 α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
a : ℕ
ha : a ∈ m
⊢ 0 < a
Tactic:
exact lt_of_lt_of_le (by norm_num) (hm.2 a ha)
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 ℕ
hm : Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
g : Equiv.Perm α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
a : ℕ
ha : a ∈ m
⊢ 0 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: OnCycleFactors.Equiv.Perm.card_of_cycleType
Proof state before:
case hb.hb
α : 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
⊢ Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)) > 0
Tactic:
apply Multiset.prod_pos
Proof state after:
case hb.hb.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 α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ ∀ a ∈ Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m), 0 < a
Theorem: OnCycleFactors.Equiv.Perm.card_of_cycleType
Proof state before:
case hb.hb.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 α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
⊢ ∀ a ∈ Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m), 0 < a
Tactic:
intro a
Proof state after:
case hb.hb.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 α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
a : ℕ
⊢ a ∈ Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m) → 0 < a
Theorem: OnCycleFactors.Equiv.Perm.card_of_cycleType
Proof state before:
case hb.hb.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 α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
a : ℕ
⊢ a ∈ Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m) → 0 < a
Tactic:
rw [Multiset.mem_map]
Proof state after:
case hb.hb.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 α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
a : ℕ
⊢ (∃ a_1 ∈ Multiset.dedup m, Nat.factorial (Multiset.count a_1 m) = a) → 0 < a
Theorem: OnCycleFactors.Equiv.Perm.card_of_cycleType
Proof state before:
case hb.hb.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 α
hg : g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
a : ℕ
⊢ (∃ a_1 ∈ Multiset.dedup m, Nat.factorial (Multiset.count a_1 m) = a) → 0 < a
Tactic:
rintro ⟨b, _, rfl⟩
Proof state after:
case hb.hb.h.intro.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
b : ℕ
left✝ : b ∈ Multiset.dedup m
⊢ 0 < Nat.factorial (Multiset.count b m)
Theorem: OnCycleFactors.Equiv.Perm.card_of_cycleType
Proof state before:
case hb.hb.h.intro.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
b : ℕ
left✝ : b ∈ Multiset.dedup m
⊢ 0 < Nat.factorial (Multiset.count b m)
Tactic:
apply Nat.factorial_pos
Proof state after:
no goals
Theorem: OnCycleFactors.Equiv.Perm.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)
⊢ (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card = 0
Tactic:
rw [Finset.card_eq_zero, ← Finset.not_nonempty_iff_eq_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)
⊢ ¬(Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).Nonempty
Theorem: OnCycleFactors.Equiv.Perm.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)
⊢ ¬(Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).Nonempty
Tactic:
rw [← Equiv.permWithCycleType_nonempty_iff] at hm
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Equiv.permWithCycleType α m).Nonempty
⊢ ¬(Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).Nonempty
Theorem: OnCycleFactors.Equiv.Perm.card_of_cycleType
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬(Equiv.permWithCycleType α m).Nonempty
⊢ ¬(Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).Nonempty
Tactic:
exact hm
Proof state after:
no goals
Theorem: OnCycleFactors.AlternatingGroup.of_cycleType_eq
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
⊢ Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
      (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ) =
    if Even (Multiset.sum m + Multiset.card m) then Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ
    else ∅
Tactic:
split_ifs with hm
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
⊢ Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
      (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ) =
    Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬Even (Multiset.sum m + Multiset.card m)
⊢ Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
      (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ) =
    ∅