internlm/Lean-Github huggingface dataset:
Theorem: OnCycleFactors.Group.conj_class_eq_conj_orbit
Proof state before:
case h.mp.intro
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k c : G
hc : c * g * c⁻¹ = k
⊢ ∃ x, ConjAct.ofConjAct x * g * (ConjAct.ofConjAct x)⁻¹ = k

case h.mpr
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k : G
⊢ (∃ x, ConjAct.ofConjAct x * g * (ConjAct.ofConjAct x)⁻¹ = k) → ∃ c, c * g * c⁻¹ = k
Tactic:
use ConjAct.toConjAct c
Proof state after:
case h
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k c : G
hc : c * g * c⁻¹ = k
⊢ ConjAct.ofConjAct (ConjAct.toConjAct c) * g * (ConjAct.ofConjAct (ConjAct.toConjAct c))⁻¹ = k

case h.mpr
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k : G
⊢ (∃ x, ConjAct.ofConjAct x * g * (ConjAct.ofConjAct x)⁻¹ = k) → ∃ c, c * g * c⁻¹ = k
Theorem: OnCycleFactors.Group.conj_class_eq_conj_orbit
Proof state before:
case h
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k c : G
hc : c * g * c⁻¹ = k
⊢ ConjAct.ofConjAct (ConjAct.toConjAct c) * g * (ConjAct.ofConjAct (ConjAct.toConjAct c))⁻¹ = k

case h.mpr
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k : G
⊢ (∃ x, ConjAct.ofConjAct x * g * (ConjAct.ofConjAct x)⁻¹ = k) → ∃ c, c * g * c⁻¹ = k
Tactic:
simp only [hc, ConjAct.ofConjAct_toConjAct]
Proof state after:
case h.mpr
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k : G
⊢ (∃ x, ConjAct.ofConjAct x * g * (ConjAct.ofConjAct x)⁻¹ = k) → ∃ c, c * g * c⁻¹ = k
Theorem: OnCycleFactors.Group.conj_class_eq_conj_orbit
Proof state before:
case h.mpr
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k : G
⊢ (∃ x, ConjAct.ofConjAct x * g * (ConjAct.ofConjAct x)⁻¹ = k) → ∃ c, c * g * c⁻¹ = k
Tactic:
rintro ⟨x, hx⟩
Proof state after:
case h.mpr.intro
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k : G
x : ConjAct G
hx : ConjAct.ofConjAct x * g * (ConjAct.ofConjAct x)⁻¹ = k
⊢ ∃ c, c * g * c⁻¹ = k
Theorem: OnCycleFactors.Group.conj_class_eq_conj_orbit
Proof state before:
case h.mpr.intro
α : Type ?u.424342
inst✝² : DecidableEq α
inst✝¹ : Fintype α
g✝ : Equiv.Perm α
G : Type u_1
inst✝ : Group G
g k : G
x : ConjAct G
hx : ConjAct.ofConjAct x * g * (ConjAct.ofConjAct x)⁻¹ = k
⊢ ∃ c, c * g * c⁻¹ = k
Tactic:
use ConjAct.ofConjAct x
Proof state after:
no goals
Theorem: OnCycleFactors.Equiv.Perm.conj_class_card_mul_eq
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ 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 α)
Tactic:
classical
simp_rw [Group.conj_class_eq_conj_orbit g]
simp only [mul_assoc]
rw [mul_comm]
simp only [← mul_assoc]
rw [← Equiv.Perm.conj_stabilizer_card g]
rw [mul_comm]
rw [MulAction.card_orbit_mul_card_stabilizer_eq_card_group (ConjAct (Equiv.Perm α)) g]
rw [ConjAct.card, Fintype.card_perm]
Proof state after:
no goals
Theorem: OnCycleFactors.Equiv.Perm.conj_class_card_mul_eq
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ 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 α)
Tactic:
simp_rw [Group.conj_class_eq_conj_orbit g]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↑(MulAction.orbit (ConjAct (Equiv.Perm α)) g) *
          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 α)
Theorem: OnCycleFactors.Equiv.Perm.conj_class_card_mul_eq
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↑(MulAction.orbit (ConjAct (Equiv.Perm α)) g) *
          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 α)
Tactic:
simp only [mul_assoc]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↑(MulAction.orbit (ConjAct (Equiv.Perm α)) g) *
      (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 α)
Theorem: OnCycleFactors.Equiv.Perm.conj_class_card_mul_eq
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↑(MulAction.orbit (ConjAct (Equiv.Perm α)) g) *
      (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 α)
