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

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↥(MulAction.stabilizer (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)))
Tactic:
rw [Subgroup.card_eq_card_quotient_mul_card_subgroup (φ g).ker]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card (↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g) ⧸ MonoidHom.ker (φ g)) *
      Fintype.card ↥(MonoidHom.ker (φ 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)))

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card (↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g) ⧸ MonoidHom.ker (φ g)) *
      Fintype.card ↥(MonoidHom.ker (φ 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 [Fintype.card_congr (QuotientGroup.quotientKerEquivRange (φ g)).toEquiv]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↥(MonoidHom.range (φ g)) * Fintype.card ↥(MonoidHom.ker (φ 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)))

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↥(MonoidHom.range (φ g)) * Fintype.card ↥(MonoidHom.ker (φ 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.card_eq_fintype_card, hφ_range_card]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Multiset.prod
        (Multiset.map (fun n => Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g)))
          (Multiset.dedup (Equiv.Perm.cycleType g))) *
      Fintype.card ↥(MonoidHom.ker (φ 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)))

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Multiset.prod
        (Multiset.map (fun n => Nat.factorial (Multiset.count n (Equiv.Perm.cycleType g)))
          (Multiset.dedup (Equiv.Perm.cycleType g))) *
      Fintype.card ↥(MonoidHom.ker (φ 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 [mul_comm]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↥(MonoidHom.ker (φ 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)))

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↥(MonoidHom.ker (φ g)) =
    Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) * Multiset.prod (Equiv.Perm.cycleType g)
Tactic:
rw [← hψ_range_card]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↥(MonoidHom.ker (φ g)) = Fintype.card ↑(Set.range ⇑(θ g))

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↥(MonoidHom.ker (φ g)) = Fintype.card ↑(Set.range ⇑(θ g))
Tactic:
rw [hψ_range_card']
State after:
no goals