internlm/Lean-Github huggingface dataset:
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
case inl.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
d : Equiv.Perm α
hd : d ∈ Equiv.Perm.cycleFactorsFinset g
hm : (Equiv.Perm.support c).card = (Equiv.Perm.support d).card
hm' : c ≠ d
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g } :=
  Equiv.swap { val := c, property := hc } { val := d, property := hd }
a : Equiv.Perm.Basis g
hτ : τ ∈ Iφ g
k : Equiv.Perm α := ConjAct.ofConjAct ↑((φ' a) { val := τ, property := hτ })
hk2 : ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), ConjAct.toConjAct k • ↑c = ↑(τ c)
hksup : Equiv.Perm.support k ≤ Equiv.Perm.support g
hk_apply :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) (m n : ℕ), (k ^ m) ((g ^ n) (a c)) = (g ^ n) (a ((τ ^ m) c))
this : Equiv.Perm.cycleType k = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType k)) 2
this' : Multiset.card (Equiv.Perm.cycleType k) * 2 = (Equiv.Perm.support k).card
x : α
hx : x ∈ Equiv.Perm.support k
cx : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hcx : ∀ y ∈ Equiv.Perm.support ↑cx, Equiv.Perm.SameCycle g y x
hxcx : x ∈ Equiv.Perm.support ↑cx
hccx : c = ↑cx
⊢ x ∈ Equiv.Perm.support c
Tactic:
rw [hccx]
Proof state after:
case inl.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
d : Equiv.Perm α
hd : d ∈ Equiv.Perm.cycleFactorsFinset g
hm : (Equiv.Perm.support c).card = (Equiv.Perm.support d).card
hm' : c ≠ d
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g } :=
  Equiv.swap { val := c, property := hc } { val := d, property := hd }
a : Equiv.Perm.Basis g
hτ : τ ∈ Iφ g
k : Equiv.Perm α := ConjAct.ofConjAct ↑((φ' a) { val := τ, property := hτ })
hk2 : ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), ConjAct.toConjAct k • ↑c = ↑(τ c)
hksup : Equiv.Perm.support k ≤ Equiv.Perm.support g
hk_apply :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) (m n : ℕ), (k ^ m) ((g ^ n) (a c)) = (g ^ n) (a ((τ ^ m) c))
this : Equiv.Perm.cycleType k = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType k)) 2
this' : Multiset.card (Equiv.Perm.cycleType k) * 2 = (Equiv.Perm.support k).card
x : α
hx : x ∈ Equiv.Perm.support k
cx : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hcx : ∀ y ∈ Equiv.Perm.support ↑cx, Equiv.Perm.SameCycle g y x
hxcx : x ∈ Equiv.Perm.support ↑cx
hccx : c = ↑cx
⊢ x ∈ Equiv.Perm.support ↑cx
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
case inl.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
d : Equiv.Perm α
hd : d ∈ Equiv.Perm.cycleFactorsFinset g
hm : (Equiv.Perm.support c).card = (Equiv.Perm.support d).card
hm' : c ≠ d
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g } :=
  Equiv.swap { val := c, property := hc } { val := d, property := hd }
a : Equiv.Perm.Basis g
hτ : τ ∈ Iφ g
k : Equiv.Perm α := ConjAct.ofConjAct ↑((φ' a) { val := τ, property := hτ })
hk2 : ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), ConjAct.toConjAct k • ↑c = ↑(τ c)
hksup : Equiv.Perm.support k ≤ Equiv.Perm.support g
hk_apply :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) (m n : ℕ), (k ^ m) ((g ^ n) (a c)) = (g ^ n) (a ((τ ^ m) c))
this : Equiv.Perm.cycleType k = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType k)) 2
this' : Multiset.card (Equiv.Perm.cycleType k) * 2 = (Equiv.Perm.support k).card
x : α
hx : x ∈ Equiv.Perm.support k
cx : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hcx : ∀ y ∈ Equiv.Perm.support ↑cx, Equiv.Perm.SameCycle g y x
hxcx : x ∈ Equiv.Perm.support ↑cx
hccx : c = ↑cx
⊢ x ∈ Equiv.Perm.support ↑cx
Tactic:
exact hxcx
Proof state after:
no goals
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
d : Equiv.Perm α
hd : d ∈ Equiv.Perm.cycleFactorsFinset g
hm : (Equiv.Perm.support c).card = (Equiv.Perm.support d).card
hm' : c ≠ d
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g } :=
  Equiv.swap { val := c, property := hc } { val := d, property := hd }
