Theorem: OnCycleFactors.θAux_apply_of_cycleOf_eq_mem (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hx : Equiv.Perm.cycleOf g x = ↑c
⊢ Equiv.Perm.cycleOf g (θAux g k v x) = ↑c
Tactic:
rw [θAux_apply_of_cycleOf_eq c hx]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hx : Equiv.Perm.cycleOf g x = ↑c
⊢ Equiv.Perm.cycleOf g (↑(v c) x) = ↑c

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hx : Equiv.Perm.cycleOf g x = ↑c
⊢ Equiv.Perm.cycleOf g (↑(v c) x) = ↑c
Tactic:
obtain ⟨m, hm⟩ := (v c).prop
State after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hx : Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
⊢ Equiv.Perm.cycleOf g (↑(v c) x) = ↑c

State before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hx : Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
⊢ Equiv.Perm.cycleOf g (↑(v c) x) = ↑c
Tactic:
dsimp only at hm
State after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hx : Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : ↑c ^ m = ↑(v c)
⊢ Equiv.Perm.cycleOf g (↑(v c) x) = ↑c

State before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hx : Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : ↑c ^ m = ↑(v c)
⊢ Equiv.Perm.cycleOf g (↑(v c) x) = ↑c
Tactic:
rw [← hm, ← hx]
State after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hx : Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : ↑c ^ m = ↑(v c)
⊢ Equiv.Perm.cycleOf g ((Equiv.Perm.cycleOf g x ^ m) x) = Equiv.Perm.cycleOf g x

State before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hx : Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : ↑c ^ m = ↑(v c)
⊢ Equiv.Perm.cycleOf g ((Equiv.Perm.cycleOf g x ^ m) x) = Equiv.Perm.cycleOf g x
Tactic:
simp only [Equiv.Perm.cycleOf_zpow_apply_self, Equiv.Perm.cycleOf_self_apply_zpow]
State after:
no goals