internlm/Lean-Github huggingface dataset:
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof state before:
case h.e'_2.h.e'_6.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
⊢ ∀ x ∈ Finset.univ, Equiv.Perm.sign ↑(uv x) = 1
Tactic:
rintro ⟨c, hc⟩ _
Proof state after:
case h.e'_2.h.e'_6.h.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
⊢ Equiv.Perm.sign ↑(uv { val := c, property := hc }) = 1
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof state before:
case h.e'_2.h.e'_6.h.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
⊢ Equiv.Perm.sign ↑(uv { val := c, property := hc }) = 1
Tactic:
obtain ⟨k, hk⟩ := (uv _).prop
Proof state after:
case h.e'_2.h.e'_6.h.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑?m.575606 ^ x) k = ↑(uv ?m.575606)
⊢ Equiv.Perm.sign ↑(uv { val := c, property := hc }) = 1
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof state before:
case h.e'_2.h.e'_6.h.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑?m.575606 ^ x) k = ↑(uv ?m.575606)
⊢ Equiv.Perm.sign ↑(uv { val := c, property := hc }) = 1
Tactic:
rw [← hk, map_zpow]
Proof state after:
case h.e'_2.h.e'_6.h.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ Equiv.Perm.sign ↑{ val := c, property := hc } ^ k = 1
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof state before:
case h.e'_2.h.e'_6.h.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ Equiv.Perm.sign ↑{ val := c, property := hc } ^ k = 1
Tactic:
convert one_zpow k
Proof state after:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ Equiv.Perm.sign ↑{ val := c, property := hc } = 1
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof state before:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ Equiv.Perm.sign ↑{ val := c, property := hc } = 1
Tactic:
simp only
Proof state after:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ Equiv.Perm.sign c = 1
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof state before:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ Equiv.Perm.sign c = 1
Tactic:
rw [Equiv.Perm.IsCycle.sign, Odd.neg_one_pow, neg_neg]
Proof state after:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ Odd (Equiv.Perm.support c).card

case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ Equiv.Perm.IsCycle c
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof state before:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ Odd (Equiv.Perm.support c).card

case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ Equiv.Perm.IsCycle c
Tactic:
apply h_odd
Proof state after:
case h.e'_2.h.e'_5.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ (Equiv.Perm.support c).card ∈ Equiv.Perm.cycleType g

case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ Equiv.Perm.IsCycle c
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof state before:
case h.e'_2.h.e'_5.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ (Equiv.Perm.support c).card ∈ Equiv.Perm.cycleType g

case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ Equiv.Perm.IsCycle c
Tactic:
rw [Equiv.Perm.cycleType_def, Multiset.mem_map]
Proof state after:
case h.e'_2.h.e'_5.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ ∃ a ∈ (Equiv.Perm.cycleFactorsFinset g).val, (Finset.card ∘ Equiv.Perm.support) a = (Equiv.Perm.support c).card

case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ Equiv.Perm.IsCycle c
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof state before:
case h.e'_2.h.e'_5.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ ∃ a ∈ (Equiv.Perm.cycleFactorsFinset g).val, (Finset.card ∘ Equiv.Perm.support) a = (Equiv.Perm.support c).card

case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ Equiv.Perm.IsCycle c
Tactic:
use c
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ c ∈ (Equiv.Perm.cycleFactorsFinset g).val ∧ (Finset.card ∘ Equiv.Perm.support) c = (Equiv.Perm.support c).card

case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ Equiv.Perm.IsCycle c
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof state before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ c ∈ (Equiv.Perm.cycleFactorsFinset g).val ∧ (Finset.card ∘ Equiv.Perm.support) c = (Equiv.Perm.support c).card

case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ Equiv.Perm.IsCycle c
Tactic:
exact ⟨hc, rfl⟩
Proof state after:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ Equiv.Perm.IsCycle c
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof state before:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
a✝ : { val := c, property := hc } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc } ^ x) k = ↑(uv { val := c, property := hc })
⊢ Equiv.Perm.IsCycle c
Tactic:
rw [Equiv.Perm.mem_cycleFactorsFinset_iff] at hc
Proof state after:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc✝ : c ∈ Equiv.Perm.cycleFactorsFinset g
hc : Equiv.Perm.IsCycle c ∧ ∀ a ∈ Equiv.Perm.support c, c a = g a
a✝ : { val := c, property := hc✝ } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc✝ } ^ x) k = ↑(uv { val := c, property := hc✝ })
⊢ Equiv.Perm.IsCycle c
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof state before:
case h.e'_2.h.e'_5
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h_odd : ∀ i ∈ Equiv.Perm.cycleType g, Odd i
h_fixed : Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1
h_count : ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
y : Equiv.Perm ↑(Function.fixedPoints ⇑g)
uv : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
hx : (θ g) (y, uv) ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
hx' : (θ g) (y, uv) ∈ Set.range ⇑(θ g)
c : Equiv.Perm α
hc✝ : c ∈ Equiv.Perm.cycleFactorsFinset g
hc : Equiv.Perm.IsCycle c ∧ ∀ a ∈ Equiv.Perm.support c, c a = g a
a✝ : { val := c, property := hc✝ } ∈ Finset.univ
k : ℤ
hk : (fun x => ↑{ val := c, property := hc✝ } ^ x) k = ↑(uv { val := c, property := hc✝ })
⊢ Equiv.Perm.IsCycle c
Tactic:
exact hc.left
Proof state after:
no goals