Tactic:
rw [mul_comm]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ 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)))) *
      Fintype.card ↑(MulAction.orbit (ConjAct (Equiv.Perm α)) g) =
    Nat.factorial (Fintype.card α)
Theorem: OnCycleFactors.Equiv.Perm.conj_class_card_mul_eq
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ 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)))) *
      Fintype.card ↑(MulAction.orbit (ConjAct (Equiv.Perm α)) g) =
    Nat.factorial (Fintype.card α)
Tactic:
simp only [← mul_assoc]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ 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))) *
      Fintype.card ↑(MulAction.orbit (ConjAct (Equiv.Perm α)) g) =
    Nat.factorial (Fintype.card α)
Theorem: OnCycleFactors.Equiv.Perm.conj_class_card_mul_eq
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ 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))) *
      Fintype.card ↑(MulAction.orbit (ConjAct (Equiv.Perm α)) g) =
    Nat.factorial (Fintype.card α)
Tactic:
rw [← Equiv.Perm.conj_stabilizer_card g]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g) *
      Fintype.card ↑(MulAction.orbit (ConjAct (Equiv.Perm α)) g) =
    Nat.factorial (Fintype.card α)
Theorem: OnCycleFactors.Equiv.Perm.conj_class_card_mul_eq
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g) *
      Fintype.card ↑(MulAction.orbit (ConjAct (Equiv.Perm α)) g) =
    Nat.factorial (Fintype.card α)
Tactic:
rw [mul_comm]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↑(MulAction.orbit (ConjAct (Equiv.Perm α)) g) *
      Fintype.card ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g) =
    Nat.factorial (Fintype.card α)
Theorem: OnCycleFactors.Equiv.Perm.conj_class_card_mul_eq
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↑(MulAction.orbit (ConjAct (Equiv.Perm α)) g) *
      Fintype.card ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g) =
    Nat.factorial (Fintype.card α)
Tactic:
rw [MulAction.card_orbit_mul_card_stabilizer_eq_card_group (ConjAct (Equiv.Perm α)) g]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card (ConjAct (Equiv.Perm α)) = Nat.factorial (Fintype.card α)
Theorem: OnCycleFactors.Equiv.Perm.conj_class_card_mul_eq
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card (ConjAct (Equiv.Perm α)) = Nat.factorial (Fintype.card α)
Tactic:
rw [ConjAct.card, Fintype.card_perm]
Proof state after:
no goals
Theorem: OnCycleFactors.Multiset.prod_pos
Proof state before:
α : Type ?u.434129
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
R : Type u_1
inst✝¹ : StrictOrderedCommSemiring R
inst✝ : Nontrivial R
m : Multiset R
h : ∀ a ∈ m, 0 < a
⊢ 0 < Multiset.prod m
Tactic:
induction' m using Multiset.induction with a m ih
Proof state after:
case empty
α : Type ?u.434129
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
R : Type u_1
inst✝¹ : StrictOrderedCommSemiring R
inst✝ : Nontrivial R
h : ∀ a ∈ 0, 0 < a
⊢ 0 < Multiset.prod 0

case cons
α : Type ?u.434129
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
R : Type u_1
inst✝¹ : StrictOrderedCommSemiring R
inst✝ : Nontrivial R
a : R
m : Multiset R
ih : (∀ a ∈ m, 0 < a) → 0 < Multiset.prod m
h : ∀ a_1 ∈ a ::ₘ m, 0 < a_1
⊢ 0 < Multiset.prod (a ::ₘ m)
Theorem: OnCycleFactors.Multiset.prod_pos
Proof state before:
case empty
α : Type ?u.434129
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
R : Type u_1
inst✝¹ : StrictOrderedCommSemiring R
inst✝ : Nontrivial R
h : ∀ a ∈ 0, 0 < a
⊢ 0 < Multiset.prod 0
Tactic:
simp
Proof state after:
no goals
Theorem: OnCycleFactors.Multiset.prod_pos
Proof state before:
case cons
α : Type ?u.434129
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
R : Type u_1
inst✝¹ : StrictOrderedCommSemiring R
inst✝ : Nontrivial R
a : R
m : Multiset R
ih : (∀ a ∈ m, 0 < a) → 0 < Multiset.prod m
h : ∀ a_1 ∈ a ::ₘ m, 0 < a_1
⊢ 0 < Multiset.prod (a ::ₘ m)
Tactic:
rw [Multiset.prod_cons]
Proof state after:
case cons
α : Type ?u.434129
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
R : Type u_1
inst✝¹ : StrictOrderedCommSemiring R
inst✝ : Nontrivial R
a : R
m : Multiset R
ih : (∀ a ∈ m, 0 < a) → 0 < Multiset.prod m
h : ∀ a_1 ∈ a ::ₘ m, 0 < a_1
⊢ 0 < a * Multiset.prod m
Theorem: OnCycleFactors.Multiset.prod_pos
Proof state before:
case cons
α : Type ?u.434129
inst✝³ : DecidableEq α
inst✝² : Fintype α
g : Equiv.Perm α
R : Type u_1
inst✝¹ : StrictOrderedCommSemiring R
inst✝ : Nontrivial R
a : R
m : Multiset R
ih : (∀ a ∈ m, 0 < a) → 0 < Multiset.prod m
h : ∀ a_1 ∈ a ::ₘ m, 0 < a_1
⊢ 0 < a * Multiset.prod m
Tactic:
exact
  mul_pos (h _ <| Multiset.mem_cons_self _ _)
    (ih fun a ha => h a <| Multiset.mem_cons_of_mem ha)
