internlm/Lean-Github huggingface dataset:
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
α : 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 (Equiv.Perm.support c).card 2
⊢ Equiv.Perm.sign k = -1
Tactic:
rw [Equiv.Perm.sign_of_cycleType]
Proof state after:
α : 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 (Equiv.Perm.support c).card 2
⊢ (-1) ^ (Multiset.sum (Equiv.Perm.cycleType k) + Multiset.card (Equiv.Perm.cycleType k)) = -1
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
α : 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 (Equiv.Perm.support c).card 2
⊢ (-1) ^ (Multiset.sum (Equiv.Perm.cycleType k) + Multiset.card (Equiv.Perm.cycleType k)) = -1
Tactic:
rw [this]
Proof state after:
α : 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 (Equiv.Perm.support c).card 2
⊢ (-1) ^
      (Multiset.sum (Multiset.replicate (Equiv.Perm.support c).card 2) +
        Multiset.card (Multiset.replicate (Equiv.Perm.support c).card 2)) =
    -1
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
α : 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 (Equiv.Perm.support c).card 2
⊢ (-1) ^
      (Multiset.sum (Multiset.replicate (Equiv.Perm.support c).card 2) +
        Multiset.card (Multiset.replicate (Equiv.Perm.support c).card 2)) =
    -1
Tactic:
simp only [Multiset.sum_replicate, Algebra.id.smul_eq_mul, Multiset.card_replicate]
Proof state after:
α : 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 (Equiv.Perm.support c).card 2
⊢ (-1) ^ ((Equiv.Perm.support c).card * 2 + (Equiv.Perm.support c).card) = -1
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
α : 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 (Equiv.Perm.support c).card 2
⊢ (-1) ^ ((Equiv.Perm.support c).card * 2 + (Equiv.Perm.support c).card) = -1
Tactic:
rw [Odd.neg_one_pow]
Proof state after:
α : 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 (Equiv.Perm.support c).card 2
⊢ Odd ((Equiv.Perm.support c).card * 2 + (Equiv.Perm.support c).card)
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
α : 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 (Equiv.Perm.support c).card 2
⊢ Odd ((Equiv.Perm.support c).card * 2 + (Equiv.Perm.support c).card)
Tactic:
rw [Nat.odd_add']
Proof state after:
α : 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 (Equiv.Perm.support c).card 2
⊢ Odd (Equiv.Perm.support c).card ↔ Even ((Equiv.Perm.support c).card * 2)
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
α : 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 (Equiv.Perm.support c).card 2
⊢ Odd (Equiv.Perm.support c).card ↔ Even ((Equiv.Perm.support c).card * 2)
Tactic:
simp only [odd_of_mem_kerφ h c.support.card
  (by rw [Equiv.Perm.cycleType_def, Multiset.mem_map]
      exact ⟨c, hc, rfl⟩),
  true_iff_iff]
Proof state after:
α : 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 (Equiv.Perm.support c).card 2
⊢ Even ((Equiv.Perm.support c).card * 2)
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
α : 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 (Equiv.Perm.support c).card 2
⊢ Even ((Equiv.Perm.support c).card * 2)
Tactic:
rw [mul_comm]
Proof state after:
α : 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 (Equiv.Perm.support c).card 2
⊢ Even (2 * (Equiv.Perm.support c).card)
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
α : 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 (Equiv.Perm.support c).card 2
⊢ Even (2 * (Equiv.Perm.support c).card)
Tactic:
apply even_two_mul
Proof state after:
no goals
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
α : 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 (Equiv.Perm.support c).card 2
⊢ (Equiv.Perm.support c).card ∈ Equiv.Perm.cycleType g
Tactic:
rw [Equiv.Perm.cycleType_def, Multiset.mem_map]
Proof state after:
α : 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 (Equiv.Perm.support c).card 2
⊢ ∃ a ∈ (Equiv.Perm.cycleFactorsFinset g).val, (Finset.card ∘ Equiv.Perm.support) a = (Equiv.Perm.support c).card
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
α : 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 (Equiv.Perm.support c).card 2
⊢ ∃ a ∈ (Equiv.Perm.cycleFactorsFinset g).val, (Finset.card ∘ Equiv.Perm.support) a = (Equiv.Perm.support c).card
Tactic:
exact ⟨c, hc, rfl⟩
Proof state after:
no goals
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
α : 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
⊢ ∀ (m n : ℕ), Commute (k ^ m) (g ^ n)
Tactic:
apply Commute.pow_pow
Proof state after:
case 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
⊢ Commute k g
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
case 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
⊢ Commute k g
Tactic:
rw [Commute, SemiconjBy, ← mul_inv_eq_iff_eq_mul]
Proof state after:
case 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
⊢ k * g * k⁻¹ = g
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
case 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
⊢ k * g * k⁻¹ = g
Tactic:
exact (OnCycleFactors.φ' a ⟨τ, hτ⟩).prop
Proof state after:
no goals
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
α : 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 : ∀ (m n : ℕ), Commute (k ^ m) (g ^ n)
⊢ ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) (m n : ℕ), (k ^ m) ((g ^ n) (a c)) = (g ^ n) (a ((τ ^ m) c))
Tactic:
intro c m n
Proof state after:
α : 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 : ∀ (m n : ℕ), Commute (k ^ m) (g ^ n)
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
m n : ℕ
⊢ (k ^ m) ((g ^ n) (a c)) = (g ^ n) (a ((τ ^ m) c))