awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ #(↑(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

Tactic:
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)
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
⊢ #(↑(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

Tactic:
exact 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)
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
neg neg₁ : #(↑x : Perm α).support = #(↑x : Perm α).support
⊢ card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) x) : Perm α)) =
    #(↑x : Perm α).support

Tactic:
rw [Equiv.swap_apply_of_ne_of_ne hx hx']

Premises used: Equiv.swap_apply_of_ne_of_ne
-- 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
⊢ Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) τ

Tactic:
have hτ : τ ∈ range_toPermHom' g := fun x ↦ by
    by_cases hx : x = ⟨c, hc⟩
    · rw [hx, Equiv.swap_apply_left]; exact hm.symm
    by_cases hx' : x = ⟨d, hd⟩
    · rw [hx', Equiv.swap_apply_right]; exact hm
    · rw [Equiv.swap_apply_of_ne_of_ne hx hx']
-- 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
hτ : Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) τ
⊢ let k : ↥(Subgroup.centralizer {g}) :=
    (a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(Subgroup.centralizer {g}))
      (Subtype.mk (p := fun (x : Perm ↥g.cycleFactorsFinset) ↦
        Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) x) τ hτ);
  k =
    (a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(Subgroup.centralizer {g}))
      (Subtype.mk (p := fun (x : Perm ↥g.cycleFactorsFinset) ↦
        Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) x) τ hτ)

Tactic:
set k := toCentralizer a ⟨τ, hτ⟩ with hk

Premises used: Subtype.mk, Equiv.Perm.Basis.toCentralizer, DFunLike.coe
-- 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
hτ : Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) τ
k : ↥(Subgroup.centralizer {g}) :=
  (a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(Subgroup.centralizer {g}))
    (Subtype.mk (p := fun (x : Perm ↥g.cycleFactorsFinset) ↦
      Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) x) τ hτ)
hk :
  k =
    (a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(Subgroup.centralizer {g}))
      (Subtype.mk (p := fun (x : Perm ↥g.cycleFactorsFinset) ↦
        Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) x) τ hτ)
hsign_k : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (↑k : Perm α) : ℤˣ) (-1 : ℤˣ)
apply : Eq (α := ℤˣ) 1 (-1)
⊢ False

Tactic:
apply units_ne_neg_self (1 : ℤˣ)

Premises used: units_ne_neg_self, OfNat.ofNat
-- 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
hτ : Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) τ
k : ↥(Subgroup.centralizer {g}) :=
  (a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(Subgroup.centralizer {g}))
    (Subtype.mk (p := fun (x : Perm ↥g.cycleFactorsFinset) ↦
      Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) x) τ hτ)
hk :
  k =
    (a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(Subgroup.centralizer {g}))
      (Subtype.mk (p := fun (x : Perm ↥g.cycleFactorsFinset) ↦
        Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) x) τ hτ)
hsign_k : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (↑k : Perm α) : ℤˣ) (-1 : ℤˣ)
rw : Eq (α := ℤˣ) (1 : ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (↑k : Perm α) : ℤˣ)
rw₁ rw₂ : Eq (α := ℤˣ) 1 1
⊢ Eq (α := ℤˣ) 1 (-1)

Tactic:
rw [← hsign_k, h (toCentralizer a ⟨τ, hτ⟩).prop]

Premises used: Subtype.mk, Equiv.Perm.Basis.toCentralizer, Subtype.prop, DFunLike.coe
-- 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
hτ : Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) τ
k : ↥(Subgroup.centralizer {g}) :=
  (a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(Subgroup.centralizer {g}))
    (Subtype.mk (p := fun (x : Perm ↥g.cycleFactorsFinset) ↦
      Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) x) τ hτ)
hk :
  k =
    (a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(Subgroup.centralizer {g}))
      (Subtype.mk (p := fun (x : Perm ↥g.cycleFactorsFinset) ↦
        Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) x) τ hτ)
suffices : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (↑k : Perm α) : ℤˣ) (-1 : ℤˣ)
⊢ False

Tactic:
suffices hsign_k : k.val.sign = -1 by
    apply units_ne_neg_self (1 : ℤˣ)
    rw [← hsign_k, h (toCentralizer a ⟨τ, hτ⟩).prop]
-- 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
hτ : Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) τ
k : ↥(Subgroup.centralizer {g}) :=
  (a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(Subgroup.centralizer {g}))
    (Subtype.mk (p := fun (x : Perm ↥g.cycleFactorsFinset) ↦
      Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) x) τ hτ)
hk :
  k =
    (a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(Subgroup.centralizer {g}))
      (Subtype.mk (p := fun (x : Perm ↥g.cycleFactorsFinset) ↦
        Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) x) τ hτ)
