internlm/Lean-Github huggingface dataset:
Theorem: OnCycleFactors.θ_apply_single
Proof state before:
case neg.intro.a.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
vc : ↥(Subgroup.zpowers ↑c)
x : α
hx : x ∉ Equiv.Perm.support g
m : ℤ
hm : ↑c ^ m = ↑vc
hx' : x ∈ Equiv.Perm.support (↑c ^ m)
⊢ x ∈ Equiv.Perm.support ↑c
Tactic:
apply Equiv.Perm.support_zpow_le _ _ hx'
Proof state after:
no goals
Theorem: OnCycleFactors.sign_ψ
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ Equiv.Perm.sign ((θ g) (k, v)) = Equiv.Perm.sign k * Finset.prod Finset.univ fun c => Equiv.Perm.sign ↑(v c)
Tactic:
rw [← Prod.fst_mul_snd ⟨k, v⟩]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ Equiv.Perm.sign ((θ g) (((k, v).1, 1) * (1, (k, v).2))) =
    Equiv.Perm.sign k * Finset.prod Finset.univ fun c => Equiv.Perm.sign ↑(v c)
Theorem: OnCycleFactors.sign_ψ
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ Equiv.Perm.sign ((θ g) (((k, v).1, 1) * (1, (k, v).2))) =
    Equiv.Perm.sign k * Finset.prod Finset.univ fun c => Equiv.Perm.sign ↑(v c)
Tactic:
simp only [map_mul]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ Equiv.Perm.sign ((θ g) (k, 1)) * Equiv.Perm.sign ((θ g) (1, v)) =
    Equiv.Perm.sign k * Finset.prod Finset.univ fun c => Equiv.Perm.sign ↑(v c)
Theorem: OnCycleFactors.sign_ψ
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ Equiv.Perm.sign ((θ g) (k, 1)) * Equiv.Perm.sign ((θ g) (1, v)) =
    Equiv.Perm.sign k * Finset.prod Finset.univ fun c => Equiv.Perm.sign ↑(v c)
Tactic:
apply congr_arg₂
Proof state after:
case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ Equiv.Perm.sign ((θ g) (k, 1)) = Equiv.Perm.sign k

case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ Equiv.Perm.sign ((θ g) (1, v)) = Finset.prod Finset.univ fun c => Equiv.Perm.sign ↑(v c)
Theorem: OnCycleFactors.sign_ψ
Proof state before:
case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ Equiv.Perm.sign ((θ g) (k, 1)) = Equiv.Perm.sign k
Tactic:
rw [θ_apply_fst, Equiv.Perm.sign_ofSubtype]
Proof state after:
no goals
Theorem: OnCycleFactors.sign_ψ
Proof state before:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ Equiv.Perm.sign ((θ g) (1, v)) = Finset.prod Finset.univ fun c => Equiv.Perm.sign ↑(v c)
Tactic:
rw [← MonoidHom.inr_apply, ← MonoidHom.comp_apply]
Proof state after:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ (MonoidHom.comp Equiv.Perm.sign (θ g))
      ((MonoidHom.inr (Equiv.Perm ↑(MulAction.fixedBy α g))
          ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)))
        v) =
    Finset.prod Finset.univ fun c => Equiv.Perm.sign ↑(v c)
Theorem: OnCycleFactors.sign_ψ
Proof state before:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ (MonoidHom.comp Equiv.Perm.sign (θ g))
      ((MonoidHom.inr (Equiv.Perm ↑(MulAction.fixedBy α g))
          ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)))
        v) =
    Finset.prod Finset.univ fun c => Equiv.Perm.sign ↑(v c)
Tactic:
conv_lhs => rw [← Finset.noncommProd_mul_single v]
Proof state after:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ (MonoidHom.comp Equiv.Perm.sign (θ g))
      ((MonoidHom.inr (Equiv.Perm ↑(MulAction.fixedBy α g))
          ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)))
        (Finset.noncommProd Finset.univ (fun i => Pi.mulSingle i (v i)) ⋯)) =
    Finset.prod Finset.univ fun c => Equiv.Perm.sign ↑(v c)
