Theorem: OnCycleFactors.hθ_2 (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
uv :
  Equiv.Perm ↑(Function.fixedPoints ⇑g) × ((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
⊢ ((θ g) uv) x = ↑(uv.2 c) x
Tactic:
unfold θ
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
uv :
  Equiv.Perm ↑(Function.fixedPoints ⇑g) × ((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
⊢ ({ toOneHom := { toFun := fun kv => θFun g kv.1 kv.2, map_one' := ⋯ }, map_mul' := ⋯ } uv) x = ↑(uv.2 c) x

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
uv :
  Equiv.Perm ↑(Function.fixedPoints ⇑g) × ((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
⊢ ({ toOneHom := { toFun := fun kv => θFun g kv.1 kv.2, map_one' := ⋯ }, map_mul' := ⋯ } uv) x = ↑(uv.2 c) x
Tactic:
unfold θFun
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
uv :
  Equiv.Perm ↑(Function.fixedPoints ⇑g) × ((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
⊢ ({
          toOneHom :=
            {
              toFun := fun kv =>
                { toFun := θAux g kv.1 kv.2, invFun := θAux g kv.1⁻¹ kv.2⁻¹, left_inv := ⋯, right_inv := ⋯ },
              map_one' := ⋯ },
          map_mul' := ⋯ }
        uv)
      x =
    ↑(uv.2 c) x

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
uv :
  Equiv.Perm ↑(Function.fixedPoints ⇑g) × ((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
⊢ ({
          toOneHom :=
            {
              toFun := fun kv =>
                { toFun := θAux g kv.1 kv.2, invFun := θAux g kv.1⁻¹ kv.2⁻¹, left_inv := ⋯, right_inv := ⋯ },
              map_one' := ⋯ },
          map_mul' := ⋯ }
        uv)
      x =
    ↑(uv.2 c) x
Tactic:
simp only [MonoidHom.coe_mk, OneHom.coe_mk, Equiv.coe_fn_mk]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
uv :
  Equiv.Perm ↑(Function.fixedPoints ⇑g) × ((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
⊢ θAux g uv.1 uv.2 x = ↑(uv.2 c) x

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
uv :
  Equiv.Perm ↑(Function.fixedPoints ⇑g) × ((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
⊢ θAux g uv.1 uv.2 x = ↑(uv.2 c) x
Tactic:
exact θAux_apply_of_cycleOf_eq c hx
State after:
no goals