Theorem: OnCycleFactors.hψ_range_card (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↑(Set.range ⇑(θ g)) =
    Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) * Multiset.prod (Equiv.Perm.cycleType g)
Tactic:
rw [Set.card_range_of_injective (hθ_injective g)]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card
      (Equiv.Perm ↑(Function.fixedPoints ⇑g) ×
        ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c))) =
    Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) * Multiset.prod (Equiv.Perm.cycleType g)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card
      (Equiv.Perm ↑(Function.fixedPoints ⇑g) ×
        ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c))) =
    Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) * Multiset.prod (Equiv.Perm.cycleType g)
Tactic:
rw [Fintype.card_prod]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card (Equiv.Perm ↑(Function.fixedPoints ⇑g)) *
      Fintype.card ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)) =
    Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) * Multiset.prod (Equiv.Perm.cycleType g)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card (Equiv.Perm ↑(Function.fixedPoints ⇑g)) *
      Fintype.card ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)) =
    Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) * Multiset.prod (Equiv.Perm.cycleType g)
Tactic:
rw [Fintype.card_perm]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Nat.factorial (Fintype.card ↑(Function.fixedPoints ⇑g)) *
      Fintype.card ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)) =
    Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) * Multiset.prod (Equiv.Perm.cycleType g)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Nat.factorial (Fintype.card ↑(Function.fixedPoints ⇑g)) *
      Fintype.card ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)) =
    Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) * Multiset.prod (Equiv.Perm.cycleType g)
Tactic:
rw [Fintype.card_pi]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ (Nat.factorial (Fintype.card ↑(Function.fixedPoints ⇑g)) *
      Finset.prod Finset.univ fun a => Fintype.card ↥(Subgroup.zpowers ↑a)) =
    Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)) * Multiset.prod (Equiv.Perm.cycleType g)

State before:
case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Nat.factorial (Fintype.card ↑(Function.fixedPoints ⇑g)) =
    Nat.factorial (Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g))
Tactic:
apply congr_arg
State after:
case hx.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↑(Function.fixedPoints ⇑g) = Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)

State before:
case hx.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Fintype.card ↑(Function.fixedPoints ⇑g) = Fintype.card α - Multiset.sum (Equiv.Perm.cycleType g)
Tactic:
exact Equiv.Perm.card_fixedBy g
State after:
no goals

State before:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ (Finset.prod Finset.univ fun a => Fintype.card ↥(Subgroup.zpowers ↑a)) = Multiset.prod (Equiv.Perm.cycleType g)
Tactic:
rw [Equiv.Perm.cycleType]
State after:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ (Finset.prod Finset.univ fun a => Fintype.card ↥(Subgroup.zpowers ↑a)) =
    Multiset.prod (Multiset.map (Finset.card ∘ Equiv.Perm.support) (Equiv.Perm.cycleFactorsFinset g).val)

State before:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ (Finset.prod Finset.univ fun a => Fintype.card ↥(Subgroup.zpowers ↑a)) =
    Multiset.prod (Multiset.map (Finset.card ∘ Equiv.Perm.support) (Equiv.Perm.cycleFactorsFinset g).val)
Tactic:
simp only [Finset.univ_eq_attach, Finset.attach_val, Function.comp_apply]
State after:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ (Finset.prod (Finset.attach (Equiv.Perm.cycleFactorsFinset g)) fun a => Fintype.card ↥(Subgroup.zpowers ↑a)) =
    Multiset.prod (Multiset.map (fun x => (Equiv.Perm.support x).card) (Equiv.Perm.cycleFactorsFinset g).val)

State before:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ (Finset.prod (Finset.attach (Equiv.Perm.cycleFactorsFinset g)) fun a => Fintype.card ↥(Subgroup.zpowers ↑a)) =
    Multiset.prod (Multiset.map (fun x => (Equiv.Perm.support x).card) (Equiv.Perm.cycleFactorsFinset g).val)
