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
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₁ : (↑k : Perm α).cycleType.card ∈ g.cycleType
⊢ Odd (↑k : Perm α).cycleType.card

Tactic:
apply odd_of_centralizer_le_alternatingGroup h

Premises used: Equiv.Perm.OnCycleFactors.odd_of_centralizer_le_alternatingGroup
-- 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 :
  Multiset.card (α := ℕ) (Multiset.replicate (↑k : Perm α).cycleType.card 2) * 2 =
    Multiset.sum (Multiset.replicate (↑k : Perm α).cycleType.card 2)
⊢ (↑k : Perm α).cycleType.card * 2 = #(↑k : Perm α).support

Tactic:
rw [← sum_cycleType, hk_cT]

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 α
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
⊢ Multiset.card (α := ℕ) (Multiset.replicate (↑k : Perm α).cycleType.card 2) * 2 =
    Multiset.sum (Multiset.replicate (↑k : Perm α).cycleType.card 2)

Tactic:
simp
-- 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
⊢ (↑k : Perm α).cycleType.card * 2 = #(↑k : Perm α).support

Tactic:
have this : (k : Perm α).cycleType.card * 2 = (k : Perm α).support.card := by
    rw [← sum_cycleType, hk_cT]
    simp
-- 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
this : (↑k : Perm α).cycleType.card * 2 = #(↑k : Perm α).support
⊢ Ne (α := ℕ) 2 0

Tactic:
simp
-- 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
this : (↑k : Perm α).cycleType.card * 2 = #(↑k : Perm α).support
rw : #(↑k : Perm α).support = #c.support * 2
⊢ (↑k : Perm α).cycleType.card = #c.support

Tactic:
rw [← Nat.mul_left_inj (a := 2) (by simp), this]

Premises used: Nat.mul_left_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τ)
hk_cT : (↑k : Perm α).cycleType = Multiset.replicate (↑k : Perm α).cycleType.card 2
this : (↑k : Perm α).cycleType.card * 2 = #(↑k : Perm α).support
simp : ∑ c ∈ τ.support, #(↑c : Perm α).support = #c.support * 2
⊢ #(↑k : Perm α).support = #c.support * 2

Tactic:
simp only [hk, toCentralizer, MonoidHom.coe_mk, OneHom.coe_mk, card_ofPermHom_support]

Premises used: OneHom.coe_mk, Equiv.Perm.Basis.card_ofPermHom_support, Equiv.Perm.Basis.toCentralizer, MonoidHom.coe_mk
-- 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
this : (↑k : Perm α).cycleType.card * 2 = #(↑k : Perm α).support
⊢ Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc ≠
    Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) d hd

Tactic:
have H : (⟨c, hc⟩ : g.cycleFactorsFinset) ≠ ⟨d, hd⟩ := Subtype.coe_ne_coe.mp 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
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
this : (↑k : Perm α).cycleType.card * 2 = #(↑k : Perm α).support
H :
  Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc ≠
    Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) d hd
simp :
  ∑
      x ∈
        {Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc,
          Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) d hd},
      #(↑x : Perm α).support =
    #c.support * 2
⊢ ∑ c ∈ τ.support, #(↑c : Perm α).support = #c.support * 2

Tactic:
simp only [τ, support_swap H]

Premises used: Equiv.Perm.support_swap
-- 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
this : (↑k : Perm α).cycleType.card * 2 = #(↑k : Perm α).support
H :
  Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc ≠
    Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) d hd
⊢ Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc ∉
    {Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) d hd}

Tactic:
simp only [mem_singleton, H, not_false_eq_true]

Premises used: Finset.mem_singleton, not_false_eq_true
-- 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
this : (↑k : Perm α).cycleType.card * 2 = #(↑k : Perm α).support
H :
  Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc ≠
    Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) d hd
rw :
  #(↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc) : Perm α).support +
      ∑ x ∈ {Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) d hd}, #(↑x : Perm α).support =
    #c.support * 2
rw₁ :
  #(↑(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 =
    #c.support * 2
rw₂ :
  #d.support + #(↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) d hd) : Perm α).support =
    #d.support * 2
rw₃ rw₄ :
  #d.support + #(↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) d hd) : Perm α).support =
    #d.support + #d.support
⊢ ∑
      x ∈
        {Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc,
          Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) d hd},
      #(↑x : Perm α).support =
    #c.support * 2

Tactic:
rw [Finset.sum_insert (by simp only [mem_singleton, H, not_false_eq_true]),
      Finset.sum_singleton, hm, mul_two]

Premises used: Finset.sum_singleton, Finset.sum_insert, mul_two
-- 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
this : (↑k : Perm α).cycleType.card * 2 = #(↑k : Perm α).support
that : (↑k : Perm α).cycleType.card = #c.support
h₁ : #c.support ∈ g.cycleType
⊢ (↑k : Perm α).cycleType.card ∈ g.cycleType

Tactic:
rw [that]
-- 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
this : (↑k : Perm α).cycleType.card * 2 = #(↑k : Perm α).support
that : (↑k : Perm α).cycleType.card = #c.support
h₁ : ∃ a ∈ g.cycleFactorsFinset.val, (card ∘ support) a = #c.support
⊢ #c.support ∈ g.cycleType

Tactic:
simp only [cycleType_def, Multiset.mem_map]

Premises used: Multiset.mem_map, 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 α
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
this : (↑k : Perm α).cycleType.card * 2 = #(↑k : Perm α).support
that : (↑k : Perm α).cycleType.card = #c.support
⊢ (card ∘ support) c = #c.support

Tactic:
simp only [Function.comp_apply]

Premises used: Function.comp_apply
-- 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
this : (↑k : Perm α).cycleType.card * 2 = #(↑k : Perm α).support
that : (↑k : Perm α).cycleType.card = #c.support
⊢ ∃ a ∈ g.cycleFactorsFinset.val, (card ∘ support) a = #c.support

Tactic:
exact ⟨c, hc, by simp only [Function.comp_apply]⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
h :
  ∀ (x : Perm α),
    x ∈
        MonoidHom.range (G :=
          Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
            ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))))
          (kerParam g) ↔
      Membership.mem (γ := Subgroup (Perm α)) (Subgroup.centralizer {g}) x
⊢ MonoidHom.range (G :=
      Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
        ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))))
      (kerParam g) =
    Subgroup.centralizer {g}

Tactic:
ext x