internlm/Lean-Github huggingface dataset:
Theorem: OnCycleFactors.AlternatingGroup.of_cycleType_eq
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
⊢ Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
      (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ) =
    Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ
Tactic:
ext g
Proof state after:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
⊢ g ∈
      Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
        (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ) ↔
    g ∈ Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ
Theorem: OnCycleFactors.AlternatingGroup.of_cycleType_eq
Proof state before:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
⊢ g ∈
      Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
        (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ) ↔
    g ∈ Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ
Tactic:
simp only [Finset.mem_image, Finset.mem_filter]
Proof state after:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
⊢ g ∈
      Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
        (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ) ↔
    g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
Theorem: OnCycleFactors.AlternatingGroup.of_cycleType_eq
Proof state before:
case pos.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
⊢ g ∈
      Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
        (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ) ↔
    g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
Tactic:
constructor
Proof state after:
case pos.a.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
⊢ g ∈
      Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
        (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ) →
    g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m

case pos.a.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
⊢ g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m →
    g ∈
      Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
        (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ)
Theorem: OnCycleFactors.AlternatingGroup.of_cycleType_eq
Proof state before:
case pos.a.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
⊢ g ∈
      Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
        (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ) →
    g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
Tactic:
intro hg
Proof state after:
case pos.a.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
hg :
  g ∈
    Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
      (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ)
⊢ g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
Theorem: OnCycleFactors.AlternatingGroup.of_cycleType_eq
Proof state before:
case pos.a.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
hg :
  g ∈
    Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
      (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ)
⊢ g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
Tactic:
rw [Finset.mem_map] at hg
Proof state after:
case pos.a.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
hg :
  ∃ a ∈ Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ,
    { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ } a = g
⊢ g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
Theorem: OnCycleFactors.AlternatingGroup.of_cycleType_eq
Proof state before:
case pos.a.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
hg :
  ∃ a ∈ Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ,
    { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ } a = g
⊢ g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m
Tactic:
obtain ⟨⟨k, hk⟩, hk', rfl⟩ := hg
Proof state after:
case pos.a.mp.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
k : Equiv.Perm α
hk : k ∈ alternatingGroup α
hk' : { val := k, property := hk } ∈ Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ
⊢ { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ } { val := k, property := hk } ∈ Finset.univ ∧
    Equiv.Perm.cycleType
        ({ toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ } { val := k, property := hk }) =
      m
Theorem: OnCycleFactors.AlternatingGroup.of_cycleType_eq
Proof state before:
case pos.a.mp.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
k : Equiv.Perm α
hk : k ∈ alternatingGroup α
hk' : { val := k, property := hk } ∈ Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ
⊢ { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ } { val := k, property := hk } ∈ Finset.univ ∧
    Equiv.Perm.cycleType
        ({ toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ } { val := k, property := hk }) =
      m
Tactic:
apply And.intro (Finset.mem_univ _)
Proof state after:
case pos.a.mp.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
k : Equiv.Perm α
hk : k ∈ alternatingGroup α
hk' : { val := k, property := hk } ∈ Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ
⊢ Equiv.Perm.cycleType ({ toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ } { val := k, property := hk }) =
    m
Theorem: OnCycleFactors.AlternatingGroup.of_cycleType_eq
Proof state before:
case pos.a.mp.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
k : Equiv.Perm α
hk : k ∈ alternatingGroup α
hk' : { val := k, property := hk } ∈ Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ
⊢ Equiv.Perm.cycleType ({ toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ } { val := k, property := hk }) =
    m
Tactic:
simp only [Finset.mem_filter, Finset.mem_univ, Subgroup.coe_mk, true_and_iff] at hk'
Proof state after:
case pos.a.mp.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
k : Equiv.Perm α
hk : k ∈ alternatingGroup α
hk' : Equiv.Perm.cycleType k = m
⊢ Equiv.Perm.cycleType ({ toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ } { val := k, property := hk }) =
    m
Theorem: OnCycleFactors.AlternatingGroup.of_cycleType_eq
Proof state before:
case pos.a.mp.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
k : Equiv.Perm α
hk : k ∈ alternatingGroup α
hk' : Equiv.Perm.cycleType k = m
⊢ Equiv.Perm.cycleType ({ toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ } { val := k, property := hk }) =
    m
