Theorem: OnCycleFactors.θAux_cycleOf_apply_eq (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 : α
⊢ Equiv.Perm.cycleOf g (θAux g k v x) = Equiv.Perm.cycleOf g x
Tactic:
by_cases hx : g.cycleOf x ∈ g.cycleFactorsFinset
State after:
case pos
α : 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 : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ Equiv.Perm.cycleOf g (θAux g k v x) = Equiv.Perm.cycleOf g x

case neg
α : 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 : α
hx : Equiv.Perm.cycleOf g x ∉ Equiv.Perm.cycleFactorsFinset g
⊢ Equiv.Perm.cycleOf g (θAux g k v x) = Equiv.Perm.cycleOf g x

State before:
case pos
α : 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 : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ Equiv.Perm.cycleOf g (θAux g k v x) = Equiv.Perm.cycleOf g x
Tactic:
rw [θAux_apply_of_cycleOf_eq ⟨g.cycleOf x, hx⟩ rfl]
State after:
case pos
α : 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 : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ Equiv.Perm.cycleOf g (↑(v { val := Equiv.Perm.cycleOf g x, property := hx }) x) = Equiv.Perm.cycleOf g x

State before:
case pos
α : 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 : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ Equiv.Perm.cycleOf g (↑(v { val := Equiv.Perm.cycleOf g x, property := hx }) x) = Equiv.Perm.cycleOf g x
Tactic:
obtain ⟨m, hm⟩ := (v _).prop
State after:
case pos.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 : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
m : ℤ
hm : (fun x => ↑?m.317682 ^ x) m = ↑(v ?m.317682)
⊢ Equiv.Perm.cycleOf g (↑(v { val := Equiv.Perm.cycleOf g x, property := hx }) x) = Equiv.Perm.cycleOf g x

State before:
case pos.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 : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
m : ℤ
hm : (fun x => ↑?m.317682 ^ x) m = ↑(v ?m.317682)
⊢ Equiv.Perm.cycleOf g (↑(v { val := Equiv.Perm.cycleOf g x, property := hx }) x) = Equiv.Perm.cycleOf g x
Tactic:
dsimp only at hm
State after:
case pos.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 : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
m : ℤ
hm : ↑?m.317682 ^ m = ↑(v ?m.317682)
⊢ Equiv.Perm.cycleOf g (↑(v { val := Equiv.Perm.cycleOf g x, property := hx }) x) = Equiv.Perm.cycleOf g x

State before:
case pos.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 : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
m : ℤ
hm : ↑?m.317682 ^ m = ↑(v ?m.317682)
⊢ Equiv.Perm.cycleOf g (↑(v { val := Equiv.Perm.cycleOf g x, property := hx }) x) = Equiv.Perm.cycleOf g x
Tactic:
rw [← hm]
State after:
case pos.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 : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
m : ℤ
hm : ↑{ val := Equiv.Perm.cycleOf g x, property := hx } ^ m = ↑(v { val := Equiv.Perm.cycleOf g x, property := hx })
⊢ Equiv.Perm.cycleOf g ((↑{ val := Equiv.Perm.cycleOf g x, property := hx } ^ m) x) = Equiv.Perm.cycleOf g x

State before:
case pos.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 : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
m : ℤ
hm : ↑{ val := Equiv.Perm.cycleOf g x, property := hx } ^ m = ↑(v { val := Equiv.Perm.cycleOf g x, property := hx })
⊢ Equiv.Perm.cycleOf g ((↑{ val := Equiv.Perm.cycleOf g x, property := hx } ^ 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

State before:
case neg
α : 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 : α
hx : Equiv.Perm.cycleOf g x ∉ Equiv.Perm.cycleFactorsFinset g
⊢ Equiv.Perm.cycleOf g (θAux g k v x) = Equiv.Perm.cycleOf g x
Tactic:
rw [g.cycleOf_mem_cycleFactorsFinset_iff, Equiv.Perm.not_mem_support] at hx
State after:
case neg
α : 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 : α
hx : g x = x
⊢ Equiv.Perm.cycleOf g (θAux g k v x) = Equiv.Perm.cycleOf g x

State before:
case neg
α : 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 : α
hx : g x = x
⊢ Equiv.Perm.cycleOf g (θAux g k v x) = Equiv.Perm.cycleOf g x
Tactic:
rw [g.cycleOf_eq_one_iff.mpr hx, g.cycleOf_eq_one_iff,
  ← Function.mem_fixedPoints_iff]
State after:
case neg
α : 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 : α
hx : g x = x
⊢ θAux g k v x ∈ Function.fixedPoints ⇑g

State before:
case neg
α : 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 : α
hx : g x = x
⊢ θAux g k v x ∈ Function.fixedPoints ⇑g
Tactic:
apply θAux_apply_of_mem_fixedPoints_mem
State after:
case neg.hx
α : 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 : α
hx : g x = x
⊢ x ∈ Function.fixedPoints ⇑g

State before:
case neg.hx
α : 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 : α
hx : g x = x
⊢ x ∈ Function.fixedPoints ⇑g
Tactic:
exact hx
State after:
no goals