a : Equiv.Perm.Basis g
hτ : τ ∈ Iφ g
k : Equiv.Perm α := ConjAct.ofConjAct ↑((φ' a) { val := τ, property := hτ })
hk2 : ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), ConjAct.toConjAct k • ↑c = ↑(τ c)
hksup : Equiv.Perm.support k ≤ Equiv.Perm.support g
hk_apply :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) (m n : ℕ), (k ^ m) ((g ^ n) (a c)) = (g ^ n) (a ((τ ^ m) c))
this : Equiv.Perm.cycleType k = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType k)) 2
this' : Multiset.card (Equiv.Perm.cycleType k) * 2 = (Equiv.Perm.support k).card
x : α
hx : x ∈ Equiv.Perm.support k
cx : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hcx : ∀ y ∈ Equiv.Perm.support ↑cx, Equiv.Perm.SameCycle g y x
hxcx : x ∈ Equiv.Perm.support ↑cx
hdcx : d = ↑cx
⊢ x ∈ Equiv.Perm.support c ∨ x ∈ Equiv.Perm.support d
Tactic:
apply Or.intro_right
Proof state after:
case inr.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
d : Equiv.Perm α
hd : d ∈ Equiv.Perm.cycleFactorsFinset g
hm : (Equiv.Perm.support c).card = (Equiv.Perm.support d).card
hm' : c ≠ d
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g } :=
  Equiv.swap { val := c, property := hc } { val := d, property := hd }
a : Equiv.Perm.Basis g
hτ : τ ∈ Iφ g
k : Equiv.Perm α := ConjAct.ofConjAct ↑((φ' a) { val := τ, property := hτ })
hk2 : ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), ConjAct.toConjAct k • ↑c = ↑(τ c)
hksup : Equiv.Perm.support k ≤ Equiv.Perm.support g
hk_apply :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) (m n : ℕ), (k ^ m) ((g ^ n) (a c)) = (g ^ n) (a ((τ ^ m) c))
this : Equiv.Perm.cycleType k = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType k)) 2
this' : Multiset.card (Equiv.Perm.cycleType k) * 2 = (Equiv.Perm.support k).card
x : α
hx : x ∈ Equiv.Perm.support k
cx : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hcx : ∀ y ∈ Equiv.Perm.support ↑cx, Equiv.Perm.SameCycle g y x
hxcx : x ∈ Equiv.Perm.support ↑cx
hdcx : d = ↑cx
⊢ x ∈ Equiv.Perm.support d
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
case inr.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
d : Equiv.Perm α
hd : d ∈ Equiv.Perm.cycleFactorsFinset g
hm : (Equiv.Perm.support c).card = (Equiv.Perm.support d).card
hm' : c ≠ d
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g } :=
  Equiv.swap { val := c, property := hc } { val := d, property := hd }
a : Equiv.Perm.Basis g
hτ : τ ∈ Iφ g
k : Equiv.Perm α := ConjAct.ofConjAct ↑((φ' a) { val := τ, property := hτ })
hk2 : ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), ConjAct.toConjAct k • ↑c = ↑(τ c)
hksup : Equiv.Perm.support k ≤ Equiv.Perm.support g
hk_apply :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) (m n : ℕ), (k ^ m) ((g ^ n) (a c)) = (g ^ n) (a ((τ ^ m) c))
this : Equiv.Perm.cycleType k = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType k)) 2
this' : Multiset.card (Equiv.Perm.cycleType k) * 2 = (Equiv.Perm.support k).card
x : α
hx : x ∈ Equiv.Perm.support k
cx : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hcx : ∀ y ∈ Equiv.Perm.support ↑cx, Equiv.Perm.SameCycle g y x
hxcx : x ∈ Equiv.Perm.support ↑cx
hdcx : d = ↑cx
⊢ x ∈ Equiv.Perm.support d
Tactic:
rw [hdcx]
Proof state after:
case inr.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
d : Equiv.Perm α
hd : d ∈ Equiv.Perm.cycleFactorsFinset g
hm : (Equiv.Perm.support c).card = (Equiv.Perm.support d).card
hm' : c ≠ d
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g } :=
  Equiv.swap { val := c, property := hc } { val := d, property := hd }
