Theorem: OnCycleFactors.θAux_mul (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)
k : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
x : α
⊢ θAux g k' v' (θAux g k v x) = θAux g (k' * k) (v' * v) 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)
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
⊢ θAux g k' v' (θAux g k v x) = θAux g (k' * k) (v' * v) 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)
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
⊢ θAux g k' v' (θAux g k v x) = θAux g (k' * k) (v' * v) 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)
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
⊢ θAux g k' v' (θAux g k v x) = θAux g (k' * k) (v' * v) x
Tactic:
rw [θAux_apply_of_cycleOf_eq ⟨g.cycleOf x, hx⟩ (θAux_apply_of_cycleOf_eq_mem ⟨_, hx⟩ rfl),
  θAux_apply_of_cycleOf_eq ⟨g.cycleOf x, hx⟩ rfl,
  θ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)
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
⊢ ↑(v' { val := Equiv.Perm.cycleOf g x, property := hx }) (↑(v { val := Equiv.Perm.cycleOf g x, property := hx }) x) =
    ↑((v' * v) { val := Equiv.Perm.cycleOf g x, property := hx }) 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)
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
⊢ ↑(v' { val := Equiv.Perm.cycleOf g x, property := hx }) (↑(v { val := Equiv.Perm.cycleOf g x, property := hx }) x) =
    ↑((v' * v) { val := Equiv.Perm.cycleOf g x, property := hx }) x
Tactic:
simp only [ne_eq, Pi.mul_apply, Submonoid.coe_mul,
  Subgroup.coe_toSubmonoid, Equiv.Perm.coe_mul, Function.comp_apply]
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)
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
⊢ θAux g k' v' (θAux g k v x) = θAux g (k' * k) (v' * v) x
Tactic:
have hx' : g.cycleOf (θAux g k v x) ∉ g.cycleFactorsFinset := by
  rw [θAux_cycleOf_apply_eq]
  exact 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)
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
hx' : Equiv.Perm.cycleOf g (θAux g k v x) ∉ Equiv.Perm.cycleFactorsFinset g
⊢ θAux g k' v' (θAux g k v x) = θAux g (k' * k) (v' * v) 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)
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
hx' : Equiv.Perm.cycleOf g (θAux g k v x) ∉ Equiv.Perm.cycleFactorsFinset g
⊢ θAux g k' v' (θAux g k v x) = θAux g (k' * k) (v' * v) x
Tactic:
nth_rewrite 1 [θAux, dif_neg 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)
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
hx' : Equiv.Perm.cycleOf g (θAux g k v x) ∉ Equiv.Perm.cycleFactorsFinset g
⊢ (Equiv.Perm.ofSubtype k') (θAux g k v x) = θAux g (k' * k) (v' * v) 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)
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
hx' : Equiv.Perm.cycleOf g (θAux g k v x) ∉ Equiv.Perm.cycleFactorsFinset g
⊢ (Equiv.Perm.ofSubtype k') (θAux g k v x) = θAux g (k' * k) (v' * v) x
Tactic:
simp only [θAux, dif_neg 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)
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
hx' : Equiv.Perm.cycleOf g (θAux g k v x) ∉ Equiv.Perm.cycleFactorsFinset g
⊢ (Equiv.Perm.ofSubtype k') ((Equiv.Perm.ofSubtype k) x) = (Equiv.Perm.ofSubtype (k' * k)) 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)
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
hx' : Equiv.Perm.cycleOf g (θAux g k v x) ∉ Equiv.Perm.cycleFactorsFinset g
⊢ (Equiv.Perm.ofSubtype k') ((Equiv.Perm.ofSubtype k) x) = (Equiv.Perm.ofSubtype (k' * k)) x
Tactic:
simp only [map_mul, Equiv.Perm.coe_mul, Function.comp_apply]
State after:
no goals

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)
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.cycleFactorsFinset g
Tactic:
rw [θAux_cycleOf_apply_eq]
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)
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 x ∉ Equiv.Perm.cycleFactorsFinset g

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)
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 x ∉ Equiv.Perm.cycleFactorsFinset g
Tactic:
exact hx
State after:
no goals