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 α
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
⊢ 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) c hc) : Perm α).support =
  #(↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) d hd) : Perm α).support
Tactic: rw [hx', Equiv.swap_apply_right]
-- 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
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
have neg : #(↑x : Perm α).support = #(↑x : Perm α).support
Tactic: rw [Equiv.swap_apply_of_ne_of_ne hx hx']
-- 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
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
⊢ False
have hτ : 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']
-- 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
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) τ
⊢ False
have hk : 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
-- 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
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 : ℤˣ)
⊢ False
have apply : Eq (α := ℤˣ) 1 (-1)
Tactic: apply units_ne_neg_self (1 : ℤˣ)
-- 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
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 : ℤˣ)
⊢ Eq (α := ℤˣ) 1 (-1)
have rw : Eq (α := ℤˣ) (1 : ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (↑k : Perm α) : ℤˣ)
Tactic: rw [← hsign_k, h (toCentralizer a ⟨τ, hτ⟩).prop]
-- 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
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 α) : ℤˣ)
⊢ Eq (α := ℤˣ) 1 (-1)
have rw₁ : Eq (α := ℤˣ) 1 1
Tactic: rw [← hsign_k, h (toCentralizer a ⟨τ, hτ⟩).prop]
-- 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
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τ)
⊢ False
have suffices : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (↑k : Perm α) : ℤˣ) (-1 : ℤˣ)
Tactic: suffices hsign_k : k.val.sign = -1 by
    apply units_ne_neg_self (1 : ℤˣ)
    rw [← hsign_k, h (toCentralizer a ⟨τ, hτ⟩).prop]
-- 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
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
have 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}))
Tactic: rw [Multiset.eq_replicate_card, ← pow_prime_eq_one_iff, ← Subgroup.coe_pow,
      ← Subgroup.coe_one, Subtype.coe_inj, hk, ← map_pow]
-- 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
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}))
        (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}))
have h₁ : HPow.hPow (β := ℕ)
    (Subtype.mk (p := fun (x : Perm ↥g.cycleFactorsFinset) ↦
      Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (range_toPermHom' g) x) τ hτ)
    2 =
  1
Tactic: convert! MonoidHom.map_one _
-- 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
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 =
    1
have 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: rw [← Subtype.coe_inj]
-- 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
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 (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (↑k : Perm α) : ℤˣ) (-1 : ℤˣ)
have hk_cT : (↑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
-- 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
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
⊢ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (↑k : Perm α) : ℤˣ) (-1 : ℤˣ)
have rw : HPow.hPow (α := ℤˣ) (-1)
    (Multiset.sum (Multiset.replicate (↑k : Perm α).cycleType.card 2) +
      Multiset.card (α := ℕ) (Multiset.replicate (↑k : Perm α).cycleType.card 2)) =
  -1
Tactic: rw [sign_of_cycleType, hk_cT]
-- 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
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
⊢ HPow.hPow (α := ℤˣ) (-1)
      (Multiset.sum (Multiset.replicate (↑k : Perm α).cycleType.card 2) +
        Multiset.card (α := ℕ) (Multiset.replicate (↑k : Perm α).cycleType.card 2)) =
    -1
have simp : HPow.hPow (α := ℤˣ) (-1) (↑k : Perm α).cycleType.card = -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]
-- 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
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
⊢ HPow.hPow (α := ℤˣ) (-1) (↑k : Perm α).cycleType.card = -1
have h₁ : Odd (↑k : Perm α).cycleType.card
Tactic: apply Odd.neg_one_pow
-- 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
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
⊢ Odd (↑k : Perm α).cycleType.card
have h₁ : (↑k : Perm α).cycleType.card ∈ g.cycleType
Tactic: apply odd_of_centralizer_le_alternatingGroup 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
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
⊢ (↑k : Perm α).cycleType.card * 2 = #(↑k : Perm α).support
have rw : Multiset.card (α := ℕ) (Multiset.replicate (↑k : Perm α).cycleType.card 2) * 2 =
  Multiset.sum (Multiset.replicate (↑k : Perm α).cycleType.card 2)
Tactic: rw [← sum_cycleType, hk_cT]