internlm/Lean-Github huggingface dataset:
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
case neg
α : 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))
x : α
hx : x ∉ Equiv.Perm.support g
⊢ x ∉ Equiv.Perm.support (k ^ 2)
Tactic:
intro hx'
Proof state after:
case neg
α : 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))
x : α
hx : x ∉ Equiv.Perm.support g
hx' : x ∈ Equiv.Perm.support (k ^ 2)
⊢ False
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
case neg
α : 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))
x : α
hx : x ∉ Equiv.Perm.support g
hx' : x ∈ Equiv.Perm.support (k ^ 2)
⊢ False
Tactic:
apply hx
Proof state after:
case neg
α : 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))
x : α
hx : x ∉ Equiv.Perm.support g
hx' : x ∈ Equiv.Perm.support (k ^ 2)
⊢ x ∈ Equiv.Perm.support g
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
case neg
α : 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))
x : α
hx : x ∉ Equiv.Perm.support g
hx' : x ∈ Equiv.Perm.support (k ^ 2)
⊢ x ∈ Equiv.Perm.support g
Tactic:
apply hksup
Proof state after:
case neg.a
α : 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))
x : α
hx : x ∉ Equiv.Perm.support g
hx' : x ∈ Equiv.Perm.support (k ^ 2)
⊢ x ∈ Equiv.Perm.support k
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
case neg.a
α : 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))
x : α
hx : x ∉ Equiv.Perm.support g
hx' : x ∈ Equiv.Perm.support (k ^ 2)
⊢ x ∈ Equiv.Perm.support k
Tactic:
apply Equiv.Perm.support_pow_le k 2
Proof state after:
case neg.a.a
α : 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))
x : α
hx : x ∉ Equiv.Perm.support g
hx' : x ∈ Equiv.Perm.support (k ^ 2)
⊢ x ∈ Equiv.Perm.support (k ^ 2)
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
case neg.a.a
α : 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))
x : α
hx : x ∉ Equiv.Perm.support g
hx' : x ∈ Equiv.Perm.support (k ^ 2)
⊢ x ∈ Equiv.Perm.support (k ^ 2)
Tactic:
exact hx'
Proof state after:
no goals
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
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
⊢ τ ∈ Iφ g
Tactic:
intro x
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
x : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ (Equiv.Perm.support ↑(τ x)).card = (Equiv.Perm.support ↑x).card
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
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
x : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ (Equiv.Perm.support ↑(τ x)).card = (Equiv.Perm.support ↑x).card
Tactic:
by_cases hx : x = ⟨c, hc⟩
Proof state after:
case pos
α : 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
x : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hx : x = { val := c, property := hc }
⊢ (Equiv.Perm.support ↑(τ x)).card = (Equiv.Perm.support ↑x).card

case neg
α : 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
x : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hx : ¬x = { val := c, property := hc }
⊢ (Equiv.Perm.support ↑(τ x)).card = (Equiv.Perm.support ↑x).card
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
case neg
α : 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
x : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hx : ¬x = { val := c, property := hc }
⊢ (Equiv.Perm.support ↑(τ x)).card = (Equiv.Perm.support ↑x).card
Tactic:
by_cases hx' : x = ⟨d, hd⟩
Proof state after:
case pos
α : 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
x : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hx : ¬x = { val := c, property := hc }
hx' : x = { val := d, property := hd }
⊢ (Equiv.Perm.support ↑(τ x)).card = (Equiv.Perm.support ↑x).card