a : Equiv.Perm.Basis g
hτ : τ ∈ Iφ g
k : Equiv.Perm α := ConjAct.ofConjAct ↑((φ' a) { val := τ, property := hτ })
hk2 : ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), ConjAct.toConjAct k • ↑c = ↑(τ c)
hksup : Equiv.Perm.support k ≤ Equiv.Perm.support g
hk_apply :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) (m n : ℕ), (k ^ m) ((g ^ n) (a c)) = (g ^ n) (a ((τ ^ m) c))
this : Equiv.Perm.cycleType k = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType k)) 2
this' : Multiset.card (Equiv.Perm.cycleType k) * 2 = (Equiv.Perm.support k).card
x : α
hx : x ∈ Equiv.Perm.support k
cx : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hcx : ∀ y ∈ Equiv.Perm.support ↑cx, Equiv.Perm.SameCycle g y x
hxcx : x ∈ Equiv.Perm.support ↑cx
hdcx : d = ↑cx
⊢ x ∈ Equiv.Perm.support ↑cx
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
case inr.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
d : Equiv.Perm α
hd : d ∈ Equiv.Perm.cycleFactorsFinset g
hm : (Equiv.Perm.support c).card = (Equiv.Perm.support d).card
hm' : c ≠ d
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g } :=
  Equiv.swap { val := c, property := hc } { val := d, property := hd }
a : Equiv.Perm.Basis g
hτ : τ ∈ Iφ g
k : Equiv.Perm α := ConjAct.ofConjAct ↑((φ' a) { val := τ, property := hτ })
hk2 : ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), ConjAct.toConjAct k • ↑c = ↑(τ c)
hksup : Equiv.Perm.support k ≤ Equiv.Perm.support g
hk_apply :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) (m n : ℕ), (k ^ m) ((g ^ n) (a c)) = (g ^ n) (a ((τ ^ m) c))
this : Equiv.Perm.cycleType k = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType k)) 2
this' : Multiset.card (Equiv.Perm.cycleType k) * 2 = (Equiv.Perm.support k).card
x : α
hx : x ∈ Equiv.Perm.support k
cx : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hcx : ∀ y ∈ Equiv.Perm.support ↑cx, Equiv.Perm.SameCycle g y x
hxcx : x ∈ Equiv.Perm.support ↑cx
hdcx : d = ↑cx
⊢ x ∈ Equiv.Perm.support ↑cx
Tactic:
exact hxcx
Proof state after:
no goals
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
case a.mp.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
d : Equiv.Perm α
hd : d ∈ Equiv.Perm.cycleFactorsFinset g
hm : (Equiv.Perm.support c).card = (Equiv.Perm.support d).card
hm' : c ≠ d
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g } :=
  Equiv.swap { val := c, property := hc } { val := d, property := hd }
a : Equiv.Perm.Basis g
hτ : τ ∈ Iφ g
k : Equiv.Perm α := ConjAct.ofConjAct ↑((φ' a) { val := τ, property := hτ })
hk2 : ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), ConjAct.toConjAct k • ↑c = ↑(τ c)
hksup : Equiv.Perm.support k ≤ Equiv.Perm.support g
hk_apply :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) (m n : ℕ), (k ^ m) ((g ^ n) (a c)) = (g ^ n) (a ((τ ^ m) c))
this : Equiv.Perm.cycleType k = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType k)) 2
this' : Multiset.card (Equiv.Perm.cycleType k) * 2 = (Equiv.Perm.support k).card
x : α
hx : x ∈ Equiv.Perm.support k
cx : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hcx : ∀ y ∈ Equiv.Perm.support ↑cx, Equiv.Perm.SameCycle g y x
hxcx : x ∈ Equiv.Perm.support ↑cx
⊢ c = ↑cx ∨ d = ↑cx
Tactic:
obtain ⟨n, _, hnx⟩ := (hcx (a cx) (a.mem_support cx)).exists_pow_eq'
Proof state after:
case a.mp.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
d : Equiv.Perm α
hd : d ∈ Equiv.Perm.cycleFactorsFinset g
hm : (Equiv.Perm.support c).card = (Equiv.Perm.support d).card
hm' : c ≠ d
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g } :=
  Equiv.swap { val := c, property := hc } { val := d, property := hd }