Theorem: OnCycleFactors.sign_ψ
Proof state before:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ (MonoidHom.comp Equiv.Perm.sign (θ g))
      ((MonoidHom.inr (Equiv.Perm ↑(MulAction.fixedBy α g))
          ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)))
        (Finset.noncommProd Finset.univ (fun i => Pi.mulSingle i (v i)) ⋯)) =
    Finset.prod Finset.univ fun c => Equiv.Perm.sign ↑(v c)
Tactic:
simp only [Finset.noncommProd_map]
Proof state after:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ Finset.noncommProd Finset.univ
      (fun i =>
        (MonoidHom.comp Equiv.Perm.sign (θ g))
          ((MonoidHom.inr (Equiv.Perm ↑(MulAction.fixedBy α g))
              ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)))
            (Pi.mulSingle i (v i))))
      ⋯ =
    Finset.prod Finset.univ fun c => Equiv.Perm.sign ↑(v c)
Theorem: OnCycleFactors.sign_ψ
Proof state before:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ Finset.noncommProd Finset.univ
      (fun i =>
        (MonoidHom.comp Equiv.Perm.sign (θ g))
          ((MonoidHom.inr (Equiv.Perm ↑(MulAction.fixedBy α g))
              ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)))
            (Pi.mulSingle i (v i))))
      ⋯ =
    Finset.prod Finset.univ fun c => Equiv.Perm.sign ↑(v c)
Tactic:
rw [Finset.noncommProd_eq_prod]
Proof state after:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ (Finset.prod Finset.univ fun i =>
      (MonoidHom.comp Equiv.Perm.sign (θ g))
        ((MonoidHom.inr (Equiv.Perm ↑(MulAction.fixedBy α g))
            ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)))
          (Pi.mulSingle i (v i)))) =
    Finset.prod Finset.univ fun c => Equiv.Perm.sign ↑(v c)
Theorem: OnCycleFactors.sign_ψ
Proof state before:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ (Finset.prod Finset.univ fun i =>
      (MonoidHom.comp Equiv.Perm.sign (θ g))
        ((MonoidHom.inr (Equiv.Perm ↑(MulAction.fixedBy α g))
            ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)))
          (Pi.mulSingle i (v i)))) =
    Finset.prod Finset.univ fun c => Equiv.Perm.sign ↑(v c)
Tactic:
apply Finset.prod_congr rfl
Proof state after:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ ∀ x ∈ Finset.univ,
    (MonoidHom.comp Equiv.Perm.sign (θ g))
        ((MonoidHom.inr (Equiv.Perm ↑(MulAction.fixedBy α g))
            ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)))
          (Pi.mulSingle x (v x))) =
      Equiv.Perm.sign ↑(v x)
Theorem: OnCycleFactors.sign_ψ
Proof state before:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
⊢ ∀ x ∈ Finset.univ,
    (MonoidHom.comp Equiv.Perm.sign (θ g))
        ((MonoidHom.inr (Equiv.Perm ↑(MulAction.fixedBy α g))
            ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)))
          (Pi.mulSingle x (v x))) =
      Equiv.Perm.sign ↑(v x)
Tactic:
intro c _
Proof state after:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
a✝ : c ∈ Finset.univ
⊢ (MonoidHom.comp Equiv.Perm.sign (θ g))
      ((MonoidHom.inr (Equiv.Perm ↑(MulAction.fixedBy α g))
          ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)))
        (Pi.mulSingle c (v c))) =
    Equiv.Perm.sign ↑(v c)