rw :
  Eq (α := ↥(Subgroup.centralizer {g}))
    ((a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(Subgroup.centralizer {g}))
        (HPow.hPow (β := ℕ)
          (Subtype.mk (p := fun (x : Perm ↥g.cycleFactorsFinset) ↦
            Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) x) τ hτ)
          2) :
      ↥(Subgroup.centralizer {g}))
    (1 : ↥(Subgroup.centralizer {g}))
⊢ (↑k : Perm α).cycleType = Multiset.replicate (↑k : Perm α).cycleType.card 2

Tactic:
rw [Multiset.eq_replicate_card, ← pow_prime_eq_one_iff, ← Subgroup.coe_pow,
      ← Subgroup.coe_one, Subtype.coe_inj, hk, ← map_pow]

Premises used: Subtype.coe_inj, Subgroup.coe_pow, map_pow, Subgroup.coe_one, Equiv.Perm.pow_prime_eq_one_iff, Multiset.eq_replicate_card
-- 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
hτ : Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) τ
k : ↥(Subgroup.centralizer {g}) :=
  (a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(Subgroup.centralizer {g}))
    (Subtype.mk (p := fun (x : Perm ↥g.cycleFactorsFinset) ↦
      Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) x) τ hτ)
hk :
  k =
    (a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(Subgroup.centralizer {g}))
      (Subtype.mk (p := fun (x : Perm ↥g.cycleFactorsFinset) ↦
        Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) x) τ hτ)
⊢ Eq (α := ↥(Subgroup.centralizer {g}))
    ((a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(Subgroup.centralizer {g})) 1) 1

Tactic:
MonoidHom.map_one _

Premises used: MonoidHom.map_one
-- 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
hτ : Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) τ
k : ↥(Subgroup.centralizer {g}) :=
  (a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(Subgroup.centralizer {g}))
    (Subtype.mk (p := fun (x : Perm ↥g.cycleFactorsFinset) ↦
      Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) x) τ hτ)
hk :
  k =
    (a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(Subgroup.centralizer {g}))
      (Subtype.mk (p := fun (x : Perm ↥g.cycleFactorsFinset) ↦
        Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) x) τ hτ)
h₁ :
  HPow.hPow (β := ℕ)
      (Subtype.mk (p := fun (x : Perm ↥g.cycleFactorsFinset) ↦
        Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) x) τ hτ)
      2 =
    1
⊢ Eq (α := ↥(Subgroup.centralizer {g}))
    ((a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(Subgroup.centralizer {g}))
        (HPow.hPow (β := ℕ)
          (Subtype.mk (p := fun (x : Perm ↥g.cycleFactorsFinset) ↦
            Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) x) τ hτ)
          2) :
      ↥(Subgroup.centralizer {g}))
    (1 : ↥(Subgroup.centralizer {g}))

Tactic:
convert! MonoidHom.map_one _

Premises used: MonoidHom.map_one
-- 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
hτ : Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) τ
k : ↥(Subgroup.centralizer {g}) :=
  (a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(Subgroup.centralizer {g}))
    (Subtype.mk (p := fun (x : Perm ↥g.cycleFactorsFinset) ↦
      Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) x) τ hτ)
hk :
  k =
    (a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(Subgroup.centralizer {g}))
      (Subtype.mk (p := fun (x : Perm ↥g.cycleFactorsFinset) ↦
        Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) x) τ hτ)
h₁ :
  (↑(HPow.hPow (β := ℕ)
          (Subtype.mk (p := fun (x : Perm ↥g.cycleFactorsFinset) ↦
            Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) x) τ hτ)
          2) :
      Perm ↥g.cycleFactorsFinset) =
    (↑1 : Perm ↥g.cycleFactorsFinset)
⊢ HPow.hPow (β := ℕ)
      (Subtype.mk (p := fun (x : Perm ↥g.cycleFactorsFinset) ↦
        Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) x) τ hτ)
      2 =
    1

Tactic:
rw [← Subtype.coe_inj]

Premises used: Subtype.coe_inj
-- 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
hτ : Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) τ
k : ↥(Subgroup.centralizer {g}) :=
  (a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(Subgroup.centralizer {g}))
    (Subtype.mk (p := fun (x : Perm ↥g.cycleFactorsFinset) ↦
      Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) x) τ hτ)
hk :
  k =
    (a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(Subgroup.centralizer {g}))
      (Subtype.mk (p := fun (x : Perm ↥g.cycleFactorsFinset) ↦
        Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) x) τ hτ)
⊢ (↑(HPow.hPow (β := ℕ)
          (Subtype.mk (p := fun (x : Perm ↥g.cycleFactorsFinset) ↦
            Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) x) τ hτ)
          2) :
      Perm ↥g.cycleFactorsFinset) =
    (↑1 : Perm ↥g.cycleFactorsFinset)