a : Equiv.Perm.Basis g
hτ : τ ∈ Iφ g
k : Equiv.Perm α := ConjAct.ofConjAct ↑((φ' a) { val := τ, property := hτ })
hk2 : ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), ConjAct.toConjAct k • ↑c = ↑(τ c)
hksup : Equiv.Perm.support k ≤ Equiv.Perm.support g
hk_apply :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) (m n : ℕ), (k ^ m) ((g ^ n) (a c)) = (g ^ n) (a ((τ ^ m) c))
this : Equiv.Perm.cycleType k = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType k)) 2
this' : Multiset.card (Equiv.Perm.cycleType k) * 2 = (Equiv.Perm.support k).card
x : α
hx : x ∈ Equiv.Perm.support k
cx : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hcx : ∀ y ∈ Equiv.Perm.support ↑cx, Equiv.Perm.SameCycle g y x
hxcx : x ∈ Equiv.Perm.support ↑cx
n : ℕ
left✝ : n < orderOf g
hnx : (g ^ n) (a cx) = x
⊢ c = ↑cx ∨ d = ↑cx
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
case a.mp.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
d : Equiv.Perm α
hd : d ∈ Equiv.Perm.cycleFactorsFinset g
hm : (Equiv.Perm.support c).card = (Equiv.Perm.support d).card
hm' : c ≠ d
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g } :=
  Equiv.swap { val := c, property := hc } { val := d, property := hd }
a : Equiv.Perm.Basis g
hτ : τ ∈ Iφ g
k : Equiv.Perm α := ConjAct.ofConjAct ↑((φ' a) { val := τ, property := hτ })
hk2 : ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), ConjAct.toConjAct k • ↑c = ↑(τ c)
hksup : Equiv.Perm.support k ≤ Equiv.Perm.support g
hk_apply :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) (m n : ℕ), (k ^ m) ((g ^ n) (a c)) = (g ^ n) (a ((τ ^ m) c))
this : Equiv.Perm.cycleType k = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType k)) 2
this' : Multiset.card (Equiv.Perm.cycleType k) * 2 = (Equiv.Perm.support k).card
x : α
hx : x ∈ Equiv.Perm.support k
cx : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hcx : ∀ y ∈ Equiv.Perm.support ↑cx, Equiv.Perm.SameCycle g y x
hxcx : x ∈ Equiv.Perm.support ↑cx
n : ℕ
left✝ : n < orderOf g
hnx : (g ^ n) (a cx) = x
⊢ c = ↑cx ∨ d = ↑cx
Tactic:
rw [Equiv.Perm.mem_support, ← hnx] at hx
Proof state after:
case a.mp.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
d : Equiv.Perm α
hd : d ∈ Equiv.Perm.cycleFactorsFinset g
hm : (Equiv.Perm.support c).card = (Equiv.Perm.support d).card
hm' : c ≠ d
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g } :=
  Equiv.swap { val := c, property := hc } { val := d, property := hd }
a : Equiv.Perm.Basis g
hτ : τ ∈ Iφ g
k : Equiv.Perm α := ConjAct.ofConjAct ↑((φ' a) { val := τ, property := hτ })
hk2 : ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), ConjAct.toConjAct k • ↑c = ↑(τ c)
hksup : Equiv.Perm.support k ≤ Equiv.Perm.support g
hk_apply :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) (m n : ℕ), (k ^ m) ((g ^ n) (a c)) = (g ^ n) (a ((τ ^ m) c))
this : Equiv.Perm.cycleType k = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType k)) 2
this' : Multiset.card (Equiv.Perm.cycleType k) * 2 = (Equiv.Perm.support k).card
x : α
cx : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hcx : ∀ y ∈ Equiv.Perm.support ↑cx, Equiv.Perm.SameCycle g y x
hxcx : x ∈ Equiv.Perm.support ↑cx
n : ℕ
hx : k ((g ^ n) (a cx)) ≠ (g ^ n) (a cx)
left✝ : n < orderOf g
hnx : (g ^ n) (a cx) = x
⊢ c = ↑cx ∨ d = ↑cx
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
case a.mp.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
d : Equiv.Perm α
hd : d ∈ Equiv.Perm.cycleFactorsFinset g
hm : (Equiv.Perm.support c).card = (Equiv.Perm.support d).card
hm' : c ≠ d
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g } :=
  Equiv.swap { val := c, property := hc } { val := d, property := hd }
