awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
X : Type u_3
hX : 5 ≤ Cardinal.mk X
h : IsSolvable.{u_3} (Perm X)
⊢ Nonempty.{max 1 (u_3 + 1)} (Fin 5 ↪ X)
have rwa : Cardinal.lift.{u_3, 0} (Cardinal.mk (Fin 5)) ≤ Cardinal.lift.{u_3, u_3} (Cardinal.mk X)
Tactic: rwa [← Cardinal.lift_mk_le, Cardinal.mk_fin, Cardinal.lift_natCast, Cardinal.lift_id]
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
X : Type u_3
hX : 5 ≤ Cardinal.mk X
h : IsSolvable.{u_3} (Perm X)
rwa : Cardinal.lift.{u_3, 0} (Cardinal.mk (Fin 5)) ≤ Cardinal.lift.{u_3, u_3} (Cardinal.mk X)
⊢ Nonempty.{max 1 (u_3 + 1)} (Fin 5 ↪ X)
have rwa₁ : Cardinal.lift.{u_3, 0} (↑5 : Cardinal.{0}) ≤ Cardinal.lift.{u_3, u_3} (Cardinal.mk X)
Tactic: rwa [← Cardinal.lift_mk_le, Cardinal.mk_fin, Cardinal.lift_natCast, Cardinal.lift_id]
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
X : Type u_3
hX : 5 ≤ Cardinal.mk X
h : IsSolvable.{u_3} (Perm X)
rwa : Cardinal.lift.{u_3, 0} (Cardinal.mk (Fin 5)) ≤ Cardinal.lift.{u_3, u_3} (Cardinal.mk X)
rwa₁ : Cardinal.lift.{u_3, 0} (↑5 : Cardinal.{0}) ≤ Cardinal.lift.{u_3, u_3} (Cardinal.mk X)
⊢ Nonempty.{max 1 (u_3 + 1)} (Fin 5 ↪ X)
have rwa₂ : (↑5 : Cardinal.{u_3}) ≤ Cardinal.lift.{u_3, u_3} (Cardinal.mk X)
Tactic: rwa [← Cardinal.lift_mk_le, Cardinal.mk_fin, Cardinal.lift_natCast, Cardinal.lift_id]
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (goal)
Goal:
X : Type u_3
hX : 5 ≤ Cardinal.mk X
h : IsSolvable.{u_3} (Perm X)
rwa : Cardinal.lift.{u_3, 0} (Cardinal.mk (Fin 5)) ≤ Cardinal.lift.{u_3, u_3} (Cardinal.mk X)
rwa₁ : Cardinal.lift.{u_3, 0} (↑5 : Cardinal.{0}) ≤ Cardinal.lift.{u_3, u_3} (Cardinal.mk X)
rwa₂ : (↑5 : Cardinal.{u_3}) ≤ Cardinal.lift.{u_3, u_3} (Cardinal.mk X)
⊢ Nonempty.{max 1 (u_3 + 1)} (Fin 5 ↪ X)
have rwa₃ : (↑5 : Cardinal.{u_3}) ≤ Cardinal.mk X
Tactic: rwa [← Cardinal.lift_mk_le, Cardinal.mk_fin, Cardinal.lift_natCast, Cardinal.lift_id]
-- Lean 4 proof step from Mathlib.GroupTheory.Solvable (hypothesis)
Goal:
X : Type u_3
hX : 5 ≤ Cardinal.mk X
h : IsSolvable.{u_3} (Perm X)
⊢ False
have key : Nonempty.{max 1 (u_3 + 1)} (Fin 5 ↪ X)
Tactic: have key : Nonempty (Fin 5 ↪ X) := by
    rwa [← Cardinal.lift_mk_le, Cardinal.mk_fin, Cardinal.lift_natCast, Cardinal.lift_id]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
