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 : ∀ (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:
simp only [Commute, SemiconjBy] at 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 : ∀ (m n : ℕ), k ^ m * g ^ n = g ^ n * k ^ m
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
m n : ℕ
⊢ (k ^ m) ((g ^ n) (a c)) = (g ^ n) (a ((τ ^ m) c))
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 : ℕ), k ^ m * g ^ n = g ^ n * k ^ m
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
m n : ℕ
⊢ (k ^ m) ((g ^ n) (a c)) = (g ^ n) (a ((τ ^ m) c))
Tactic:
rw [← Equiv.Perm.mul_apply, this, Equiv.Perm.mul_apply, EmbeddingLike.apply_eq_iff_eq]
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 : ℕ), k ^ m * g ^ n = g ^ n * k ^ m
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
m n : ℕ
⊢ (k ^ m) (a c) = a ((τ ^ m) c)
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 : ℕ), k ^ m * g ^ n = g ^ n * k ^ m
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
m n : ℕ
⊢ (k ^ m) (a c) = a ((τ ^ m) c)
Tactic:
induction' m with m hrec
Proof state after:
case zero
α : 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 : ℕ), k ^ m * g ^ n = g ^ n * k ^ m
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
n : ℕ
⊢ (k ^ Nat.zero) (a c) = a ((τ ^ Nat.zero) c)

case succ
α : 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 : ℕ), k ^ m * g ^ n = g ^ n * k ^ m
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
n m : ℕ
hrec : (k ^ m) (a c) = a ((τ ^ m) c)
⊢ (k ^ Nat.succ m) (a c) = a ((τ ^ Nat.succ m) c)
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
case zero
α : 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 : ℕ), k ^ m * g ^ n = g ^ n * k ^ m
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
n : ℕ
⊢ (k ^ Nat.zero) (a c) = a ((τ ^ Nat.zero) c)
Tactic:
simp only [pow_zero, Equiv.Perm.coe_one, id.def]
Proof state after:
no goals
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
case succ
α : 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 : ℕ), k ^ m * g ^ n = g ^ n * k ^ m
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
n m : ℕ
hrec : (k ^ m) (a c) = a ((τ ^ m) c)
⊢ (k ^ Nat.succ m) (a c) = a ((τ ^ Nat.succ m) c)
Tactic:
rw [pow_succ', Equiv.Perm.mul_apply]
Proof state after:
case succ
α : 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 : ℕ), k ^ m * g ^ n = g ^ n * k ^ m
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
n m : ℕ
hrec : (k ^ m) (a c) = a ((τ ^ m) c)
⊢ k ((k ^ m) (a c)) = a ((τ ^ Nat.succ m) c)
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
case succ
α : 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 : ℕ), k ^ m * g ^ n = g ^ n * k ^ m
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
n m : ℕ
hrec : (k ^ m) (a c) = a ((τ ^ m) c)
⊢ k ((k ^ m) (a c)) = a ((τ ^ Nat.succ m) c)
Tactic:
rw [hrec]
Proof state after:
case succ
α : 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 : ℕ), k ^ m * g ^ n = g ^ n * k ^ m
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
n m : ℕ
hrec : (k ^ m) (a c) = a ((τ ^ m) c)
⊢ k (a ((τ ^ m) c)) = a ((τ ^ Nat.succ m) c)
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
case succ
α : 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 : ℕ), k ^ m * g ^ n = g ^ n * k ^ m
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
n m : ℕ
hrec : (k ^ m) (a c) = a ((τ ^ m) c)
⊢ k (a ((τ ^ m) c)) = a ((τ ^ Nat.succ m) c)
Tactic:
rw [OnCycleFactors.φ'_apply ⟨τ, hτ⟩]
Proof state after:
case succ
α : 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 : ℕ), k ^ m * g ^ n = g ^ n * k ^ m
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
n m : ℕ
hrec : (k ^ m) (a c) = a ((τ ^ m) c)
⊢ OnCycleFactors.k a (↑{ val := τ, property := hτ }) (a ((τ ^ m) c)) = a ((τ ^ Nat.succ m) c)
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
case succ
α : 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 : ℕ), k ^ m * g ^ n = g ^ n * k ^ m
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
n m : ℕ
hrec : (k ^ m) (a c) = a ((τ ^ m) c)
⊢ OnCycleFactors.k a (↑{ val := τ, property := hτ }) (a ((τ ^ m) c)) = a ((τ ^ Nat.succ m) c)
Tactic:
rw [OnCycleFactors.k_apply_base _ hτ]
Proof state after:
case succ
α : 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 : ℕ), k ^ m * g ^ n = g ^ n * k ^ m
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
n m : ℕ
hrec : (k ^ m) (a c) = a ((τ ^ m) c)
⊢ a (τ ((τ ^ m) c)) = a ((τ ^ Nat.succ m) c)
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
case succ
α : 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 : ℕ), k ^ m * g ^ n = g ^ n * k ^ m
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
n m : ℕ
hrec : (k ^ m) (a c) = a ((τ ^ m) c)
⊢ a (τ ((τ ^ m) c)) = a ((τ ^ Nat.succ m) c)
Tactic:
rw [pow_succ']
Proof state after:
case succ
α : 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 : ℕ), k ^ m * g ^ n = g ^ n * k ^ m
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
n m : ℕ
hrec : (k ^ m) (a c) = a ((τ ^ m) c)
⊢ a (τ ((τ ^ m) c)) = a ((τ * τ ^ m) c)
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
case succ
α : 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 : ℕ), k ^ m * g ^ n = g ^ n * k ^ m
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
n m : ℕ
hrec : (k ^ m) (a c) = a ((τ ^ m) c)
⊢ a (τ ((τ ^ m) c)) = a ((τ * τ ^ m) c)
Tactic:
rw [Equiv.Perm.coe_mul]
Proof state after:
case succ
α : 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 : ℕ), k ^ m * g ^ n = g ^ n * k ^ m
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
n m : ℕ
hrec : (k ^ m) (a c) = a ((τ ^ m) c)
⊢ a (τ ((τ ^ m) c)) = a ((⇑τ ∘ ⇑(τ ^ m)) c)
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
case succ
α : 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 : ℕ), k ^ m * g ^ n = g ^ n * k ^ m
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
n m : ℕ
hrec : (k ^ m) (a c) = a ((τ ^ m) c)
⊢ a (τ ((τ ^ m) c)) = a ((⇑τ ∘ ⇑(τ ^ m)) c)
Tactic:
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
hk_apply :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) (m n : ℕ), (k ^ m) ((g ^ n) (a c)) = (g ^ n) (a ((τ ^ m) c))
this : ∀ i ∈ Equiv.Perm.cycleType k, i = 2
⊢ Equiv.Perm.cycleType k = Multiset.replicate (Equiv.Perm.support c).card 2
Tactic:
rw [← Multiset.eq_replicate_card] at 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
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
⊢ Equiv.Perm.cycleType k = Multiset.replicate (Equiv.Perm.support c).card 2