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

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ Function.Injective ⇑(θ g)
Tactic:
rw [← MonoidHom.ker_eq_bot_iff, eq_bot_iff]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ MonoidHom.ker (θ g) ≤ ⊥

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
⊢ MonoidHom.ker (θ g) ≤ ⊥
Tactic:
rintro ⟨u, v⟩
State after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ (u, v) ∈ MonoidHom.ker (θ g) → (u, v) ∈ ⊥

State before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ (u, v) ∈ MonoidHom.ker (θ g) → (u, v) ∈ ⊥
Tactic:
unfold θ
State after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ (u, v) ∈ MonoidHom.ker { toOneHom := { toFun := fun kv => θFun g kv.1 kv.2, map_one' := ⋯ }, map_mul' := ⋯ } →
    (u, v) ∈ ⊥

State before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ (u, v) ∈ MonoidHom.ker { toOneHom := { toFun := fun kv => θFun g kv.1 kv.2, map_one' := ⋯ }, map_mul' := ⋯ } →
    (u, v) ∈ ⊥
Tactic:
unfold θFun
State after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ (u, v) ∈
      MonoidHom.ker
        {
          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' := ⋯ } →
    (u, v) ∈ ⊥

State before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ (u, v) ∈
      MonoidHom.ker
        {
          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' := ⋯ } →
    (u, v) ∈ ⊥
Tactic:
simp only [MonoidHom.coe_mk, OneHom.coe_mk, MonoidHom.mem_ker, Equiv.Perm.ext_iff]
State after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ (∀ (x : α), { toFun := θAux g u v, invFun := θAux g u⁻¹ v⁻¹, left_inv := ⋯, right_inv := ⋯ } x = 1 x) → (u, v) ∈ ⊥

State before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ (∀ (x : α), { toFun := θAux g u v, invFun := θAux g u⁻¹ v⁻¹, left_inv := ⋯, right_inv := ⋯ } x = 1 x) → (u, v) ∈ ⊥
Tactic:
simp only [Equiv.coe_fn_mk, Equiv.Perm.coe_one, id_eq]
State after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ (∀ (x : α), θAux g u v x = x) → (u, v) ∈ ⊥

State before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ (∀ (x : α), θAux g u v x = x) → (u, v) ∈ ⊥
Tactic:
intro huv
State after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
⊢ (u, v) ∈ ⊥

State before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
⊢ (u, v) ∈ ⊥
Tactic:
simp only [Subgroup.mem_bot, Prod.mk_eq_one, MonoidHom.mem_ker]
State after:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
⊢ u = 1 ∧ v = 1

State before:
case mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
⊢ u = 1 ∧ v = 1
Tactic:
constructor
State after:
case mk.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
⊢ u = 1

case mk.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
⊢ v = 1

State before:
case mk.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
⊢ u = 1
Tactic:
ext ⟨x, hx⟩
State after:
case mk.left.H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ ↑(u { val := x, property := hx }) = ↑(1 { val := x, property := hx })

State before:
case mk.left.H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ ↑(u { val := x, property := hx }) = ↑(1 { val := x, property := hx })
Tactic:
simp only [Equiv.Perm.coe_one, id_eq]
State after:
case mk.left.H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ ↑(u { val := x, property := hx }) = x

State before:
case mk.left.H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ ↑(u { val := x, property := hx }) = x
Tactic:
conv_rhs => rw [← huv x]
State after:
case mk.left.H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ ↑(u { val := x, property := hx }) = θAux g u v x

State before:
case mk.left.H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ ↑(u { val := x, property := hx }) = θAux g u v x
Tactic:
rw [θAux_apply_of_mem_fixedPoints, Equiv.Perm.ofSubtype_apply_of_mem]
State after:
case mk.left.H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ x ∈ Function.fixedPoints ⇑g

State before:
case mk.left.H.mk.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ x ∈ Function.fixedPoints ⇑g
Tactic:
exact hx
State after:
no goals

State before:
case mk.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
⊢ v = 1
Tactic:
ext c x
State after:
case mk.right.h.a.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
⊢ ↑(v c) x = ↑(1 c) x

State before:
case mk.right.h.a.H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
⊢ ↑(v c) x = ↑(1 c) x
Tactic:
by_cases hx : g.cycleOf x = 1
State after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : Equiv.Perm.cycleOf g x = 1
⊢ ↑(v c) x = ↑(1 c) x

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : ¬Equiv.Perm.cycleOf g x = 1
⊢ ↑(v c) x = ↑(1 c) x

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : ¬Equiv.Perm.cycleOf g x = 1
⊢ ↑(v c) x = ↑(1 c) x
Tactic:
rw [← ne_eq, Equiv.Perm.cycleOf_ne_one_iff_mem] at hx
State after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ↑(v c) x = ↑(1 c) x

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ↑(v c) x = ↑(1 c) x
Tactic:
simp only [Pi.one_apply, OneMemClass.coe_one, Equiv.Perm.coe_one, id_eq]
State after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ↑(v c) x = x

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ↑(v c) x = x
Tactic:
by_cases hc : g.cycleOf x = ↑c
State after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : Equiv.Perm.cycleOf g x = ↑c
⊢ ↑(v c) x = x

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ ↑(v c) x = x

State before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : Equiv.Perm.cycleOf g x = 1
⊢ ↑(v c) x = ↑(1 c) x
Tactic:
simp only [Equiv.Perm.cycleOf_eq_one_iff, ← Equiv.Perm.not_mem_support] at hx
State after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
⊢ ↑(v c) x = ↑(1 c) x

State before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
⊢ ↑(v c) x = ↑(1 c) x
Tactic:
simp only [Pi.one_apply, OneMemClass.coe_one, Equiv.Perm.coe_one, id_eq]
State after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
⊢ ↑(v c) x = x

State before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
⊢ ↑(v c) x = x
Tactic:
obtain ⟨m, hm⟩ := (v c).prop
State after:
case pos.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
⊢ ↑(v c) x = x

State before:
case pos.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
⊢ ↑(v c) x = x
Tactic:
rw [← hm]
State after:
case pos.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
⊢ ((fun x => ↑c ^ x) m) x = x

State before:
case pos.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
⊢ ((fun x => ↑c ^ x) m) x = x
Tactic:
dsimp
State after:
case pos.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
⊢ (↑c ^ m) x = x

State before:
case pos.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
⊢ (↑c ^ m) x = x
Tactic:
rw [← Equiv.Perm.not_mem_support]
State after:
case pos.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
⊢ x ∉ Equiv.Perm.support (↑c ^ m)

State before:
case pos.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
⊢ x ∉ Equiv.Perm.support (↑c ^ m)
Tactic:
intro hx'
State after:
case pos.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
⊢ False

State before:
case pos.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
⊢ False
Tactic:
suffices ¬ x ∈ Equiv.Perm.support c by
  apply this
  apply Equiv.Perm.support_zpow_le _ _ hx'
State after:
case pos.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
⊢ x ∉ Equiv.Perm.support ↑c

State before:
case pos.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
⊢ x ∉ Equiv.Perm.support ↑c
Tactic:
intro hx'
State after:
case pos.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
hx'✝ : x ∈ Equiv.Perm.support (↑c ^ m)
hx' : x ∈ Equiv.Perm.support ↑c
⊢ False

State before:
case pos.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
hx'✝ : x ∈ Equiv.Perm.support (↑c ^ m)
hx' : x ∈ Equiv.Perm.support ↑c
⊢ False
Tactic:
apply hx
State after:
case pos.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
hx'✝ : x ∈ Equiv.Perm.support (↑c ^ m)
hx' : x ∈ Equiv.Perm.support ↑c
⊢ x ∈ Equiv.Perm.support g

State before:
case pos.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
hx'✝ : x ∈ Equiv.Perm.support (↑c ^ m)
hx' : x ∈ Equiv.Perm.support ↑c
⊢ x ∈ Equiv.Perm.support g
Tactic:
apply Equiv.Perm.mem_cycleFactorsFinset_support_le c.prop hx'
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
this : x ∉ Equiv.Perm.support ↑c
⊢ False
Tactic:
apply this
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
this : x ∉ Equiv.Perm.support ↑c
⊢ x ∈ Equiv.Perm.support ↑c

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
this : x ∉ Equiv.Perm.support ↑c
⊢ x ∈ Equiv.Perm.support ↑c
Tactic:
apply Equiv.Perm.support_zpow_le _ _ hx'
State after:
no goals

State before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : Equiv.Perm.cycleOf g x = ↑c
⊢ ↑(v c) x = x
Tactic:
rw [← θAux_apply_of_cycleOf_eq c hc, huv]
State after:
no goals

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ ↑(v c) x = x
Tactic:
obtain ⟨m, hm⟩ := (v c).prop
State after:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
⊢ ↑(v c) x = x

State before:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
⊢ ↑(v c) x = x
Tactic:
rw [← hm]
State after:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
⊢ ((fun x => ↑c ^ x) m) x = x

State before:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
⊢ ((fun x => ↑c ^ x) m) x = x
Tactic:
dsimp
State after:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
⊢ (↑c ^ m) x = x

State before:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
⊢ (↑c ^ m) x = x
Tactic:
rw [← Equiv.Perm.not_mem_support]
State after:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
⊢ x ∉ Equiv.Perm.support (↑c ^ m)

State before:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
⊢ x ∉ Equiv.Perm.support (↑c ^ m)
Tactic:
intro hx'
State after:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
⊢ False

State before:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
⊢ False
Tactic:
suffices ¬ x ∈ Equiv.Perm.support c by
  apply this
  apply Equiv.Perm.support_zpow_le _ _ hx'
State after:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
⊢ x ∉ Equiv.Perm.support ↑c

State before:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
⊢ x ∉ Equiv.Perm.support ↑c
Tactic:
intro h
State after:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
h : x ∈ Equiv.Perm.support ↑c
⊢ False

State before:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
h : x ∈ Equiv.Perm.support ↑c
⊢ False
Tactic:
exact hc (Equiv.Perm.cycle_is_cycleOf h c.prop).symm
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
this : x ∉ Equiv.Perm.support ↑c
⊢ False
Tactic:
apply this
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
this : x ∉ Equiv.Perm.support ↑c
⊢ x ∈ Equiv.Perm.support ↑c

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ g : Equiv.Perm α
u : Equiv.Perm ↑(Function.fixedPoints ⇑g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
huv : ∀ (x : α), θAux g u v x = x
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑(v c)
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
this : x ∉ Equiv.Perm.support ↑c
⊢ x ∈ Equiv.Perm.support ↑c
Tactic:
apply Equiv.Perm.support_zpow_le _ _ hx'
State after:
no goals