i : ℕ
hi : i ∈ g.cycleType
⊢ Odd i
have hi₁ : ∃ a ∈ g.cycleFactorsFinset.val, (card ∘ support) a = i
Tactic: rw [cycleType_def g, Multiset.mem_map] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
i : ℕ
hi : ∃ a ∈ g.cycleFactorsFinset.val, (card ∘ support) a = i
⊢ Odd i
have obtain : ∀ (c : Perm α) (hc : c ∈ g.cycleFactorsFinset.val), Odd ((card ∘ support) c)
Tactic: obtain ⟨c, hc, rfl⟩ := hi
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset.val
⊢ Odd ((card ∘ support) c)
have hc₁ : c ∈ g.cycleFactorsFinset
Tactic: rw [← Finset.mem_def] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
this : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) c : ℤˣ) (1 : ℤˣ)
⊢ Odd ((card ∘ support) c)
have rw : ∀ (this : HPow.hPow (α := ℤˣ) (-1) #c.support ≠ 1), Odd ((card ∘ support) c)
Tactic: rw [IsCycle.sign _, neg_eq_iff_eq_neg, ← Int.units_ne_iff_eq_neg] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
this : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) c : ℤˣ) (1 : ℤˣ)
rw : ∀ (this : HPow.hPow (α := ℤˣ) (-1) #c.support ≠ 1), Odd ((card ∘ support) c)
⊢ Odd ((card ∘ support) c)
have rw₁ : c.IsCycle
Tactic: rw [IsCycle.sign _, neg_eq_iff_eq_neg, ← Int.units_ne_iff_eq_neg] at this
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
this : HPow.hPow (α := ℤˣ) (-1) #c.support ≠ 1
⊢ Odd ((card ∘ support) c)
have rw : ¬Even #c.support
Tactic: rw [← Nat.not_even_iff_odd, comp_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
this : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) c : ℤˣ) (1 : ℤˣ)
⊢ c.IsCycle
have hc₁ : c.IsCycle ∧ ∀ a ∈ c.support, Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
Tactic: rw [mem_cycleFactorsFinset_iff] at hc
Cleared hypotheses: hc, this
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ Odd ((card ∘ support) c)
have suffices : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) c : ℤˣ) (1 : ℤˣ)
Tactic: suffices sign c = 1 by
    rw [IsCycle.sign _, neg_eq_iff_eq_neg, ← Int.units_ne_iff_eq_neg] at this
    · rw [← Nat.not_even_iff_odd, comp_apply]
      exact fun h ↦ this h.neg_one_pow
    · rw [mem_cycleFactorsFinset_iff] at hc
      exact hc.left
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) c : ℤˣ) (1 : ℤˣ)
have a : Membership.mem (γ := Subgroup (Perm α)) (Subgroup.centralizer {g}) c
Tactic: apply h
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.centralizer {g}) c
have a : c * g = g * c
Tactic: rw [Subgroup.mem_centralizer_singleton_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
⊢ Eq.{u_1 + 1} (α := Finset (Perm α))
    (map (α := ↥(alternatingGroup α)) (Embedding.subtype fun (x : Perm α) ↦ x ∈ alternatingGroup α)
      {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = m})
    (if Even (m.sum + m.card) then {g : Perm α | g.cycleType = m} else ∅)
have pos : ∀ (hm : Even (m.sum + m.card)),
  Eq.{u_1 + 1} (α := Finset (Perm α))
    (map (α := ↥(alternatingGroup α)) (Embedding.subtype fun (x : Perm α) ↦ x ∈ alternatingGroup α)
      {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = m})
    {g : Perm α | g.cycleType = m}
Tactic: split_ifs with hm
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
pos :
  ∀ (hm : Even (m.sum + m.card)),
    Eq.{u_1 + 1} (α := Finset (Perm α))
      (map (α := ↥(alternatingGroup α)) (Embedding.subtype fun (x : Perm α) ↦ x ∈ alternatingGroup α)
        {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = m})
      {g : Perm α | g.cycleType = m}
⊢ Eq.{u_1 + 1} (α := Finset (Perm α))
    (map (α := ↥(alternatingGroup α)) (Embedding.subtype fun (x : Perm α) ↦ x ∈ alternatingGroup α)
      {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = m})
    (if Even (m.sum + m.card) then {g : Perm α | g.cycleType = m} else ∅)
have neg : ∀ (hm : ¬Even (m.sum + m.card)),
  Eq.{u_1 + 1} (α := Finset (Perm α))
    (map (α := ↥(alternatingGroup α)) (Embedding.subtype fun (x : Perm α) ↦ x ∈ alternatingGroup α)
      {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = m})
    ∅
Tactic: split_ifs with hm
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
hm : Even (m.sum + m.card)
⊢ Eq.{u_1 + 1} (α := Finset (Perm α))
    (map (α := ↥(alternatingGroup α)) (Embedding.subtype fun (x : Perm α) ↦ x ∈ alternatingGroup α)
      {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = m})
    {g : Perm α | g.cycleType = m}
have pos : ∀ (g : Perm α),
  Membership.mem (γ := Finset (Perm α))
      (map (α := ↥(alternatingGroup α)) (Embedding.subtype fun (x : Perm α) ↦ x ∈ alternatingGroup α)
        {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = m})
      g ↔
    Membership.mem (γ := Finset (Perm α)) {g : Perm α | g.cycleType = m} g
Tactic: ext g
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
hm : Even (m.sum + m.card)
g : Perm α
⊢ Membership.mem (γ := Finset (Perm α))
      (map (α := ↥(alternatingGroup α)) (Embedding.subtype fun (x : Perm α) ↦ x ∈ alternatingGroup α)
        {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = m})
      g ↔
    Membership.mem (γ := Finset (Perm α)) {g : Perm α | g.cycleType = m} g
have pos : g.cycleType = m → Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) g : ℤˣ) (1 : ℤˣ)
Tactic: simp_rw [Finset.mem_map, Finset.mem_filter_univ, Embedding.coe_subtype, Subtype.exists,
      mem_alternatingGroup, exists_and_left, exists_prop, exists_eq_right_right,
      and_iff_left_iff_imp]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
