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