awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)!))
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)!))
⊢ 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₄ : (if m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then
    (Fintype.card α)! / ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
  else 0) =
  (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)!))
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)!))
pos₄ :
  (if m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then
      (Fintype.card α)! / ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
    else 0) =
    (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₅ : (Fintype.card α)! / ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n 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)!))
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)!))
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)!))
pos₄ :
  (if m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then
      (Fintype.card α)! / ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
    else 0) =
    (Fintype.card α)! / ((Fintype.card α - m.sum)! * (m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!))
pos₅ :
  (Fintype.card α)! / ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n 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₆ : (Fintype.card α)! / ((Fintype.card α - m.sum)! * (m.prod * ∏ n ∈ m.toFinset, (Multiset.count n 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))
⊢ card.{u_1} (α := ↥(alternatingGroup α)) {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = m} = 0
have neg : card.{u_1} (α := Perm α) (if Even (m.sum + m.card) then {g : Perm α | g.cycleType = m} else ∅) = 0
Tactic: rw [← Finset.card_map, map_subtype_of_cycleType]
-- 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} (α := Perm α) (if Even (m.sum + m.card) then {g : Perm α | g.cycleType = m} else ∅) = 0
have neg : (if Even (m.sum + m.card) then card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} else 0) = 0
Tactic: rw [apply_ite Finset.card, Finset.card_empty]
-- 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))
⊢ (if Even (m.sum + m.card) then card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} else 0) = 0
have pos : ∀ (hm' : Even (m.sum + m.card)), card.{u_1} (α := Perm α) {g : Perm α | g.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))
pos : ∀ (hm' : Even (m.sum + m.card)), card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} = 0
⊢ (if Even (m.sum + m.card) then card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} else 0) = 0
have neg : ∀ (hm' : ¬Even (m.sum + m.card)), Eq (α := ℕ) 0 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))
hm' : Even (m.sum + m.card)
⊢ card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} = 0
have pos : ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
Tactic: rw [Equiv.Perm.card_of_cycleType, if_neg]
-- 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))
hm' : Even (m.sum + m.card)
⊢ ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
have pos : ∀ (hm : ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)), ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
Tactic: obtain hm | hm := not_and_or.mp 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))
hm' : Even (m.sum + m.card)
pos : ∀ (hm : ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)), ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
have pos₁ : ∀ (hm : ¬Even (m.sum + m.card)), ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
Tactic: obtain hm | hm := not_and_or.mp hm
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
n : ℕ
hn : 2 ≤ n
hα : n ≤ Fintype.card α
⊢ Finset.card.{u_1} (α := ↥(alternatingGroup α)) {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {n}} =
    if Odd n then (n - 1)! * (Fintype.card α).choose n else 0
have rw : (if Even (Multiset.sum {n} + Multiset.card (α := ℕ) {n}) then
    Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = {n}}
  else Finset.card.{u_1} (α := Perm α) ∅) =
  if Odd n then (n - 1)! * (Fintype.card α).choose n else 0
Tactic: rw [← card_map, map_subtype_of_cycleType, apply_ite Finset.card]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
n : ℕ
hn : 2 ≤ n
hα : n ≤ Fintype.card α
⊢ (if Even (Multiset.sum {n} + Multiset.card (α := ℕ) {n}) then
      Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = {n}}
    else Finset.card.{u_1} (α := Perm α) ∅) =
    if Odd n then (n - 1)! * (Fintype.card α).choose n else 0
have simp : (if Even (n + 1) then Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = {n}} else 0) =
  if Odd n then (n - 1)! * (Fintype.card α).choose n else 0
Tactic: simp only [Multiset.sum_singleton, Multiset.card_singleton, Finset.card_empty]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
n : ℕ
hn : 2 ≤ n
hα : n ≤ Fintype.card α
⊢ (if Even (n + 1) then Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = {n}} else 0) =
    if Odd n then (n - 1)! * (Fintype.card α).choose n else 0
have simp_rw : (if ¬Odd (n + 1) then Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = {n}} else 0) =
  if Odd n then (n - 1)! * (Fintype.card α).choose n else 0
Tactic: simp_rw [← Nat.not_odd_iff_even, Nat.odd_add_one, not_not,
    Perm.card_of_cycleType_singleton hn hα]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
n : ℕ
hn : 2 ≤ n
hα : n ≤ Fintype.card α
simp_rw :
  (if ¬Odd (n + 1) then Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = {n}} else 0) =
    if Odd n then (n - 1)! * (Fintype.card α).choose n else 0