Proof state after:
no goals
Theorem: OnCycleFactors.Equiv.Perm.conj_class_card
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↑{h | IsConj g h} =
    Nat.factorial (Fintype.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 [← Equiv.Perm.conj_class_card_mul_eq g]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↑{h | IsConj g h} =
    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 (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.conj_class_card
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↑{h | IsConj g h} =
    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 (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 [Nat.div_eq_of_eq_mul_left _]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ 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))) =
    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))))

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ 0 <
    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.conj_class_card
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ 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))) =
    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))))

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ 0 <
    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 [← mul_assoc]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ 0 <
    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.conj_class_card
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ 0 <
    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 [← Equiv.Perm.conj_stabilizer_card g]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ 0 < Fintype.card ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
Theorem: OnCycleFactors.Equiv.Perm.conj_class_card
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ 0 < Fintype.card ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)
Tactic:
refine' Fintype.card_pos
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 ℕ
⊢ (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) * Multiset.prod m *
        Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m))) =
    if Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then Nat.factorial (Fintype.card α) else 0
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 α - Multiset.sum m) * Multiset.prod m *
        Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m))) =
    Nat.factorial (Fintype.card α)

case 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
Theorem: OnCycleFactors.Equiv.Perm.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
⊢ (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:
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 α - 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 α)
Theorem: OnCycleFactors.Equiv.Perm.card_of_cycleType_mul_eq
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 h => Equiv.Perm.cycleType h = m) Finset.univ = Finset.filter (fun h => IsConj g h) Finset.univ
Tactic:
ext h
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 : Equiv.Perm α
hg : g ∈ Equiv.permWithCycleType α m
h : Equiv.Perm α
⊢ h ∈ Finset.filter (fun h => Equiv.Perm.cycleType h = m) Finset.univ ↔
    h ∈ Finset.filter (fun h => IsConj g h) Finset.univ
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 α
⊢ h ∈ Finset.filter (fun h => Equiv.Perm.cycleType h = m) Finset.univ ↔
    h ∈ Finset.filter (fun h => IsConj g h) Finset.univ
Tactic:
simp only [Finset.mem_filter, Finset.mem_univ, true_and_iff, Set.mem_toFinset, Set.mem_setOf_eq]
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 : Equiv.Perm α
hg : g ∈ Equiv.permWithCycleType α m
h : Equiv.Perm α
⊢ Equiv.Perm.cycleType h = m ↔ IsConj g h
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 ↔ IsConj g h
Tactic:
rw [isConj_comm]
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 : Equiv.Perm α
hg : g ∈ Equiv.permWithCycleType α m
h : Equiv.Perm α
⊢ Equiv.Perm.cycleType h = m ↔ IsConj h 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 : Equiv.Perm α
hg : g ∈ Equiv.permWithCycleType α m
h : Equiv.Perm α
⊢ Equiv.Perm.cycleType h = m ↔ IsConj h g
Tactic:
rw [Equiv.Perm.isConj_iff_cycleType_eq]
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 : Equiv.Perm α
hg : g ∈ Equiv.permWithCycleType α m
h : Equiv.Perm α
⊢ Equiv.Perm.cycleType h = m ↔ Equiv.Perm.cycleType h = Equiv.Perm.cycleType g