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 α
⊢ ∀ x ∈ (Equiv.Perm.cycleFactorsFinset g).val,
    ∀ y ∈ (Equiv.Perm.cycleFactorsFinset g).val,
      (Finset.card ∘ Equiv.Perm.support) x = (Finset.card ∘ Equiv.Perm.support) y → x = y
Tactic:
simp only [Function.comp_apply, ← Finset.mem_def]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
⊢ ∀ x ∈ Equiv.Perm.cycleFactorsFinset g,
    ∀ y ∈ Equiv.Perm.cycleFactorsFinset g, (Equiv.Perm.support x).card = (Equiv.Perm.support y).card → x = y
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 α
⊢ ∀ x ∈ Equiv.Perm.cycleFactorsFinset g,
    ∀ y ∈ Equiv.Perm.cycleFactorsFinset g, (Equiv.Perm.support x).card = (Equiv.Perm.support y).card → x = y
Tactic:
by_contra hm
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm :
  ¬∀ x ∈ Equiv.Perm.cycleFactorsFinset g,
      ∀ y ∈ Equiv.Perm.cycleFactorsFinset g, (Equiv.Perm.support x).card = (Equiv.Perm.support y).card → x = y
⊢ 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 α
hm :
  ¬∀ x ∈ Equiv.Perm.cycleFactorsFinset g,
      ∀ y ∈ Equiv.Perm.cycleFactorsFinset g, (Equiv.Perm.support x).card = (Equiv.Perm.support y).card → x = y
⊢ False
Tactic:
push_neg at hm
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
hm :
  ∃ x ∈ Equiv.Perm.cycleFactorsFinset g,
    ∃ y ∈ Equiv.Perm.cycleFactorsFinset g, (Equiv.Perm.support x).card = (Equiv.Perm.support y).card ∧ x ≠ y
⊢ 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 α
hm :
  ∃ x ∈ Equiv.Perm.cycleFactorsFinset g,
    ∃ y ∈ Equiv.Perm.cycleFactorsFinset g, (Equiv.Perm.support x).card = (Equiv.Perm.support y).card ∧ x ≠ y
⊢ False
Tactic:
obtain ⟨c, hc, d, hd, hm, hm'⟩ := hm
Proof state after:
case intro.intro.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
⊢ False
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
case intro.intro.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
⊢ False
Tactic:
let τ : Equiv.Perm g.cycleFactorsFinset := Equiv.swap ⟨c, hc⟩ ⟨d, hd⟩
Proof state after:
case intro.intro.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 }
⊢ False
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
case intro.intro.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 }
⊢ False
Tactic:
obtain ⟨a⟩ := g.existsBasis
Proof state after:
case intro.intro.intro.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
⊢ 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
⊢ False
Tactic:
let k : Equiv.Perm α := ConjAct.ofConjAct (φ' a ⟨τ, hτ⟩ : ConjAct (Equiv.Perm α))
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τ })
⊢ 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τ })
⊢ False
Tactic:
have hk2 : ∀ c : g.cycleFactorsFinset, ConjAct.toConjAct k • (c : Equiv.Perm α) = τ c := by
  intro c
  rw [ConjAct.smul_def]
  simp only [ConjAct.ofConjAct_toConjAct]
  rw [mul_inv_eq_iff_eq_mul]
  ext x
  exact OnCycleFactors.k_cycle_apply hτ c x
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)
⊢ 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)
⊢ False
Tactic:
have hksup : k.support ≤ g.support := by
  intro x
  simp only [Equiv.Perm.mem_support]
  intro hx' hx; apply hx'
  rw [← Equiv.Perm.not_mem_support] at hx
  exact OnCycleFactors.k_apply_of_not_mem_support x hx
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
⊢ 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
⊢ False
Tactic:
suffices hsign_k : Equiv.Perm.sign k = -1 by
  rw [h _, ← Units.eq_iff] at hsign_k
  exact Int.noConfusion hsign_k
  exact (φ' a ⟨τ, hτ⟩).prop
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
⊢ Equiv.Perm.sign 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
⊢ Equiv.Perm.sign k = -1
Tactic:
suffices k.cycleType = Multiset.replicate c.support.card 2 by
  rw [Equiv.Perm.sign_of_cycleType]; rw [this]
  simp only [Multiset.sum_replicate, Algebra.id.smul_eq_mul, Multiset.card_replicate]
  rw [Odd.neg_one_pow]
  rw [Nat.odd_add']
  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]
  rw [mul_comm]; apply even_two_mul
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
⊢ Equiv.Perm.cycleType k = 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))
⊢ ∀ i ∈ Equiv.Perm.cycleType k, i = 2
Tactic:
suffices hk2 : orderOf k = 2 by
  have hk2' : Nat.Prime (orderOf k) := by
    rw [hk2]
    exact Nat.prime_two
  obtain ⟨n, hn⟩ := Equiv.Perm.cycleType_prime_order hk2'
  intro i hi
  rw [hn, hk2, Multiset.mem_replicate] at hi
  exact hi.right
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))
⊢ orderOf k = 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))
⊢ orderOf k = 2
Tactic:
apply orderOf_eq_prime
Proof state after:
case hg
α : 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))
⊢ k ^ 2 = 1

case hg1
α : 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))
⊢ k ≠ 1
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
case hg1
α : 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))
⊢ k ≠ 1
Tactic:
intro hk
Proof state after:
case hg1
α : 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))
hk : k = 1
⊢ False
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
case hg1
α : 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))
hk : k = 1
⊢ False
Tactic:
apply hm'
Proof state after:
case hg1
α : 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))
hk : k = 1
⊢ c = d
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
case hg1
α : 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))
hk : k = 1
⊢ c = d
Tactic:
specialize hk2 ⟨c, hc⟩
Proof state after:
case hg1
α : 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τ })
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))
hk : k = 1
hk2 : ConjAct.toConjAct k • ↑{ val := c, property := hc } = ↑(τ { val := c, property := hc })
⊢ c = d