Theorem: OnCycleFactors.θ_apply_single (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
⊢ (θ g) (1, Pi.mulSingle c vc) = ↑vc
Tactic:
ext x
State after:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
⊢ ((θ g) (1, Pi.mulSingle c vc)) x = ↑vc x

State before:
case H
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
⊢ ((θ g) (1, Pi.mulSingle c vc)) x = ↑vc x
Tactic:
by_cases hx : g.cycleOf x ∈ g.cycleFactorsFinset
State after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ((θ g) (1, Pi.mulSingle c vc)) x = ↑vc x

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∉ Equiv.Perm.cycleFactorsFinset g
⊢ ((θ g) (1, Pi.mulSingle c vc)) x = ↑vc x

State before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ((θ g) (1, Pi.mulSingle c vc)) x = ↑vc x
Tactic:
rw [hθ_2 _ x ⟨g.cycleOf x, hx⟩ rfl]
State after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ↑((1, Pi.mulSingle c vc).2 { val := Equiv.Perm.cycleOf g x, property := hx }) x = ↑vc x

State before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
⊢ ↑((1, Pi.mulSingle c vc).2 { val := Equiv.Perm.cycleOf g x, property := hx }) x = ↑vc x
Tactic:
by_cases hc : g.cycleOf x = c
State after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : Equiv.Perm.cycleOf g x = ↑c
⊢ ↑((1, Pi.mulSingle c vc).2 { val := Equiv.Perm.cycleOf g x, property := hx }) x = ↑vc x

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ ↑((1, Pi.mulSingle c vc).2 { val := Equiv.Perm.cycleOf g x, property := hx }) x = ↑vc x

State before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : Equiv.Perm.cycleOf g x = ↑c
⊢ ↑((1, Pi.mulSingle c vc).2 { val := Equiv.Perm.cycleOf g x, property := hx }) x = ↑vc x
Tactic:
suffices c = ⟨g.cycleOf x, hx⟩ by
  rw [← this]
  simp only [Pi.mulSingle_eq_same]
State after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : Equiv.Perm.cycleOf g x = ↑c
⊢ c = { val := Equiv.Perm.cycleOf g x, property := hx }

State before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : Equiv.Perm.cycleOf g x = ↑c
⊢ c = { val := Equiv.Perm.cycleOf g x, property := hx }
Tactic:
rw [← Subtype.coe_inj, ← hc]
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : Equiv.Perm.cycleOf g x = ↑c
this : c = { val := Equiv.Perm.cycleOf g x, property := hx }
⊢ ↑((1, Pi.mulSingle c vc).2 { val := Equiv.Perm.cycleOf g x, property := hx }) x = ↑vc x
Tactic:
rw [← this]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : Equiv.Perm.cycleOf g x = ↑c
this : c = { val := Equiv.Perm.cycleOf g x, property := hx }
⊢ ↑((1, Pi.mulSingle c vc).2 c) x = ↑vc x

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : Equiv.Perm.cycleOf g x = ↑c
this : c = { val := Equiv.Perm.cycleOf g x, property := hx }
⊢ ↑((1, Pi.mulSingle c vc).2 c) x = ↑vc x
Tactic:
simp only [Pi.mulSingle_eq_same]
State after:
no goals

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ ↑((1, Pi.mulSingle c vc).2 { val := Equiv.Perm.cycleOf g x, property := hx }) x = ↑vc x
Tactic:
simp only [ne_eq]
State after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ ↑(Pi.mulSingle c vc { val := Equiv.Perm.cycleOf g x, property := hx }) x = ↑vc x

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ ↑(Pi.mulSingle c vc { val := Equiv.Perm.cycleOf g x, property := hx }) x = ↑vc x
Tactic:
rw [Pi.mulSingle_eq_of_ne]
State after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ ↑1 x = ↑vc x

case neg.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ { val := Equiv.Perm.cycleOf g x, property := hx } ≠ c

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ ↑1 x = ↑vc x

case neg.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ { val := Equiv.Perm.cycleOf g x, property := hx } ≠ c
Tactic:
simp only [OneMemClass.coe_one, Equiv.Perm.coe_one, id_eq]
State after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ x = ↑vc x

case neg.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ { val := Equiv.Perm.cycleOf g x, property := hx } ≠ c

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ x = ↑vc x

case neg.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ { val := Equiv.Perm.cycleOf g x, property := hx } ≠ c
Tactic:
apply symm
State after:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ ↑vc x = x

case neg.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ { val := Equiv.Perm.cycleOf g x, property := hx } ≠ c

State before:
case neg.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ ↑vc x = x

case neg.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ { val := Equiv.Perm.cycleOf g x, property := hx } ≠ c
Tactic:
obtain ⟨m, hm⟩ := vc.prop
State after:
case neg.a.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
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 = ↑vc
⊢ ↑vc x = x

case neg.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ { val := Equiv.Perm.cycleOf g x, property := hx } ≠ c

State before:
case neg.a.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
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 = ↑vc
⊢ ↑vc x = x

case neg.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ { val := Equiv.Perm.cycleOf g x, property := hx } ≠ c
Tactic:
dsimp at hm
State after:
case neg.a.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : ↑c ^ m = ↑vc
⊢ ↑vc x = x

case neg.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ { val := Equiv.Perm.cycleOf g x, property := hx } ≠ c

State before:
case neg.a.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : ↑c ^ m = ↑vc
⊢ ↑vc x = x

case neg.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ { val := Equiv.Perm.cycleOf g x, property := hx } ≠ c
Tactic:
rw [← hm, ← Equiv.Perm.not_mem_support]
State after:
case neg.a.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : ↑c ^ m = ↑vc
⊢ x ∉ Equiv.Perm.support (↑c ^ m)

case neg.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ { val := Equiv.Perm.cycleOf g x, property := hx } ≠ c

State before:
case neg.a.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : ↑c ^ m = ↑vc
⊢ x ∉ Equiv.Perm.support (↑c ^ m)

case neg.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ { val := Equiv.Perm.cycleOf g x, property := hx } ≠ c
Tactic:
intro hx'
State after:
case neg.a.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : ↑c ^ m = ↑vc
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
⊢ False

case neg.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ { val := Equiv.Perm.cycleOf g x, property := hx } ≠ c

State before:
case neg.a.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : ↑c ^ m = ↑vc
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
⊢ False

case neg.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ { val := Equiv.Perm.cycleOf g x, property := hx } ≠ c
Tactic:
apply hc
State after:
case neg.a.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : ↑c ^ m = ↑vc
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
⊢ Equiv.Perm.cycleOf g x = ↑c

case neg.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ { val := Equiv.Perm.cycleOf g x, property := hx } ≠ c

State before:
case neg.a.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : ↑c ^ m = ↑vc
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
⊢ Equiv.Perm.cycleOf g x = ↑c

case neg.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ { val := Equiv.Perm.cycleOf g x, property := hx } ≠ c
Tactic:
apply symm
State after:
case neg.a.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : ↑c ^ m = ↑vc
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
⊢ ↑c = Equiv.Perm.cycleOf g x

case neg.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ { val := Equiv.Perm.cycleOf g x, property := hx } ≠ c

State before:
case neg.a.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : ↑c ^ m = ↑vc
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
⊢ ↑c = Equiv.Perm.cycleOf g x

case neg.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ { val := Equiv.Perm.cycleOf g x, property := hx } ≠ c
Tactic:
apply Equiv.Perm.cycle_is_cycleOf
State after:
case neg.a.intro.a.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : ↑c ^ m = ↑vc
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
⊢ x ∈ Equiv.Perm.support ↑c

case neg.a.intro.a.hc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : ↑c ^ m = ↑vc
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
⊢ ↑c ∈ Equiv.Perm.cycleFactorsFinset g

case neg.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ { val := Equiv.Perm.cycleOf g x, property := hx } ≠ c

State before:
case neg.a.intro.a.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : ↑c ^ m = ↑vc
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
⊢ x ∈ Equiv.Perm.support ↑c

case neg.a.intro.a.hc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : ↑c ^ m = ↑vc
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
⊢ ↑c ∈ Equiv.Perm.cycleFactorsFinset g

case neg.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ { val := Equiv.Perm.cycleOf g x, property := hx } ≠ c
Tactic:
apply Equiv.Perm.support_zpow_le _ _ hx'
State after:
case neg.a.intro.a.hc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : ↑c ^ m = ↑vc
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
⊢ ↑c ∈ Equiv.Perm.cycleFactorsFinset g

case neg.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ { val := Equiv.Perm.cycleOf g x, property := hx } ≠ c

State before:
case neg.a.intro.a.hc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
m : ℤ
hm : ↑c ^ m = ↑vc
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
⊢ ↑c ∈ Equiv.Perm.cycleFactorsFinset g

case neg.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ { val := Equiv.Perm.cycleOf g x, property := hx } ≠ c
Tactic:
exact c.prop
State after:
case neg.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ { val := Equiv.Perm.cycleOf g x, property := hx } ≠ c

State before:
case neg.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
⊢ { val := Equiv.Perm.cycleOf g x, property := hx } ≠ c
Tactic:
intro hc'
State after:
case neg.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
hc' : { val := Equiv.Perm.cycleOf g x, property := hx } = c
⊢ False

State before:
case neg.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
hc' : { val := Equiv.Perm.cycleOf g x, property := hx } = c
⊢ False
Tactic:
apply hc
State after:
case neg.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
hc' : { val := Equiv.Perm.cycleOf g x, property := hx } = c
⊢ Equiv.Perm.cycleOf g x = ↑c

State before:
case neg.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∈ Equiv.Perm.cycleFactorsFinset g
hc : ¬Equiv.Perm.cycleOf g x = ↑c
hc' : { val := Equiv.Perm.cycleOf g x, property := hx } = c
⊢ Equiv.Perm.cycleOf g x = ↑c
Tactic:
rw [← hc']
State after:
no goals

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : Equiv.Perm.cycleOf g x ∉ Equiv.Perm.cycleFactorsFinset g
⊢ ((θ g) (1, Pi.mulSingle c vc)) x = ↑vc x
Tactic:
rw [Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff, Equiv.Perm.not_mem_support] at hx
State after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : g x = x
⊢ ((θ g) (1, Pi.mulSingle c vc)) x = ↑vc x

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : g x = x
⊢ ((θ g) (1, Pi.mulSingle c vc)) x = ↑vc x
Tactic:
rw [hθ_1 _ x hx]
State after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : g x = x
⊢ ↑((1, Pi.mulSingle c vc).1 { val := x, property := hx }) = ↑vc x

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : g x = x
⊢ ↑((1, Pi.mulSingle c vc).1 { val := x, property := hx }) = ↑vc x
Tactic:
dsimp only [Equiv.Perm.coe_one, id_eq]
State after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : g x = x
⊢ x = ↑vc x

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : g x = x
⊢ x = ↑vc x
Tactic:
obtain ⟨m, hm⟩ := vc.prop
State after:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : g x = x
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑vc
⊢ x = ↑vc x

State before:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : g x = x
m : ℤ
hm : (fun x => ↑c ^ x) m = ↑vc
⊢ x = ↑vc x
Tactic:
dsimp only at hm
State after:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : g x = x
m : ℤ
hm : ↑c ^ m = ↑vc
⊢ x = ↑vc x

State before:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : g x = x
m : ℤ
hm : ↑c ^ m = ↑vc
⊢ x = ↑vc x
Tactic:
rw [← hm]
State after:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : g x = x
m : ℤ
hm : ↑c ^ m = ↑vc
⊢ x = (↑c ^ m) x

State before:
case neg.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : g x = x
m : ℤ
hm : ↑c ^ m = ↑vc
⊢ x = (↑c ^ m) x
Tactic:
apply symm
State after:
case neg.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : g x = x
m : ℤ
hm : ↑c ^ m = ↑vc
⊢ (↑c ^ m) x = x

State before:
case neg.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : g x = x
m : ℤ
hm : ↑c ^ m = ↑vc
⊢ (↑c ^ m) x = x
Tactic:
rw [← Equiv.Perm.not_mem_support] at hx ⊢
State after:
case neg.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : x ∉ Equiv.Perm.support g
m : ℤ
hm : ↑c ^ m = ↑vc
⊢ x ∉ Equiv.Perm.support (↑c ^ m)

State before:
case neg.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : x ∉ Equiv.Perm.support g
m : ℤ
hm : ↑c ^ m = ↑vc
⊢ x ∉ Equiv.Perm.support (↑c ^ m)
Tactic:
intro hx'
State after:
case neg.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : x ∉ Equiv.Perm.support g
m : ℤ
hm : ↑c ^ m = ↑vc
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
⊢ False

State before:
case neg.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : x ∉ Equiv.Perm.support g
m : ℤ
hm : ↑c ^ m = ↑vc
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
⊢ False
Tactic:
apply hx
State after:
case neg.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : x ∉ Equiv.Perm.support g
m : ℤ
hm : ↑c ^ m = ↑vc
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
⊢ x ∈ Equiv.Perm.support g

State before:
case neg.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : x ∉ Equiv.Perm.support g
m : ℤ
hm : ↑c ^ m = ↑vc
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
⊢ x ∈ Equiv.Perm.support g
Tactic:
apply Equiv.Perm.mem_cycleFactorsFinset_support_le c.prop
State after:
case neg.intro.a.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : x ∉ Equiv.Perm.support g
m : ℤ
hm : ↑c ^ m = ↑vc
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
⊢ x ∈ Equiv.Perm.support ↑c

State before:
case neg.intro.a.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : x ∉ Equiv.Perm.support g
m : ℤ
hm : ↑c ^ m = ↑vc
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
⊢ x ∈ Equiv.Perm.support ↑c
Tactic:
apply Equiv.Perm.support_zpow_le _ _ hx'
State after:
no goals