Theorem: OnCycleFactors.sign_ψ (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ Equiv.Perm.sign ((θ g) (k, v)) = Equiv.Perm.sign k * Finset.prod Finset.univ fun c => Equiv.Perm.sign ↑(v c)
Tactic:
rw [← Prod.fst_mul_snd ⟨k, v⟩]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ Equiv.Perm.sign ((θ g) (((k, v).1, 1) * (1, (k, v).2))) =
    Equiv.Perm.sign k * Finset.prod Finset.univ fun c => Equiv.Perm.sign ↑(v c)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ Equiv.Perm.sign ((θ g) (((k, v).1, 1) * (1, (k, v).2))) =
    Equiv.Perm.sign k * Finset.prod Finset.univ fun c => Equiv.Perm.sign ↑(v c)
Tactic:
simp only [map_mul]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ Equiv.Perm.sign ((θ g) (k, 1)) * Equiv.Perm.sign ((θ g) (1, v)) =
    Equiv.Perm.sign k * Finset.prod Finset.univ fun c => Equiv.Perm.sign ↑(v c)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ Equiv.Perm.sign ((θ g) (k, 1)) * Equiv.Perm.sign ((θ g) (1, v)) =
    Equiv.Perm.sign k * Finset.prod Finset.univ fun c => Equiv.Perm.sign ↑(v c)
Tactic:
apply congr_arg₂
State after:
case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ Equiv.Perm.sign ((θ g) (k, 1)) = Equiv.Perm.sign k

case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ Equiv.Perm.sign ((θ g) (1, v)) = Finset.prod Finset.univ fun c => Equiv.Perm.sign ↑(v c)

State before:
case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ Equiv.Perm.sign ((θ g) (k, 1)) = Equiv.Perm.sign k
Tactic:
rw [θ_apply_fst, Equiv.Perm.sign_ofSubtype]
State after:
no goals

State before:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ Equiv.Perm.sign ((θ g) (1, v)) = Finset.prod Finset.univ fun c => Equiv.Perm.sign ↑(v c)
Tactic:
rw [← MonoidHom.inr_apply, ← MonoidHom.comp_apply]
State after:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ (MonoidHom.comp Equiv.Perm.sign (θ g))
      ((MonoidHom.inr (Equiv.Perm ↑(MulAction.fixedBy α g))
          ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)))
        v) =
    Finset.prod Finset.univ fun c => Equiv.Perm.sign ↑(v c)

State before:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ (MonoidHom.comp Equiv.Perm.sign (θ g))
      ((MonoidHom.inr (Equiv.Perm ↑(MulAction.fixedBy α g))
          ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)))
        v) =
    Finset.prod Finset.univ fun c => Equiv.Perm.sign ↑(v c)
Tactic:
conv_lhs => rw [← Finset.noncommProd_mul_single v]
State after:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ (MonoidHom.comp Equiv.Perm.sign (θ g))
      ((MonoidHom.inr (Equiv.Perm ↑(MulAction.fixedBy α g))
          ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)))
        (Finset.noncommProd Finset.univ (fun i => Pi.mulSingle i (v i)) ⋯)) =
    Finset.prod Finset.univ fun c => Equiv.Perm.sign ↑(v c)

State before:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ (MonoidHom.comp Equiv.Perm.sign (θ g))
      ((MonoidHom.inr (Equiv.Perm ↑(MulAction.fixedBy α g))
          ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)))
        (Finset.noncommProd Finset.univ (fun i => Pi.mulSingle i (v i)) ⋯)) =
    Finset.prod Finset.univ fun c => Equiv.Perm.sign ↑(v c)
Tactic:
simp only [Finset.noncommProd_map]
State after:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ Finset.noncommProd Finset.univ
      (fun i =>
        (MonoidHom.comp Equiv.Perm.sign (θ g))
          ((MonoidHom.inr (Equiv.Perm ↑(MulAction.fixedBy α g))
              ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)))
            (Pi.mulSingle i (v i))))
      ⋯ =
    Finset.prod Finset.univ fun c => Equiv.Perm.sign ↑(v c)

State before:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ Finset.noncommProd Finset.univ
      (fun i =>
        (MonoidHom.comp Equiv.Perm.sign (θ g))
          ((MonoidHom.inr (Equiv.Perm ↑(MulAction.fixedBy α g))
              ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)))
            (Pi.mulSingle i (v i))))
      ⋯ =
    Finset.prod Finset.univ fun c => Equiv.Perm.sign ↑(v c)
Tactic:
rw [Finset.noncommProd_eq_prod]
State after:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ (Finset.prod Finset.univ fun i =>
      (MonoidHom.comp Equiv.Perm.sign (θ g))
        ((MonoidHom.inr (Equiv.Perm ↑(MulAction.fixedBy α g))
            ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)))
          (Pi.mulSingle i (v i)))) =
    Finset.prod Finset.univ fun c => Equiv.Perm.sign ↑(v c)

State before:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ (Finset.prod Finset.univ fun i =>
      (MonoidHom.comp Equiv.Perm.sign (θ g))
        ((MonoidHom.inr (Equiv.Perm ↑(MulAction.fixedBy α g))
            ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)))
          (Pi.mulSingle i (v i)))) =
    Finset.prod Finset.univ fun c => Equiv.Perm.sign ↑(v c)
Tactic:
apply Finset.prod_congr rfl
State after:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ ∀ x ∈ Finset.univ,
    (MonoidHom.comp Equiv.Perm.sign (θ g))
        ((MonoidHom.inr (Equiv.Perm ↑(MulAction.fixedBy α g))
            ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)))
          (Pi.mulSingle x (v x))) =
      Equiv.Perm.sign ↑(v x)

State before:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ ∀ x ∈ Finset.univ,
    (MonoidHom.comp Equiv.Perm.sign (θ g))
        ((MonoidHom.inr (Equiv.Perm ↑(MulAction.fixedBy α g))
            ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)))
          (Pi.mulSingle x (v x))) =
      Equiv.Perm.sign ↑(v x)
Tactic:
intro c _
State after:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
a✝ : c ∈ Finset.univ
⊢ (MonoidHom.comp Equiv.Perm.sign (θ g))
      ((MonoidHom.inr (Equiv.Perm ↑(MulAction.fixedBy α g))
          ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)))
        (Pi.mulSingle c (v c))) =
    Equiv.Perm.sign ↑(v c)

State before:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
a✝ : c ∈ Finset.univ
⊢ (MonoidHom.comp Equiv.Perm.sign (θ g))
      ((MonoidHom.inr (Equiv.Perm ↑(MulAction.fixedBy α g))
          ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)))
        (Pi.mulSingle c (v c))) =
    Equiv.Perm.sign ↑(v c)
Tactic:
simp only [MonoidHom.inr_apply, MonoidHom.coe_comp, Function.comp_apply, θ_apply_single]
State after:
no goals