Tactic:
simp only [Subgroup.coeSubtype, Function.Embedding.coeFn_mk, Subgroup.coe_mk]
Proof state after:
case pos.a.mp.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
k : Equiv.Perm α
hk : k ∈ alternatingGroup α
hk' : Equiv.Perm.cycleType k = m
⊢ Equiv.Perm.cycleType k = m
Theorem: OnCycleFactors.AlternatingGroup.of_cycleType_eq
Proof state before:
case pos.a.mp.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
k : Equiv.Perm α
hk : k ∈ alternatingGroup α
hk' : Equiv.Perm.cycleType k = m
⊢ Equiv.Perm.cycleType k = m
Tactic:
exact hk'
Proof state after:
no goals
Theorem: OnCycleFactors.AlternatingGroup.of_cycleType_eq
Proof state before:
case pos.a.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
⊢ g ∈ Finset.univ ∧ Equiv.Perm.cycleType g = m →
    g ∈
      Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
        (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ)
Tactic:
rintro ⟨_, hg⟩
Proof state after:
case pos.a.mpr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
left✝ : g ∈ Finset.univ
hg : Equiv.Perm.cycleType g = m
⊢ g ∈
    Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
      (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ)
Theorem: OnCycleFactors.AlternatingGroup.of_cycleType_eq
Proof state before:
case pos.a.mpr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
left✝ : g ∈ Finset.univ
hg : Equiv.Perm.cycleType g = m
⊢ g ∈
    Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
      (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ)
Tactic:
simp only [Subgroup.coeSubtype, Finset.mem_map, Finset.mem_filter, Finset.mem_univ,
  true_and_iff, Function.Embedding.coeFn_mk, exists_prop]
Proof state after:
case pos.a.mpr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
left✝ : g ∈ Finset.univ
hg : Equiv.Perm.cycleType g = m
⊢ ∃ a, Equiv.Perm.cycleType ↑a = m ∧ ↑a = g
Theorem: OnCycleFactors.AlternatingGroup.of_cycleType_eq
Proof state before:
case pos.a.mpr.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
left✝ : g ∈ Finset.univ
hg : Equiv.Perm.cycleType g = m
⊢ ∃ a, Equiv.Perm.cycleType ↑a = m ∧ ↑a = g
Tactic:
use! g
Proof state after:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
left✝ : g ∈ Finset.univ
hg : Equiv.Perm.cycleType g = m
⊢ g ∈ alternatingGroup α
Theorem: OnCycleFactors.AlternatingGroup.of_cycleType_eq
Proof state before:
case property
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
left✝ : g ∈ Finset.univ
hg : Equiv.Perm.cycleType g = m
⊢ g ∈ alternatingGroup α
Tactic:
rw [Equiv.Perm.mem_alternatingGroup, Equiv.Perm.sign_of_cycleType, hg, Even.neg_one_pow hm]
Proof state after:
no goals
Theorem: OnCycleFactors.AlternatingGroup.of_cycleType_eq
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬Even (Multiset.sum m + Multiset.card m)
⊢ Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
      (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ) =
    ∅
Tactic:
rw [Finset.eq_empty_iff_forall_not_mem]
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬Even (Multiset.sum m + Multiset.card m)
⊢ ∀ (x : Equiv.Perm α),
    x ∉
      Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
        (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ)
Theorem: OnCycleFactors.AlternatingGroup.of_cycleType_eq
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬Even (Multiset.sum m + Multiset.card m)
⊢ ∀ (x : Equiv.Perm α),
    x ∉
      Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
        (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ)
Tactic:
intro g hg
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : ¬Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
hg :
  g ∈
    Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
      (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ)