Tactic:
apply Equiv.swap_mul_self

Premises used: Equiv.swap_mul_self
-- 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
hτ : Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) τ
k : ↥(Subgroup.centralizer {g}) :=
  (a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(Subgroup.centralizer {g}))
    (Subtype.mk (p := fun (x : Perm ↥g.cycleFactorsFinset) ↦
      Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) x) τ hτ)
hk :
  k =
    (a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(Subgroup.centralizer {g}))
      (Subtype.mk (p := fun (x : Perm ↥g.cycleFactorsFinset) ↦
        Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) x) τ hτ)
⊢ (↑k : Perm α).cycleType = Multiset.replicate (↑k : Perm α).cycleType.card 2

Tactic:
have hk_cT : k.val.cycleType = Multiset.replicate k.val.cycleType.card 2 := by
    rw [Multiset.eq_replicate_card, ← pow_prime_eq_one_iff, ← Subgroup.coe_pow,
      ← Subgroup.coe_one, Subtype.coe_inj, hk, ← map_pow]
    convert! MonoidHom.map_one _
    rw [← Subtype.coe_inj]
    apply Equiv.swap_mul_self
-- 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
hτ : Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) τ
k : ↥(Subgroup.centralizer {g}) :=
  (a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(Subgroup.centralizer {g}))
    (Subtype.mk (p := fun (x : Perm ↥g.cycleFactorsFinset) ↦
      Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) x) τ hτ)
hk :
  k =
    (a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(Subgroup.centralizer {g}))
      (Subtype.mk (p := fun (x : Perm ↥g.cycleFactorsFinset) ↦
        Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) x) τ hτ)
hk_cT : (↑k : Perm α).cycleType = Multiset.replicate (↑k : Perm α).cycleType.card 2
rw :
  HPow.hPow (α := ℤˣ) (-1)
      (Multiset.sum (Multiset.replicate (↑k : Perm α).cycleType.card 2) +
        Multiset.card (α := ℕ) (Multiset.replicate (↑k : Perm α).cycleType.card 2)) =
    -1
⊢ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (↑k : Perm α) : ℤˣ) (-1 : ℤˣ)

Tactic:
rw [sign_of_cycleType, hk_cT]

Premises used: Equiv.Perm.sign_of_cycleType
-- 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
hτ : Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) τ
k : ↥(Subgroup.centralizer {g}) :=
  (a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(Subgroup.centralizer {g}))
    (Subtype.mk (p := fun (x : Perm ↥g.cycleFactorsFinset) ↦
      Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) x) τ hτ)
hk :
  k =
    (a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(Subgroup.centralizer {g}))
      (Subtype.mk (p := fun (x : Perm ↥g.cycleFactorsFinset) ↦
        Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) x) τ hτ)
hk_cT : (↑k : Perm α).cycleType = Multiset.replicate (↑k : Perm α).cycleType.card 2
simp : HPow.hPow (α := ℤˣ) (-1) (↑k : Perm α).cycleType.card = -1
⊢ HPow.hPow (α := ℤˣ) (-1)
      (Multiset.sum (Multiset.replicate (↑k : Perm α).cycleType.card 2) +
        Multiset.card (α := ℕ) (Multiset.replicate (↑k : Perm α).cycleType.card 2)) =
    -1

Tactic:
simp only [Multiset.sum_replicate, smul_eq_mul, Multiset.card_replicate, pow_add,
    even_two, Even.mul_left, Even.neg_pow, one_pow, one_mul]

Premises used: one_pow, even_two, Multiset.card_replicate, Even.neg_pow, pow_add, Even.mul_left, Multiset.sum_replicate, smul_eq_mul, one_mul
-- 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
hτ : Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) τ
k : ↥(Subgroup.centralizer {g}) :=
  (a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(Subgroup.centralizer {g}))
    (Subtype.mk (p := fun (x : Perm ↥g.cycleFactorsFinset) ↦
      Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) x) τ hτ)
hk :
  k =
    (a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(Subgroup.centralizer {g}))
      (Subtype.mk (p := fun (x : Perm ↥g.cycleFactorsFinset) ↦
        Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) x) τ hτ)
hk_cT : (↑k : Perm α).cycleType = Multiset.replicate (↑k : Perm α).cycleType.card 2
h₁ : Odd (↑k : Perm α).cycleType.card
⊢ HPow.hPow (α := ℤˣ) (-1) (↑k : Perm α).cycleType.card = -1

Tactic:
apply Odd.neg_one_pow

Premises used: Odd.neg_one_pow