awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
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)!))
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
⊢ 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

Tactic:
split_ifs with hm
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
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)!))
pos₆ 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)!))

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]

Premises used: mul_assoc, Finset.card_map, Equiv.Perm.card_of_cycleType, if_pos, And.right, And.left, AlternatingGroup.map_subtype_of_cycleType
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
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))
neg : card.{u_1} (α := Perm α) (if Even (m.sum + m.card) then {g : Perm α | g.cycleType = m} else ∅) = 0
⊢ card.{u_1} (α := ↥(alternatingGroup α)) {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = m} = 0

Tactic:
rw [← Finset.card_map, map_subtype_of_cycleType]

Premises used: Finset.card_map, AlternatingGroup.map_subtype_of_cycleType
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
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))
neg : (if Even (m.sum + m.card) then card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} else 0) = 0
⊢ card.{u_1} (α := Perm α) (if Even (m.sum + m.card) then {g : Perm α | g.cycleType = m} else ∅) = 0

Tactic:
rw [apply_ite Finset.card, Finset.card_empty]

Premises used: apply_ite, Finset.card_empty, Finset.card
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
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
neg : ∀ (hm' : ¬Even (m.sum + m.card)), Eq (α := ℕ) 0 0
⊢ (if Even (m.sum + m.card) then card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} else 0) = 0

Tactic:
split_ifs with hm'
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
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 : ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} = 0

Tactic:
rw [Equiv.Perm.card_of_cycleType, if_neg]

Premises used: Equiv.Perm.card_of_cycleType, if_neg
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
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)
pos₁ : ∀ (hm : ¬Even (m.sum + m.card)), ¬(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

Premises used: not_and_or, Iff.mp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
hm_1 : ¬((m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card))
hm' : Even (m.sum + m.card)
hm : ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)

Tactic:
hm
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
hm_1 : ¬((m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card))
hm' : Even (m.sum + m.card)
hm : ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
⊢ ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)

Tactic:
exact hm
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
m : Multiset ℕ
hm_1 : ¬((m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card))
hm' : Even (m.sum + m.card)
hm : ¬Even (m.sum + m.card)
⊢ ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)

Tactic:
contradiction
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
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)
⊢ Eq (α := ℕ) 0 0

Tactic:
rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
n : ℕ
hn : 2 ≤ n
hα : n ≤ Fintype.card α
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
⊢ Finset.card.{u_1} (α := ↥(alternatingGroup α)) {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {n}} =
    if Odd n then (n - 1)! * (Fintype.card α).choose n else 0

Tactic:
rw [← card_map, map_subtype_of_cycleType, apply_ite Finset.card]

Premises used: Finset.card_map, apply_ite, Finset.card, AlternatingGroup.map_subtype_of_cycleType
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
n : ℕ
hn : 2 ≤ n
hα : n ≤ Fintype.card α
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
⊢ (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:
simp only [Multiset.sum_singleton, Multiset.card_singleton, Finset.card_empty]

Premises used: Multiset.card_singleton, Multiset.sum_singleton, Finset.card_empty
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
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
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

Tactic:
simp_rw [← Nat.not_odd_iff_even, Nat.odd_add_one, not_not,
    Perm.card_of_cycleType_singleton hn hα]

Premises used: Nat.odd_add_one, Classical.not_not, Nat.not_odd_iff_even, Equiv.Perm.card_of_cycleType_singleton
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
by_contra! : ∀ (hm : g.cycleType.sum + 1 < Fintype.card α), False
⊢ Fintype.card α ≤ g.cycleType.sum + 1

Tactic:
by_contra! hm
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
hm : g.cycleType.sum + 1 < Fintype.card α
⊢ 2 + g.cycleType.sum ≤ Fintype.card α

Tactic:
lia
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
hm : g.cycleType.sum + 1 < Fintype.card α
⊢ 2 + g.cycleType.sum ≤ Fintype.card α

Tactic:
replace hm : 2 + g.cycleType.sum ≤ Fintype.card α := by lia
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
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)
obtain : ∀ (a b : (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)) (hab : a ≠ b), False
⊢ False

Tactic:
obtain ⟨a, b, hab⟩ := Fintype.exists_pair_of_one_lt_card this

Premises used: Fintype.exists_pair_of_one_lt_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
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
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 : ℤˣ)
⊢ False

Tactic:
suffices sign (kerParam g ⟨swap a b, 1⟩) ≠ 1 from
      this (h (kerParam_range_le_centralizer (Set.mem_range_self _)))
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
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
⊢ 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:
simp [sign_kerParam_apply_apply, hab]