Tactic:
rw [Finset.prod_attach (s := g.cycleFactorsFinset) (f := fun a ↦ Fintype.card (Subgroup.zpowers (a : Equiv.Perm α)))]
State after:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ (Finset.prod (Equiv.Perm.cycleFactorsFinset g) fun x => Fintype.card ↥(Subgroup.zpowers x)) =
    Multiset.prod (Multiset.map (fun x => (Equiv.Perm.support x).card) (Equiv.Perm.cycleFactorsFinset g).val)

State before:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ (Finset.prod (Equiv.Perm.cycleFactorsFinset g) fun x => Fintype.card ↥(Subgroup.zpowers x)) =
    Multiset.prod (Multiset.map (fun x => (Equiv.Perm.support x).card) (Equiv.Perm.cycleFactorsFinset g).val)
Tactic:
rw [Finset.prod]
State after:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Multiset.prod (Multiset.map (fun x => Fintype.card ↥(Subgroup.zpowers x)) (Equiv.Perm.cycleFactorsFinset g).val) =
    Multiset.prod (Multiset.map (fun x => (Equiv.Perm.support x).card) (Equiv.Perm.cycleFactorsFinset g).val)

State before:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Multiset.prod (Multiset.map (fun x => Fintype.card ↥(Subgroup.zpowers x)) (Equiv.Perm.cycleFactorsFinset g).val) =
    Multiset.prod (Multiset.map (fun x => (Equiv.Perm.support x).card) (Equiv.Perm.cycleFactorsFinset g).val)
Tactic:
apply congr_arg
State after:
case hy.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Multiset.map (fun x => Fintype.card ↥(Subgroup.zpowers x)) (Equiv.Perm.cycleFactorsFinset g).val =
    Multiset.map (fun x => (Equiv.Perm.support x).card) (Equiv.Perm.cycleFactorsFinset g).val

State before:
case hy.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Multiset.map (fun x => Fintype.card ↥(Subgroup.zpowers x)) (Equiv.Perm.cycleFactorsFinset g).val =
    Multiset.map (fun x => (Equiv.Perm.support x).card) (Equiv.Perm.cycleFactorsFinset g).val
Tactic:
apply Multiset.map_congr rfl
State after:
case hy.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ ∀ x ∈ (Equiv.Perm.cycleFactorsFinset g).val, Fintype.card ↥(Subgroup.zpowers x) = (Equiv.Perm.support x).card

State before:
case hy.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ ∀ x ∈ (Equiv.Perm.cycleFactorsFinset g).val, Fintype.card ↥(Subgroup.zpowers x) = (Equiv.Perm.support x).card
Tactic:
intro x hx
State after:
case hy.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g x : Equiv.Perm α
hx : x ∈ (Equiv.Perm.cycleFactorsFinset g).val
⊢ Fintype.card ↥(Subgroup.zpowers x) = (Equiv.Perm.support x).card

State before:
case hy.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g x : Equiv.Perm α
hx : x ∈ (Equiv.Perm.cycleFactorsFinset g).val
⊢ Fintype.card ↥(Subgroup.zpowers x) = (Equiv.Perm.support x).card
Tactic:
rw [Fintype.card_zpowers, Equiv.Perm.IsCycle.orderOf]
State after:
case hy.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g x : Equiv.Perm α
hx : x ∈ (Equiv.Perm.cycleFactorsFinset g).val
⊢ Equiv.Perm.IsCycle x

State before:
case hy.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g x : Equiv.Perm α
hx : x ∈ (Equiv.Perm.cycleFactorsFinset g).val
⊢ Equiv.Perm.IsCycle x
Tactic:
simp only [Finset.mem_val, Equiv.Perm.mem_cycleFactorsFinset_iff] at hx
State after:
case hy.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g x : Equiv.Perm α
hx : Equiv.Perm.IsCycle x ∧ ∀ a ∈ Equiv.Perm.support x, x a = g a
⊢ Equiv.Perm.IsCycle x

State before:
case hy.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g x : Equiv.Perm α
hx : Equiv.Perm.IsCycle x ∧ ∀ a ∈ Equiv.Perm.support x, x a = g a
⊢ Equiv.Perm.IsCycle x
Tactic:
exact hx.left
State after:
no goals