Theorem: OnCycleFactors.Equiv.Perm.conj_class_card_mul_eq (Jordan/ConjClassCount.lean)

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]
State after:
no goals

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]
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 α)

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]
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 α)

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]
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 α)

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]
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 α)

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]
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 α)

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]
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 α)

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]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card (ConjAct (Equiv.Perm α)) = Nat.factorial (Fintype.card α)

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]
State after:
no goals