Theorem: OnCycleFactors.hφ'_equivariant (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ ↑((φ' a) τ) • ↑c = ↑(↑τ c)
Tactic:
rw [ConjAct.smul_def]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ ConjAct.ofConjAct ↑((φ' a) τ) * ↑c * (ConjAct.ofConjAct ↑((φ' a) τ))⁻¹ = ↑(↑τ c)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ ConjAct.ofConjAct ↑((φ' a) τ) * ↑c * (ConjAct.ofConjAct ↑((φ' a) τ))⁻¹ = ↑(↑τ c)
Tactic:
rw [mul_inv_eq_iff_eq_mul]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ ConjAct.ofConjAct ↑((φ' a) τ) * ↑c = ↑(↑τ c) * ConjAct.ofConjAct ↑((φ' a) τ)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ ConjAct.ofConjAct ↑((φ' a) τ) * ↑c = ↑(↑τ c) * ConjAct.ofConjAct ↑((φ' a) τ)
Tactic:
ext x
State after:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
⊢ (ConjAct.ofConjAct ↑((φ' a) τ) * ↑c) x = (↑(↑τ c) * ConjAct.ofConjAct ↑((φ' a) τ)) x

State before:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : ↥(Iφ g)
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
⊢ (ConjAct.ofConjAct ↑((φ' a) τ) * ↑c) x = (↑(↑τ c) * ConjAct.ofConjAct ↑((φ' a) τ)) x
Tactic:
exact OnCycleFactors.k_cycle_apply τ.prop c x
State after:
no goals