Theorem: OnCycleFactors.sign_ψ
Proof state before:
case hy
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
k : Equiv.Perm ↑(MulAction.fixedBy α g)
v : (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
a✝ : c ∈ Finset.univ
⊢ (MonoidHom.comp Equiv.Perm.sign (θ g))
      ((MonoidHom.inr (Equiv.Perm ↑(MulAction.fixedBy α g))
          ((c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }) → ↥(Subgroup.zpowers ↑c)))
        (Pi.mulSingle c (v c))) =
    Equiv.Perm.sign ↑(v c)
Tactic:
simp only [MonoidHom.inr_apply, MonoidHom.coe_comp, Function.comp_apply, θ_apply_single]
Proof state after:
no goals
Theorem: OnCycleFactors.odd_of_mem_kerφ
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
⊢ ∀ i ∈ Equiv.Perm.cycleType g, Odd i
Tactic:
intro i hi
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
⊢ Odd i
Theorem: OnCycleFactors.odd_of_mem_kerφ
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
⊢ Odd i
Tactic:
rw [Equiv.Perm.cycleType_def g, Multiset.mem_map] at hi
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
i : ℕ
hi : ∃ a ∈ (Equiv.Perm.cycleFactorsFinset g).val, (Finset.card ∘ Equiv.Perm.support) a = i
⊢ Odd i
Theorem: OnCycleFactors.odd_of_mem_kerφ
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
i : ℕ
hi : ∃ a ∈ (Equiv.Perm.cycleFactorsFinset g).val, (Finset.card ∘ Equiv.Perm.support) a = i
⊢ Odd i
Tactic:
obtain ⟨c, hc, rfl⟩ := hi
Proof state after:
case 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).val
⊢ Odd ((Finset.card ∘ Equiv.Perm.support) c)
Theorem: OnCycleFactors.odd_of_mem_kerφ
Proof state before:
case 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).val
⊢ Odd ((Finset.card ∘ Equiv.Perm.support) c)
Tactic:
rw [← Finset.mem_def] at hc
Proof state after:
case 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
⊢ Odd ((Finset.card ∘ Equiv.Perm.support) c)
Theorem: OnCycleFactors.odd_of_mem_kerφ
Proof state before:
case 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
⊢ Equiv.Perm.sign c = 1
Tactic:
suffices c = θ g ⟨1, Pi.mulSingle ⟨c, hc⟩ ⟨c, Subgroup.mem_zpowers c⟩⟩ by
  rw [this]
  apply h
  change ConjAct.toConjAct _ ∈ _
  apply Subgroup.map_subtype_le
  rw [OnCycleFactors.hφ_ker_eq_θ_range]
  exact Set.mem_range_self _
Proof state after:
case 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
⊢ c = (θ g) (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ })
Theorem: OnCycleFactors.odd_of_mem_kerφ
Proof state before:
case 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
⊢ c = (θ g) (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ })
Tactic:
rw [θ_apply_single]
Proof state after:
no goals
Theorem: OnCycleFactors.odd_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
this : Equiv.Perm.sign c = 1
⊢ Odd ((Finset.card ∘ Equiv.Perm.support) c)
Tactic:
rw [Equiv.Perm.IsCycle.sign _, neg_eq_iff_eq_neg] 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
this : (-1) ^ (Equiv.Perm.support c).card = -1
⊢ Odd ((Finset.card ∘ Equiv.Perm.support) c)