⊢ (if Even (n + 1) then Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = {n}} else 0) =
    if Odd n then (n - 1)! * (Fintype.card α).choose n else 0
have simp_rw₁ : (if ¬¬Odd n then Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = {n}} else 0) =
  if Odd n then (n - 1)! * (Fintype.card α).choose n else 0
Tactic: simp_rw [← Nat.not_odd_iff_even, Nat.odd_add_one, not_not,
    Perm.card_of_cycleType_singleton hn hα]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
n : ℕ
hn : 2 ≤ n
hα : n ≤ Fintype.card α
simp_rw :
  (if ¬Odd (n + 1) then Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = {n}} else 0) =
    if Odd n then (n - 1)! * (Fintype.card α).choose n else 0
simp_rw₁ :
  (if ¬¬Odd n then Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = {n}} else 0) =
    if Odd n then (n - 1)! * (Fintype.card α).choose n else 0
⊢ (if Even (n + 1) then Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = {n}} else 0) =
    if Odd n then (n - 1)! * (Fintype.card α).choose n else 0
have simp_rw₂ : (if Odd n then Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = {n}} else 0) =
  if Odd n then (n - 1)! * (Fintype.card α).choose n else 0
Tactic: simp_rw [← Nat.not_odd_iff_even, Nat.odd_add_one, not_not,
    Perm.card_of_cycleType_singleton hn 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 α
⊢ Fintype.card α ≤ g.cycleType.sum + 1
have by_contra! : ∀ (hm : g.cycleType.sum + 1 < Fintype.card α), False
Tactic: by_contra! hm
-- 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 α
hm : g.cycleType.sum + 1 < Fintype.card α
⊢ False
have hm₁ : 2 + g.cycleType.sum ≤ Fintype.card α
Tactic: replace hm : 2 + g.cycleType.sum ≤ Fintype.card α := by lia
Cleared hypotheses: hm
-- 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 α
hm : 2 + g.cycleType.sum ≤ Fintype.card α
this : 1 < Fintype.card.{u_1} (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
⊢ False
have obtain : ∀ (a b : (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)) (hab : a ≠ b), False
Tactic: obtain ⟨a, b, hab⟩ := Fintype.exists_pair_of_one_lt_card 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 α
hm : 2 + g.cycleType.sum ≤ Fintype.card α
this : 1 < Fintype.card.{u_1} (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
a b : (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
hab : a ≠ b
⊢ False
have suffices : Ne (α := ℤˣ)
  (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ)
      ((kerParam g :
          (a :
              Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
                ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α)))) →
            Perm α)
        (swap a b, 1)) :
    ℤˣ)
  (1 : ℤˣ)
Tactic: suffices sign (kerParam g ⟨swap a b, 1⟩) ≠ 1 from
      this (h (kerParam_range_le_centralizer (Set.mem_range_self _)))
-- 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 α
hm : 2 + g.cycleType.sum ≤ Fintype.card α
⊢ False
have suffices : 1 < Fintype.card.{u_1} (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
Tactic: suffices 1 < Fintype.card (Function.fixedPoints g) by
    obtain ⟨a, b, hab⟩ := Fintype.exists_pair_of_one_lt_card this
    suffices sign (kerParam g ⟨swap a b, 1⟩) ≠ 1 from
      this (h (kerParam_range_le_centralizer (Set.mem_range_self _)))
    simp [sign_kerParam_apply_apply, hab]
-- 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 α
hm : 2 + g.cycleType.sum ≤ Fintype.card α
⊢ 1 < Fintype.card.{u_1} (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
have rwa : g.cycleType.sum ≤ Fintype.card α
Tactic: rwa [card_fixedPoints g, Nat.lt_iff_add_one_le, Nat.le_sub_iff_add_le]
-- 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 α
hm : 2 + g.cycleType.sum ≤ Fintype.card α
⊢ g.cycleType.sum ≤ Fintype.card α
have rw : #g.support ≤ Fintype.card α
Tactic: rw [sum_cycleType]
-- 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 : ℕ), Multiset.count i g.cycleType ≤ 1
have rw : (Multiset.map (card ∘ support) g.cycleFactorsFinset.val).Nodup
Tactic: rw [← Multiset.nodup_iff_count_le_one, Equiv.Perm.cycleType_def]
-- 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 α
⊢ (Multiset.map (card ∘ support) g.cycleFactorsFinset.val).Nodup
have rw : ∀ x ∈ g.cycleFactorsFinset.val, ∀ y ∈ g.cycleFactorsFinset.val, (card ∘ support) x = (card ∘ support) y → x = y
Tactic: rw [Multiset.nodup_map_iff_inj_on g.cycleFactorsFinset.nodup]
-- 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 α
⊢ ∀ x ∈ g.cycleFactorsFinset.val, ∀ y ∈ g.cycleFactorsFinset.val, (card ∘ support) x = (card ∘ support) y → x = y
have simp : ∀ x ∈ g.cycleFactorsFinset, ∀ y ∈ g.cycleFactorsFinset, #x.support = #y.support → x = y
Tactic: simp only [Function.comp_apply, ← Finset.mem_def]
-- 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 α
⊢ ∀ x ∈ g.cycleFactorsFinset, ∀ y ∈ g.cycleFactorsFinset, #x.support = #y.support → x = y
have by_contra! : ∀ (c : Perm α) (hc : c ∈ g.cycleFactorsFinset) (d : Perm α) (hd : d ∈ g.cycleFactorsFinset)
  (hm : #c.support = #d.support) (hm' : c ≠ d), False
Tactic: by_contra! ⟨c, hc, d, hd, hm, hm'⟩
-- 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
d : Perm α
hd : d ∈ g.cycleFactorsFinset
hm : #c.support = #d.support
hm' : c ≠ d
τ : Perm ↥g.cycleFactorsFinset :=
  swap (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) d hd)
⊢ False
have obtain : ∀ (a : g.Basis), False
Tactic: obtain ⟨a⟩ := Equiv.Perm.Basis.nonempty g
-- 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
d : Perm α
hd : d ∈ g.cycleFactorsFinset
hm : #c.support = #d.support
hm' : c ≠ d
τ : Perm ↥g.cycleFactorsFinset :=
  swap (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) d hd)