hm : Even (m.sum + m.card)
g : Perm α
hg : g.cycleType = m
⊢ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) g : ℤˣ) (1 : ℤˣ)
have pos : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) = 1
Tactic: rw [sign_of_cycleType, hg, Even.neg_one_pow hm]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
hm : Even (m.sum + m.card)
g : Perm α
hg : g.cycleType = m
pos : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) = 1
⊢ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) g : ℤˣ) (1 : ℤˣ)
have pos₁ : HPow.hPow (α := ℤˣ) (-1) (m.sum + m.card) = 1
Tactic: rw [sign_of_cycleType, hg, Even.neg_one_pow hm]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
hm : Even (m.sum + m.card)
g : Perm α
hg : g.cycleType = m
pos : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) = 1
pos₁ : HPow.hPow (α := ℤˣ) (-1) (m.sum + m.card) = 1
⊢ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) g : ℤˣ) (1 : ℤˣ)
have pos₂ : Eq (α := ℤˣ) 1 1
Tactic: rw [sign_of_cycleType, hg, Even.neg_one_pow hm]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
⊢ Eq.{u_1 + 1} (α := Finset (Perm α))
    (map (α := ↥(alternatingGroup α)) (Embedding.subtype fun (x : Perm α) ↦ x ∈ alternatingGroup α)
      {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = m})
    ∅
have neg : ∀ (x : Perm α),
  x ∉
    map (α := ↥(alternatingGroup α)) (Embedding.subtype fun (x : Perm α) ↦ x ∈ alternatingGroup α)
      {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = m}
Tactic: rw [Finset.eq_empty_iff_forall_notMem]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
g : Perm α
hg :
  Membership.mem (γ := Finset (Perm α))
    (map (α := ↥(alternatingGroup α)) (Embedding.subtype fun (x : Perm α) ↦ x ∈ alternatingGroup α)
      {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = m})
    g