a : Equiv.Perm.Basis g
hτ : τ ∈ Iφ g
k : Equiv.Perm α := ConjAct.ofConjAct ↑((φ' a) { val := τ, property := hτ })
hk2 : ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), ConjAct.toConjAct k • ↑c = ↑(τ c)
hksup : Equiv.Perm.support k ≤ Equiv.Perm.support g
hk_apply :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) (m n : ℕ), (k ^ m) ((g ^ n) (a c)) = (g ^ n) (a ((τ ^ m) c))
this : Equiv.Perm.cycleType k = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType k)) 2
this' : Multiset.card (Equiv.Perm.cycleType k) * 2 = (Equiv.Perm.support k).card
x : α
cx : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hcx : ∀ y ∈ Equiv.Perm.support ↑cx, Equiv.Perm.SameCycle g y x
hxcx : x ∈ Equiv.Perm.support ↑cx
n : ℕ
hx : k ((g ^ n) (a cx)) ≠ (g ^ n) (a cx)
left✝ : n < orderOf g
hnx : (g ^ n) (a cx) = x
⊢ c = ↑cx ∨ d = ↑cx
Tactic:
specialize hk_apply cx 1
Proof state after:
case a.mp.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
d : Equiv.Perm α
hd : d ∈ Equiv.Perm.cycleFactorsFinset g
hm : (Equiv.Perm.support c).card = (Equiv.Perm.support d).card
hm' : c ≠ d
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g } :=
  Equiv.swap { val := c, property := hc } { val := d, property := hd }
a : Equiv.Perm.Basis g
hτ : τ ∈ Iφ g
k : Equiv.Perm α := ConjAct.ofConjAct ↑((φ' a) { val := τ, property := hτ })
hk2 : ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), ConjAct.toConjAct k • ↑c = ↑(τ c)
hksup : Equiv.Perm.support k ≤ Equiv.Perm.support g
this : Equiv.Perm.cycleType k = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType k)) 2
this' : Multiset.card (Equiv.Perm.cycleType k) * 2 = (Equiv.Perm.support k).card
x : α
cx : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hcx : ∀ y ∈ Equiv.Perm.support ↑cx, Equiv.Perm.SameCycle g y x
hxcx : x ∈ Equiv.Perm.support ↑cx
n : ℕ
hx : k ((g ^ n) (a cx)) ≠ (g ^ n) (a cx)
left✝ : n < orderOf g
hnx : (g ^ n) (a cx) = x
hk_apply : ∀ (n : ℕ), (k ^ 1) ((g ^ n) (a cx)) = (g ^ n) (a ((τ ^ 1) cx))
⊢ c = ↑cx ∨ d = ↑cx
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
case a.mp.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
d : Equiv.Perm α
hd : d ∈ Equiv.Perm.cycleFactorsFinset g
hm : (Equiv.Perm.support c).card = (Equiv.Perm.support d).card
hm' : c ≠ d
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g } :=
  Equiv.swap { val := c, property := hc } { val := d, property := hd }
a : Equiv.Perm.Basis g
hτ : τ ∈ Iφ g
k : Equiv.Perm α := ConjAct.ofConjAct ↑((φ' a) { val := τ, property := hτ })
hk2 : ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), ConjAct.toConjAct k • ↑c = ↑(τ c)
hksup : Equiv.Perm.support k ≤ Equiv.Perm.support g
this : Equiv.Perm.cycleType k = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType k)) 2
this' : Multiset.card (Equiv.Perm.cycleType k) * 2 = (Equiv.Perm.support k).card
x : α
cx : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hcx : ∀ y ∈ Equiv.Perm.support ↑cx, Equiv.Perm.SameCycle g y x
hxcx : x ∈ Equiv.Perm.support ↑cx
n : ℕ
hx : k ((g ^ n) (a cx)) ≠ (g ^ n) (a cx)
left✝ : n < orderOf g
hnx : (g ^ n) (a cx) = x
hk_apply : ∀ (n : ℕ), (k ^ 1) ((g ^ n) (a cx)) = (g ^ n) (a ((τ ^ 1) cx))
⊢ c = ↑cx ∨ d = ↑cx
Tactic:
simp only [pow_one] at hk_apply
Proof state after:
case a.mp.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
d : Equiv.Perm α
hd : d ∈ Equiv.Perm.cycleFactorsFinset g
hm : (Equiv.Perm.support c).card = (Equiv.Perm.support d).card
hm' : c ≠ d
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g } :=
  Equiv.swap { val := c, property := hc } { val := d, property := hd }