α : 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
this : Equiv.Perm.sign c = 1
⊢ Equiv.Perm.IsCycle c
Theorem: OnCycleFactors.odd_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
this : (-1) ^ (Equiv.Perm.support c).card = -1
⊢ Odd ((Finset.card ∘ Equiv.Perm.support) c)
Tactic:
rw [Nat.odd_iff_not_even, Function.comp_apply]
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
this : (-1) ^ (Equiv.Perm.support c).card = -1
⊢ ¬Even (Equiv.Perm.support c).card
Theorem: OnCycleFactors.odd_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
this : (-1) ^ (Equiv.Perm.support c).card = -1
⊢ ¬Even (Equiv.Perm.support c).card
Tactic:
rw [← neg_one_pow_eq_one_iff_even (R := ℤˣ) (by norm_num), this, ← Units.eq_iff]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
this : (-1) ^ (Equiv.Perm.support c).card = -1
⊢ ¬↑(-1) = ↑1
Theorem: OnCycleFactors.odd_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
this : (-1) ^ (Equiv.Perm.support c).card = -1
⊢ ¬↑(-1) = ↑1
Tactic:
norm_num
Proof state after:
no goals
Theorem: OnCycleFactors.odd_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
this : (-1) ^ (Equiv.Perm.support c).card = -1
⊢ -1 ≠ 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: OnCycleFactors.odd_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
this : Equiv.Perm.sign c = 1
⊢ Equiv.Perm.IsCycle c
Tactic:
rw [Equiv.Perm.mem_cycleFactorsFinset_iff] at hc
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 : Equiv.Perm.IsCycle c ∧ ∀ a ∈ Equiv.Perm.support c, c a = g a
this : Equiv.Perm.sign c = 1
⊢ Equiv.Perm.IsCycle c
Theorem: OnCycleFactors.odd_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 : Equiv.Perm.IsCycle c ∧ ∀ a ∈ Equiv.Perm.support c, c a = g a
this : Equiv.Perm.sign c = 1
⊢ Equiv.Perm.IsCycle c
Tactic:
exact hc.left
Proof state after:
no goals
Theorem: OnCycleFactors.odd_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
this : c = (θ g) (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ })
⊢ Equiv.Perm.sign c = 1
Tactic:
rw [this]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
h : MulAction.stabilizer (ConjAct (Equiv.Perm α)) g ≤ alternatingGroup α
c : Equiv.Perm α
hc : c ∈ Equiv.Perm.cycleFactorsFinset g
this : c = (θ g) (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ })
⊢ Equiv.Perm.sign ((θ g) (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ })) = 1
Theorem: OnCycleFactors.odd_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
this : c = (θ g) (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ })
⊢ Equiv.Perm.sign ((θ g) (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ })) = 1
Tactic:
apply h
Proof state after:
case 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
this : c = (θ g) (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ })
⊢ (θ g) (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }) ∈
    MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
Theorem: OnCycleFactors.odd_of_mem_kerφ
Proof state before:
case 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
this : c = (θ g) (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ })
⊢ (θ g) (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }) ∈
    MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
Tactic:
change ConjAct.toConjAct _ ∈ _
Proof state after:
case 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
this : c = (θ g) (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ })
⊢ ConjAct.toConjAct
      {
        toFun :=
          θAux g (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).1
            (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).2,
        invFun :=
          θAux g (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).1⁻¹
            (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).2⁻¹,
        left_inv := ⋯, right_inv := ⋯ } ∈
    MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
Theorem: OnCycleFactors.odd_of_mem_kerφ
Proof state before:
case 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
this : c = (θ g) (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ })
⊢ ConjAct.toConjAct
      {
        toFun :=
          θAux g (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).1
            (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).2,
        invFun :=
          θAux g (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).1⁻¹
            (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).2⁻¹,
        left_inv := ⋯, right_inv := ⋯ } ∈
    MulAction.stabilizer (ConjAct (Equiv.Perm α)) g
Tactic:
apply Subgroup.map_subtype_le
Proof state after:
case 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
this : c = (θ g) (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ })
⊢ ConjAct.toConjAct
      {
        toFun :=
          θAux g (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).1
            (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).2,
        invFun :=
          θAux g (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).1⁻¹
            (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ }).2⁻¹,
        left_inv := ⋯, right_inv := ⋯ } ∈
    Subgroup.map (Subgroup.subtype (MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)) ?a.K✝

case a.K
α : 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
this : c = (θ g) (1, Pi.mulSingle { val := c, property := hc } { val := c, property := ⋯ })
⊢ Subgroup ↥(MulAction.stabilizer (ConjAct (Equiv.Perm α)) g)