⊢ False
have hg₁ : g.cycleType = m ∧ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) g : ℤˣ) (1 : ℤˣ)
Tactic: simp_rw [Finset.mem_map, Finset.mem_filter_univ, Embedding.coe_subtype, Subtype.exists,
      mem_alternatingGroup, exists_and_left, exists_prop, exists_eq_right_right] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
g : Perm α
hg : g.cycleType = m ∧ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) g : ℤˣ) (1 : ℤˣ)
⊢ False
have hg₁ : g.cycleType = m
Tactic: rcases hg with ⟨hg, hs⟩
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
g : Perm α
hg : g.cycleType = m ∧ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) g : ℤˣ) (1 : ℤˣ)
hg₁ : g.cycleType = m
⊢ False
have hs : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) g : ℤˣ) (1 : ℤˣ)
Tactic: rcases hg with ⟨hg, hs⟩
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
hm : ¬Even (m.sum + m.card)
g : Perm α
hg : g.cycleType = m
hs : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) g : ℤˣ) (1 : ℤˣ)
⊢ False
have hs₁ : Even (m.sum + m.card)
Tactic: rw [g.sign_of_cycleType, hg, neg_one_pow_eq_one_iff_even (by simp)] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
⊢ card.{u_1} (α := ↥(alternatingGroup α)) {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = m} *
      ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) =
    if (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card) then (Fintype.card α)! else 0
have rw : (if Even (m.sum + m.card) then
    card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} *
      ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
  else 0) =
  if (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card) then (Fintype.card α)! else 0
Tactic: rw [← Finset.card_map, map_subtype_of_cycleType, apply_ite Finset.card,
    Finset.card_empty, ite_mul, zero_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
⊢ (if Even (m.sum + m.card) then
      card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} *
        ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
    else 0) =
    if (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card) then (Fintype.card α)! else 0
have simp : (if Even (m.sum + m.card) then
    card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} *
      ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
  else 0) =
  if Even (m.sum + m.card) ∧ m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then (Fintype.card α)! else 0
Tactic: simp only [and_comm (b := Even _)]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
⊢ (if Even (m.sum + m.card) then
      card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} *
        ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
    else 0) =
    if Even (m.sum + m.card) ∧ m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then (Fintype.card α)! else 0
have rw : (if Even (m.sum + m.card) then
    card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} *
      ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
  else 0) =
  if Even (m.sum + m.card) then if m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then (Fintype.card α)! else 0 else 0
Tactic: rw [ite_and, Equiv.Perm.card_of_cycleType_mul_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
rw :
  (if Even (m.sum + m.card) then
      card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} *
        ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
    else 0) =
    if Even (m.sum + m.card) then if m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then (Fintype.card α)! else 0 else 0
⊢ (if Even (m.sum + m.card) then
      card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} *
        ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
    else 0) =
    if Even (m.sum + m.card) ∧ m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then (Fintype.card α)! else 0
have rw₁ : (if Even (m.sum + m.card) then if m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then (Fintype.card α)! else 0 else 0) =
  if Even (m.sum + m.card) then if m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then (Fintype.card α)! else 0 else 0