case neg
α : 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
x : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hx : ¬x = { val := c, property := hc }
hx' : ¬x = { val := d, property := hd }
⊢ (Equiv.Perm.support ↑(τ x)).card = (Equiv.Perm.support ↑x).card
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
case pos
α : 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
x : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hx : x = { val := c, property := hc }
⊢ (Equiv.Perm.support ↑(τ x)).card = (Equiv.Perm.support ↑x).card
Tactic:
rw [hx, Equiv.swap_apply_left]
Proof state after:
case pos
α : 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
x : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hx : x = { val := c, property := hc }
⊢ (Equiv.Perm.support ↑{ val := d, property := hd }).card = (Equiv.Perm.support ↑{ val := c, property := hc }).card
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
case pos
α : 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
x : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hx : x = { val := c, property := hc }
⊢ (Equiv.Perm.support ↑{ val := d, property := hd }).card = (Equiv.Perm.support ↑{ val := c, property := hc }).card
Tactic:
exact hm.symm
Proof state after:
no goals
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
case pos
α : 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
x : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hx : ¬x = { val := c, property := hc }
hx' : x = { val := d, property := hd }
⊢ (Equiv.Perm.support ↑(τ x)).card = (Equiv.Perm.support ↑x).card
Tactic:
rw [hx', Equiv.swap_apply_right]
Proof state after:
case pos
α : 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
x : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hx : ¬x = { val := c, property := hc }
hx' : x = { val := d, property := hd }
⊢ (Equiv.Perm.support ↑{ val := c, property := hc }).card = (Equiv.Perm.support ↑{ val := d, property := hd }).card
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
case pos
α : 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
x : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hx : ¬x = { val := c, property := hc }
hx' : x = { val := d, property := hd }
⊢ (Equiv.Perm.support ↑{ val := c, property := hc }).card = (Equiv.Perm.support ↑{ val := d, property := hd }).card
Tactic:
exact hm
Proof state after:
no goals
Theorem: OnCycleFactors.count_le_one_of_mem_kerφ
Proof state before:
case neg
α : 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
x : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hx : ¬x = { val := c, property := hc }
hx' : ¬x = { val := d, property := hd }
⊢ (Equiv.Perm.support ↑(τ x)).card = (Equiv.Perm.support ↑x).card
Tactic:
rw [Equiv.swap_apply_of_ne_of_ne hx hx']
Proof state after:
no goals
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
⊢ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α ↔
    (∀ i ∈ Equiv.Perm.cycleType g, Odd i) ∧
      Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1 ∧
        ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
Tactic:
rw [SetLike.le_def]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
⊢ (∀ ⦃x : ConjAct (Equiv.Perm α)⦄, x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g → x ∈ alternatingGroup α) ↔
    (∀ i ∈ Equiv.Perm.cycleType g, Odd i) ∧
      Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1 ∧
        ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
⊢ (∀ ⦃x : ConjAct (Equiv.Perm α)⦄, x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g → x ∈ alternatingGroup α) ↔
    (∀ i ∈ Equiv.Perm.cycleType g, Odd i) ∧
      Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1 ∧
        ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
Tactic:
constructor
Proof state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
⊢ (∀ ⦃x : ConjAct (Equiv.Perm α)⦄, x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g → x ∈ alternatingGroup α) →
    (∀ i ∈ Equiv.Perm.cycleType g, Odd i) ∧
      Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1 ∧
        ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1

case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
⊢ ((∀ i ∈ Equiv.Perm.cycleType g, Odd i) ∧
      Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1 ∧
        ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1) →
    ∀ ⦃x : ConjAct (Equiv.Perm α)⦄, x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g → x ∈ alternatingGroup α
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof state before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
⊢ (∀ ⦃x : ConjAct (Equiv.Perm α)⦄, x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g → x ∈ alternatingGroup α) →
    (∀ i ∈ Equiv.Perm.cycleType g, Odd i) ∧
      Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1 ∧
        ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
Tactic:
intro h
Proof state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : ∀ ⦃x : ConjAct (Equiv.Perm α)⦄, x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g → x ∈ alternatingGroup α
⊢ (∀ i ∈ Equiv.Perm.cycleType g, Odd i) ∧
    Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1 ∧
      ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
Theorem: OnCycleFactors.kerφ_le_alternating_iff
Proof state before:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : ∀ ⦃x : ConjAct (Equiv.Perm α)⦄, x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g → x ∈ alternatingGroup α
⊢ (∀ i ∈ Equiv.Perm.cycleType g, Odd i) ∧
    Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1 ∧
      ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1
Tactic:
constructor
Proof state after:
case mp.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : ∀ ⦃x : ConjAct (Equiv.Perm α)⦄, x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g → x ∈ alternatingGroup α
⊢ ∀ i ∈ Equiv.Perm.cycleType g, Odd i

case mp.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : ∀ ⦃x : ConjAct (Equiv.Perm α)⦄, x ∈ MulAction.stabilizer (ConjAct (Equiv.Perm α)) g → x ∈ alternatingGroup α
⊢ Fintype.card α ≤ Multiset.sum (Equiv.Perm.cycleType g) + 1 ∧ ∀ (i : ℕ), Multiset.count i (Equiv.Perm.cycleType g) ≤ 1