Premises used: Equiv.Perm.OnCycleFactors.sign_kerParam_apply_apply
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
hm : 2 + g.cycleType.sum ≤ Fintype.card α
suffices : 1 < Fintype.card.{u_1} (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
⊢ False

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]
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
hm : 2 + g.cycleType.sum ≤ Fintype.card α
rwa : g.cycleType.sum ≤ Fintype.card α
⊢ 1 < Fintype.card.{u_1} (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)

Tactic:
rwa [card_fixedPoints g, Nat.lt_iff_add_one_le, Nat.le_sub_iff_add_le]

Premises used: Nat.le_sub_iff_add_le, Nat.lt_iff_add_one_le, Equiv.Perm.card_fixedPoints
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
hm : 2 + g.cycleType.sum ≤ Fintype.card α
rw : #g.support ≤ Fintype.card α
⊢ g.cycleType.sum ≤ Fintype.card α

Tactic:
rw [sum_cycleType]

Premises used: Equiv.Perm.sum_cycleType
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
hm : 2 + g.cycleType.sum ≤ Fintype.card α
⊢ #g.support ≤ Fintype.card α

Tactic:
Finset.card_le_univ _

Premises used: Finset.card_le_univ
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
hm : 2 + g.cycleType.sum ≤ Fintype.card α
⊢ #g.support ≤ Fintype.card α

Tactic:
exact Finset.card_le_univ _

Premises used: Finset.card_le_univ
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
rw : (Multiset.map (card ∘ support) g.cycleFactorsFinset.val).Nodup
⊢ ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1

Tactic:
rw [← Multiset.nodup_iff_count_le_one, Equiv.Perm.cycleType_def]

Premises used: Multiset.nodup_iff_count_le_one, Equiv.Perm.cycleType_def
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
rw : ∀ x ∈ g.cycleFactorsFinset.val, ∀ y ∈ g.cycleFactorsFinset.val, (card ∘ support) x = (card ∘ support) y → x = y
⊢ (Multiset.map (card ∘ support) g.cycleFactorsFinset.val).Nodup

Tactic:
rw [Multiset.nodup_map_iff_inj_on g.cycleFactorsFinset.nodup]

Premises used: Equiv.Perm.cycleFactorsFinset, Finset.nodup, Multiset.nodup_map_iff_inj_on
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
simp : ∀ x ∈ g.cycleFactorsFinset, ∀ y ∈ g.cycleFactorsFinset, #x.support = #y.support → x = y
⊢ ∀ x ∈ g.cycleFactorsFinset.val, ∀ y ∈ g.cycleFactorsFinset.val, (card ∘ support) x = (card ∘ support) y → x = y

Tactic:
simp only [Function.comp_apply, ← Finset.mem_def]

Premises used: Function.comp_apply, Finset.mem_def
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
by_contra! :
  ∀ (c : Perm α) (hc : c ∈ g.cycleFactorsFinset) (d : Perm α) (hd : d ∈ g.cycleFactorsFinset)
    (hm : #c.support = #d.support) (hm' : c ≠ d), False
⊢ ∀ x ∈ g.cycleFactorsFinset, ∀ y ∈ g.cycleFactorsFinset, #x.support = #y.support → x = y

Tactic:
by_contra! ⟨c, hc, d, hd, hm, hm'⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
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)
obtain : ∀ (a : g.Basis), False
⊢ False

Tactic:
obtain ⟨a⟩ := Equiv.Perm.Basis.nonempty g

Premises used: Equiv.Perm.Basis.nonempty
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
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
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
⊢ card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) x) : Perm α)) =
    #(↑x : Perm α).support

Tactic:
by_cases hx : x = ⟨c, hc⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
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 :
  #(↑(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
⊢ card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) x) : Perm α)) =
    #(↑x : Perm α).support

Tactic:
rw [hx, Equiv.swap_apply_left]

Premises used: Equiv.swap_apply_left
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
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
⊢ #(↑(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:
hm.symm

Premises used: Eq.symm
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
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
⊢ #(↑(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:
exact hm.symm

Premises used: Eq.symm
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
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
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
⊢ card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) x) : Perm α)) =
    #(↑x : Perm α).support

Tactic:
by_cases hx' : x = ⟨d, hd⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
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
hx' : x = Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) d hd
pos :
  #(↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc) : Perm α).support =
    #(↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) d hd) : Perm α).support
⊢ card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) x) : Perm α)) =
    #(↑x : Perm α).support

Tactic:
rw [hx', Equiv.swap_apply_right]

Premises used: Equiv.swap_apply_right