Theorem: OnCycleFactors.hθ_1 (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 : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ ((θ g) uv) x = ↑(uv.1 { val := x, property := hx })
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 : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ ({ toOneHom := { toFun := fun kv => θFun g kv.1 kv.2, map_one' := ⋯ }, map_mul' := ⋯ } uv) x =
    ↑(uv.1 { val := x, property := hx })

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 : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ ({ toOneHom := { toFun := fun kv => θFun g kv.1 kv.2, map_one' := ⋯ }, map_mul' := ⋯ } uv) x =
    ↑(uv.1 { val := x, property := hx })
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 : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ ({
          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.1 { val := x, property := hx })

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 : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ ({
          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.1 { val := x, property := hx })
Tactic:
simp only [Equiv.coe_fn_mk, 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 : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ θAux g uv.1 uv.2 x = ↑(uv.1 { val := x, property := hx })

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 : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ θAux g uv.1 uv.2 x = ↑(uv.1 { val := x, property := hx })
Tactic:
rw [θAux_apply_of_mem_fixedPoints, Equiv.Perm.ofSubtype_apply_of_mem]
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 : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ x ∈ Function.fixedPoints ⇑g

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