a : Equiv.Perm.Basis g
hτ : τ ∈ Iφ g
k : Equiv.Perm α := ConjAct.ofConjAct ↑((φ' a) { val := τ, property := hτ })
hk2 : ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), ConjAct.toConjAct k • ↑c = ↑(τ c)
hksup : Equiv.Perm.support k ≤ Equiv.Perm.support g
this : Equiv.Perm.cycleType k = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType k)) 2
this' : Multiset.card (Equiv.Perm.cycleType k) * 2 = (Equiv.Perm.support k).card
x : α
cx : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hcx : ∀ y ∈ Equiv.Perm.support ↑cx, Equiv.Perm.SameCycle g y x
hxcx : x ∈ Equiv.Perm.support ↑cx
n : ℕ
hx : k ((g ^ n) (a cx)) ≠ (g ^ n) (a cx)
left✝ : n < orderOf g
hnx : (g ^ n) (a cx) = x
hk_apply : ∀ (n : ℕ), k ((g ^ n) (a cx)) = (g ^ n) (a (τ cx))
⊢ c = ↑cx ∨ d = ↑cx
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
case a.mp.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
d : Equiv.Perm α
hd : d ∈ Equiv.Perm.cycleFactorsFinset g
hm : (Equiv.Perm.support c).card = (Equiv.Perm.support d).card
hm' : c ≠ d
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g } :=
  Equiv.swap { val := c, property := hc } { val := d, property := hd }
a : Equiv.Perm.Basis g
hτ : τ ∈ Iφ g
k : Equiv.Perm α := ConjAct.ofConjAct ↑((φ' a) { val := τ, property := hτ })
hk2 : ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), ConjAct.toConjAct k • ↑c = ↑(τ c)
hksup : Equiv.Perm.support k ≤ Equiv.Perm.support g
this : Equiv.Perm.cycleType k = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType k)) 2
this' : Multiset.card (Equiv.Perm.cycleType k) * 2 = (Equiv.Perm.support k).card
x : α
cx : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hcx : ∀ y ∈ Equiv.Perm.support ↑cx, Equiv.Perm.SameCycle g y x
hxcx : x ∈ Equiv.Perm.support ↑cx
n : ℕ
hx : k ((g ^ n) (a cx)) ≠ (g ^ n) (a cx)
left✝ : n < orderOf g
hnx : (g ^ n) (a cx) = x
hk_apply : ∀ (n : ℕ), k ((g ^ n) (a cx)) = (g ^ n) (a (τ cx))
⊢ c = ↑cx ∨ d = ↑cx
Tactic:
rw [hk_apply] at hx
Proof state after:
case a.mp.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
d : Equiv.Perm α
hd : d ∈ Equiv.Perm.cycleFactorsFinset g
hm : (Equiv.Perm.support c).card = (Equiv.Perm.support d).card
hm' : c ≠ d
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g } :=
  Equiv.swap { val := c, property := hc } { val := d, property := hd }
a : Equiv.Perm.Basis g
hτ : τ ∈ Iφ g
k : Equiv.Perm α := ConjAct.ofConjAct ↑((φ' a) { val := τ, property := hτ })
hk2 : ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), ConjAct.toConjAct k • ↑c = ↑(τ c)
hksup : Equiv.Perm.support k ≤ Equiv.Perm.support g
this : Equiv.Perm.cycleType k = Multiset.replicate (Multiset.card (Equiv.Perm.cycleType k)) 2
this' : Multiset.card (Equiv.Perm.cycleType k) * 2 = (Equiv.Perm.support k).card
x : α
cx : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hcx : ∀ y ∈ Equiv.Perm.support ↑cx, Equiv.Perm.SameCycle g y x
hxcx : x ∈ Equiv.Perm.support ↑cx
n : ℕ
hx : (g ^ n) (a (τ cx)) ≠ (g ^ n) (a cx)
left✝ : n < orderOf g
hnx : (g ^ n) (a cx) = x
hk_apply : ∀ (n : ℕ), k ((g ^ n) (a cx)) = (g ^ n) (a (τ cx))
⊢ c = ↑cx ∨ d = ↑cx