Theorem: OnCycleFactors.θAux_apply_of_mem_fixedPoints (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 : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ θAux g k v x = (Equiv.Perm.ofSubtype k) x
Tactic:
rw [θAux, dif_neg]
State after:
case hnc
α : 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 : x ∈ Function.fixedPoints ⇑g
⊢ Equiv.Perm.cycleOf g x ∉ Equiv.Perm.cycleFactorsFinset g

State before:
case hnc
α : 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 : x ∈ Function.fixedPoints ⇑g
⊢ Equiv.Perm.cycleOf g x ∉ Equiv.Perm.cycleFactorsFinset g
Tactic:
rw [Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff, Equiv.Perm.not_mem_support]
State after:
case hnc
α : 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 : x ∈ Function.fixedPoints ⇑g
⊢ g x = x

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