⊢ False
Theorem: OnCycleFactors.AlternatingGroup.of_cycleType_eq
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : ¬Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
hg :
  g ∈
    Finset.map { toFun := ⇑(Subgroup.subtype (alternatingGroup α)), inj' := ⋯ }
      (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ)
⊢ False
Tactic:
simp only [Subgroup.coeSubtype, Finset.mem_map, Finset.mem_filter, Finset.mem_univ,
  true_and_iff, Function.Embedding.coeFn_mk, exists_prop] at hg
Proof state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : ¬Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
hg : ∃ a, Equiv.Perm.cycleType ↑a = m ∧ ↑a = g
⊢ False
Theorem: OnCycleFactors.AlternatingGroup.of_cycleType_eq
Proof state before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g✝ : Equiv.Perm α
m : Multiset ℕ
hm : ¬Even (Multiset.sum m + Multiset.card m)
g : Equiv.Perm α
hg : ∃ a, Equiv.Perm.cycleType ↑a = m ∧ ↑a = g
⊢ False
Tactic:
obtain ⟨⟨k, hk⟩, hkm, rfl⟩ := hg
Proof state after:
case neg.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬Even (Multiset.sum m + Multiset.card m)
k : Equiv.Perm α
hk : k ∈ alternatingGroup α
hkm : Equiv.Perm.cycleType ↑{ val := k, property := hk } = m
⊢ False
Theorem: OnCycleFactors.AlternatingGroup.of_cycleType_eq
Proof state before:
case neg.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬Even (Multiset.sum m + Multiset.card m)
k : Equiv.Perm α
hk : k ∈ alternatingGroup α
hkm : Equiv.Perm.cycleType ↑{ val := k, property := hk } = m
⊢ False
Tactic:
rw [← Nat.odd_iff_not_even] at hm
Proof state after:
case neg.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : Odd (Multiset.sum m + Multiset.card m)
k : Equiv.Perm α
hk : k ∈ alternatingGroup α
hkm : Equiv.Perm.cycleType ↑{ val := k, property := hk } = m
⊢ False
Theorem: OnCycleFactors.AlternatingGroup.of_cycleType_eq
Proof state before:
case neg.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : Odd (Multiset.sum m + Multiset.card m)
k : Equiv.Perm α
hk : k ∈ alternatingGroup α
hkm : Equiv.Perm.cycleType ↑{ val := k, property := hk } = m
⊢ False
Tactic:
simp only [Subgroup.coe_mk] at hkm
Proof state after:
case neg.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : Odd (Multiset.sum m + Multiset.card m)
k : Equiv.Perm α
hk : k ∈ alternatingGroup α
hkm : Equiv.Perm.cycleType k = m
⊢ False
Theorem: OnCycleFactors.AlternatingGroup.of_cycleType_eq
Proof state before:
case neg.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : Odd (Multiset.sum m + Multiset.card m)
k : Equiv.Perm α
hk : k ∈ alternatingGroup α
hkm : Equiv.Perm.cycleType k = m
⊢ False
Tactic:
simp only [Equiv.Perm.mem_alternatingGroup, Equiv.Perm.sign_of_cycleType, hkm, Odd.neg_one_pow hm, ← Units.eq_iff] at hk
Proof state after:
case neg.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : Odd (Multiset.sum m + Multiset.card m)
k : Equiv.Perm α
hkm : Equiv.Perm.cycleType k = m
hk : ↑(-1) = ↑1
⊢ False
Theorem: OnCycleFactors.AlternatingGroup.of_cycleType_eq
Proof state before:
case neg.intro.mk.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : Odd (Multiset.sum m + Multiset.card m)
k : Equiv.Perm α
hkm : Equiv.Perm.cycleType k = m
hk : ↑(-1) = ↑1
⊢ False
Tactic:
norm_num at hk
Proof state after:
no goals
Theorem: OnCycleFactors.AlternatingGroup.card_of_cycleType_mul_eq
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
⊢ (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    if (Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m) then
      Nat.factorial (Fintype.card α)
    else 0
Tactic:
split_ifs with hm
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : (Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m)
⊢ (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    Nat.factorial (Fintype.card α)

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : ¬((Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m))
⊢ (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    0
Theorem: OnCycleFactors.AlternatingGroup.card_of_cycleType_mul_eq
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : (Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m)
⊢ (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    Nat.factorial (Fintype.card α)
Tactic:
rw [← Finset.card_map]
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : (Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m)
⊢ (Finset.map ?pos✝ (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ)).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    Nat.factorial (Fintype.card α)

case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : (Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m)
⊢ ↥(alternatingGroup α) ↪ ?m.477188

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : (Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m)
⊢ Type ?u.477186
Theorem: OnCycleFactors.AlternatingGroup.card_of_cycleType_mul_eq
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : (Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m)
⊢ (Finset.map ?pos✝ (Finset.filter (fun g => Equiv.Perm.cycleType ↑g = m) Finset.univ)).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    Nat.factorial (Fintype.card α)

case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : (Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m)
⊢ ↥(alternatingGroup α) ↪ ?m.477188

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : (Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m)
⊢ Type ?u.477186
Tactic:
rw [AlternatingGroup.of_cycleType_eq]
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : (Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m)
⊢ (if Even (Multiset.sum m + Multiset.card m) then Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ
        else ∅).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    Nat.factorial (Fintype.card α)
Theorem: OnCycleFactors.AlternatingGroup.card_of_cycleType_mul_eq
Proof state before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : (Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m)
⊢ (if Even (Multiset.sum m + Multiset.card m) then Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ
        else ∅).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    Nat.factorial (Fintype.card α)
Tactic:
rw [if_pos]
Proof state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : (Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m)
⊢ (Finset.filter (fun g => Equiv.Perm.cycleType g = m) Finset.univ).card *
      (Nat.factorial (Fintype.card α - Multiset.sum m) *
        (Multiset.prod m *
          Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n m)) (Multiset.dedup m)))) =
    Nat.factorial (Fintype.card α)

case pos.hc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
m : Multiset ℕ
hm : (Multiset.sum m ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (Multiset.sum m + Multiset.card m)
⊢ Even (Multiset.sum m + Multiset.card m)