Tactic: rw [ite_and, Equiv.Perm.card_of_cycleType_mul_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
⊢ card.{u_1} (α := ↥(alternatingGroup α)) {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = m} =
    if (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card) then
      (Fintype.card α)! / ((Fintype.card α - m.sum)! * (m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!))
    else 0
have pos : ∀ (hm : (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card)),
  card.{u_1} (α := ↥(alternatingGroup α)) {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = m} =
    (Fintype.card α)! / ((Fintype.card α - m.sum)! * (m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!))
Tactic: split_ifs with hm
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
pos :
  ∀ (hm : (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card)),
    card.{u_1} (α := ↥(alternatingGroup α)) {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = m} =
      (Fintype.card α)! / ((Fintype.card α - m.sum)! * (m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!))
⊢ card.{u_1} (α := ↥(alternatingGroup α)) {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = m} =
    if (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card) then
      (Fintype.card α)! / ((Fintype.card α - m.sum)! * (m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!))
    else 0
have neg : ∀ (hm : ¬((m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card))),
  card.{u_1} (α := ↥(alternatingGroup α)) {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = m} = 0
Tactic: split_ifs with hm
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
hm : (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card)
⊢ card.{u_1} (α := ↥(alternatingGroup α)) {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = m} =
    (Fintype.card α)! / ((Fintype.card α - m.sum)! * (m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!))
have pos : card.{u_1} (α := Perm α)
    (map (α := ↥(alternatingGroup α)) (Embedding.subtype fun (x : Perm α) ↦ x ∈ alternatingGroup α)
      {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = m}) =
  (Fintype.card α)! / ((Fintype.card α - m.sum)! * (m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!))
Tactic: rw [← Finset.card_map, map_subtype_of_cycleType, if_pos hm.2,
      Equiv.Perm.card_of_cycleType α m, if_pos hm.1, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
hm : (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card)
pos :
  card.{u_1} (α := Perm α)
      (map (α := ↥(alternatingGroup α)) (Embedding.subtype fun (x : Perm α) ↦ x ∈ alternatingGroup α)
        {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = m}) =
    (Fintype.card α)! / ((Fintype.card α - m.sum)! * (m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!))
⊢ card.{u_1} (α := ↥(alternatingGroup α)) {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = m} =
    (Fintype.card α)! / ((Fintype.card α - m.sum)! * (m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!))
have pos₁ : ↥(alternatingGroup α) ↪ Perm α
Tactic: rw [← Finset.card_map, map_subtype_of_cycleType, if_pos hm.2,
      Equiv.Perm.card_of_cycleType α m, if_pos hm.1, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
hm : (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card)
pos :
  card.{u_1} (α := Perm α)
      (map (α := ↥(alternatingGroup α)) (Embedding.subtype fun (x : Perm α) ↦ x ∈ alternatingGroup α)
        {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = m}) =
    (Fintype.card α)! / ((Fintype.card α - m.sum)! * (m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!))
pos₁ : ↥(alternatingGroup α) ↪ Perm α
rw : Type u_1
⊢ card.{u_1} (α := ↥(alternatingGroup α)) {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = m} =
    (Fintype.card α)! / ((Fintype.card α - m.sum)! * (m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!))
have pos₂ : card.{u_1} (α := Perm α) (if Even (m.sum + m.card) then {g : Perm α | g.cycleType = m} else ∅) =
  (Fintype.card α)! / ((Fintype.card α - m.sum)! * (m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!))
Tactic: rw [← Finset.card_map, map_subtype_of_cycleType, if_pos hm.2,
      Equiv.Perm.card_of_cycleType α m, if_pos hm.1, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
hm : (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card)
pos :
  card.{u_1} (α := Perm α)
      (map (α := ↥(alternatingGroup α)) (Embedding.subtype fun (x : Perm α) ↦ x ∈ alternatingGroup α)
        {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = m}) =
    (Fintype.card α)! / ((Fintype.card α - m.sum)! * (m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!))
pos₁ : ↥(alternatingGroup α) ↪ Perm α
rw : Type u_1
pos₂ :
  card.{u_1} (α := Perm α) (if Even (m.sum + m.card) then {g : Perm α | g.cycleType = m} else ∅) =
    (Fintype.card α)! / ((Fintype.card α - m.sum)! * (m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!))
⊢ card.{u_1} (α := ↥(alternatingGroup α)) {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = m} =
    (Fintype.card α)! / ((Fintype.card α - m.sum)! * (m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!))
have pos₃ : card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} =
  (Fintype.card α)! / ((Fintype.card α - m.sum)! * (m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!))
Tactic: rw [← Finset.card_map, map_subtype_of_cycleType, if_pos hm.2,
      Equiv.Perm.card_of_cycleType α m, if_pos hm.1, mul_assoc]