internlm/Lean-Github huggingface dataset:
Theorem: OnCycleFactors.θ_apply_single
Proof 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]
Proof 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
Theorem: OnCycleFactors.θ_apply_single
Proof 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
Proof 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
Theorem: OnCycleFactors.θ_apply_single
Proof 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
Proof 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
Theorem: OnCycleFactors.θ_apply_single
Proof 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
Proof 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
Theorem: OnCycleFactors.θ_apply_single
Proof 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]
Proof 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
Theorem: OnCycleFactors.θ_apply_single
Proof 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'
Proof 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
Theorem: OnCycleFactors.θ_apply_single
Proof 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
Proof 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
Theorem: OnCycleFactors.θ_apply_single
Proof 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
Proof 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
Theorem: OnCycleFactors.θ_apply_single
Proof 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
Proof 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
Theorem: OnCycleFactors.θ_apply_single
Proof 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'
Proof 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
Theorem: OnCycleFactors.θ_apply_single
Proof 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
Proof 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
Theorem: OnCycleFactors.θ_apply_single
Proof 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'
Proof 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
Theorem: OnCycleFactors.θ_apply_single
Proof 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
Proof 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
Theorem: OnCycleFactors.θ_apply_single
Proof 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']
Proof state after:
no goals
Theorem: OnCycleFactors.θ_apply_single
Proof 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
Proof 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
Theorem: OnCycleFactors.θ_apply_single
Proof 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]
Proof 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
Theorem: OnCycleFactors.θ_apply_single
Proof 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]
Proof 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
Theorem: OnCycleFactors.θ_apply_single
Proof 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
Proof 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
Theorem: OnCycleFactors.θ_apply_single
Proof 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
Proof 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
Theorem: OnCycleFactors.θ_apply_single
Proof 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]
Proof 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
Theorem: OnCycleFactors.θ_apply_single
Proof 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
Proof 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
Theorem: OnCycleFactors.θ_apply_single
Proof 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 ⊢
Proof 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)
Theorem: OnCycleFactors.θ_apply_single
Proof 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'
Proof 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
Theorem: OnCycleFactors.θ_apply_single
Proof 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
Proof 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
Theorem: OnCycleFactors.θ_apply_single
Proof 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
Proof 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