a : g.Basis
x : ↥g.cycleFactorsFinset
⊢ card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) x) : Perm α)) =
    #(↑x : Perm α).support
have pos : ∀ (hx : x = Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc),
  card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) x) : Perm α)) =
    #(↑x : Perm α).support
Tactic: by_cases hx : x = ⟨c, 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
d : Perm α
hd : d ∈ g.cycleFactorsFinset
hm : #c.support = #d.support
hm' : c ≠ d
τ : Perm ↥g.cycleFactorsFinset :=
  swap (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) d hd)
a : g.Basis
x : ↥g.cycleFactorsFinset
pos :
  ∀ (hx : x = Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc),
    card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) x) : Perm α)) =
      #(↑x : Perm α).support
⊢ card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) x) : Perm α)) =
    #(↑x : Perm α).support
have neg : ∀ (hx : ¬x = Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc),
  card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) x) : Perm α)) =
    #(↑x : Perm α).support
Tactic: by_cases hx : x = ⟨c, 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
d : Perm α
hd : d ∈ g.cycleFactorsFinset
hm : #c.support = #d.support
hm' : c ≠ d
τ : Perm ↥g.cycleFactorsFinset :=
  swap (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) d hd)
a : g.Basis
x : ↥g.cycleFactorsFinset
hx : x = Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc
⊢ card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) x) : Perm α)) =
    #(↑x : Perm α).support
have pos : #(↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) d hd) : Perm α).support =
  #(↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc) : Perm α).support
Tactic: rw [hx, Equiv.swap_apply_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
d : Perm α
hd : d ∈ g.cycleFactorsFinset
hm : #c.support = #d.support
hm' : c ≠ d
τ : Perm ↥g.cycleFactorsFinset :=
  swap (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) d hd)
a : g.Basis
x : ↥g.cycleFactorsFinset
hx : ¬x = Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc
⊢ card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) x) : Perm α)) =
    #(↑x : Perm α).support
have pos : ∀ (hx' : x = Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) d hd),
  card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) x) : Perm α)) =
    #(↑x : Perm α).support
Tactic: by_cases hx' : x = ⟨d, hd⟩
-- 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
d : Perm α
hd : d ∈ g.cycleFactorsFinset
hm : #c.support = #d.support
hm' : c ≠ d
τ : Perm ↥g.cycleFactorsFinset :=
  swap (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) d hd)
a : g.Basis
x : ↥g.cycleFactorsFinset
hx : ¬x = Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc
pos :
  ∀ (hx' : x = Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) d hd),
    card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) x) : Perm α)) =
      #(↑x : Perm α).support
⊢ card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) x) : Perm α)) =
    #(↑x : Perm α).support
have neg : ∀ (hx' : ¬x = Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) d hd),
  card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) x) : Perm α)) =
    #(↑x : Perm α).support
Tactic: by_cases hx' : x = ⟨d, hd⟩