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
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
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
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
⊢ Multiset.replicate (Multiset.card (Equiv.Perm.cycleType k)) 2 = Multiset.replicate (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
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
⊢ Multiset.replicate (Multiset.card (Equiv.Perm.cycleType k)) 2 = Multiset.replicate (Equiv.Perm.support c).card 2
Tactic:
congr
Proof state after:
case e_n
α : 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
⊢ Multiset.card (Equiv.Perm.cycleType k) = (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
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.sum (Equiv.Perm.cycleType k) = (Equiv.Perm.support k).card
⊢ Multiset.card (Equiv.Perm.cycleType k) = (Equiv.Perm.support c).card
Tactic:
rw [this] 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
this' : Multiset.sum (Multiset.replicate (Multiset.card (Equiv.Perm.cycleType k)) 2) = (Equiv.Perm.support k).card
⊢ Multiset.card (Equiv.Perm.cycleType k) = (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
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.sum (Multiset.replicate (Multiset.card (Equiv.Perm.cycleType k)) 2) = (Equiv.Perm.support k).card
⊢ Multiset.card (Equiv.Perm.cycleType k) = (Equiv.Perm.support c).card
Tactic:
simp only [Multiset.sum_replicate, Algebra.id.smul_eq_mul] 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
this' : Multiset.card (Equiv.Perm.cycleType k) * 2 = (Equiv.Perm.support k).card
⊢ Multiset.card (Equiv.Perm.cycleType k) = (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
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
⊢ 2 ≠ 0
Tactic:
norm_num
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 : 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
this2 : Equiv.Perm.support k = Equiv.Perm.support c ∪ Equiv.Perm.support d
⊢ (Equiv.Perm.support k).card = (Equiv.Perm.support c).card * 2
Tactic:
rw [this2]
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
this' : Multiset.card (Equiv.Perm.cycleType k) * 2 = (Equiv.Perm.support k).card
this2 : Equiv.Perm.support k = Equiv.Perm.support c ∪ Equiv.Perm.support d
⊢ (Equiv.Perm.support c ∪ Equiv.Perm.support d).card = (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
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
this2 : Equiv.Perm.support k = Equiv.Perm.support c ∪ Equiv.Perm.support d
⊢ Disjoint (Equiv.Perm.support c) (Equiv.Perm.support d)
Tactic:
rw [← Equiv.Perm.disjoint_iff_disjoint_support]
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
this' : Multiset.card (Equiv.Perm.cycleType k) * 2 = (Equiv.Perm.support k).card
this2 : Equiv.Perm.support k = Equiv.Perm.support c ∪ Equiv.Perm.support d
⊢ Equiv.Perm.Disjoint c d
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 : 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
this2 : Equiv.Perm.support k = Equiv.Perm.support c ∪ Equiv.Perm.support d
⊢ Equiv.Perm.Disjoint c d
Tactic:
by_contra hcd
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
this' : Multiset.card (Equiv.Perm.cycleType k) * 2 = (Equiv.Perm.support k).card
this2 : Equiv.Perm.support k = Equiv.Perm.support c ∪ Equiv.Perm.support d
hcd : ¬Equiv.Perm.Disjoint c d
⊢ False
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 : 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
this2 : Equiv.Perm.support k = Equiv.Perm.support c ∪ Equiv.Perm.support d
hcd : ¬Equiv.Perm.Disjoint c d
⊢ False
Tactic:
apply hm'
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
this' : Multiset.card (Equiv.Perm.cycleType k) * 2 = (Equiv.Perm.support k).card
this2 : Equiv.Perm.support k = Equiv.Perm.support c ∪ Equiv.Perm.support d
hcd : ¬Equiv.Perm.Disjoint c d
⊢ c = d
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 : 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
this2 : Equiv.Perm.support k = Equiv.Perm.support c ∪ Equiv.Perm.support d
hcd : ¬Equiv.Perm.Disjoint c d
⊢ c = d
Tactic:
exact Set.Pairwise.eq g.cycleFactorsFinset_pairwise_disjoint hc hd hcd
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 : 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
this2 : Equiv.Perm.support k = Equiv.Perm.support c ∪ Equiv.Perm.support d
this3 : (Equiv.Perm.support d).card = (Equiv.Perm.support c).card
⊢ (Equiv.Perm.support c).card + (Equiv.Perm.support d).card = (Equiv.Perm.support c).card * 2
Tactic:
rw [this3]
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
this' : Multiset.card (Equiv.Perm.cycleType k) * 2 = (Equiv.Perm.support k).card
this2 : Equiv.Perm.support k = Equiv.Perm.support c ∪ Equiv.Perm.support d
this3 : (Equiv.Perm.support d).card = (Equiv.Perm.support c).card
⊢ (Equiv.Perm.support c).card + (Equiv.Perm.support c).card = (Equiv.Perm.support c).card * 2