awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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τ)
hk_cT : (↑k : Perm α).cycleType = Multiset.replicate (↑k : Perm α).cycleType.card 2
⊢ (↑k : Perm α).cycleType.card ∈ g.cycleType
have this : (↑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
-- 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
this : (↑k : Perm α).cycleType.card * 2 = #(↑k : Perm α).support
⊢ (↑k : Perm α).cycleType.card = #c.support
have rw : #(↑k : Perm α).support = #c.support * 2
Tactic: rw [← Nat.mul_left_inj (a := 2) (by simp), this]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
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
⊢ #(↑k : Perm α).support = #c.support * 2
have simp : ∑ c ∈ τ.support, #(↑c : Perm α).support = #c.support * 2
Tactic: simp only [hk, toCentralizer, MonoidHom.coe_mk, OneHom.coe_mk, card_ofPermHom_support]
-- 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τ)
hk_cT : (↑k : Perm α).cycleType = Multiset.replicate (↑k : Perm α).cycleType.card 2
this : (↑k : Perm α).cycleType.card * 2 = #(↑k : Perm α).support
⊢ ∑ c ∈ τ.support, #(↑c : Perm α).support = #c.support * 2
have H : 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'
-- 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
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
⊢ ∑ c ∈ τ.support, #(↑c : Perm α).support = #c.support * 2
have 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
Tactic: simp only [τ, support_swap 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
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
⊢ ∑
      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
have 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
Tactic: rw [Finset.sum_insert (by simp only [mem_singleton, H, not_false_eq_true]),
      Finset.sum_singleton, hm, mul_two]
-- 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
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
⊢ ∑
      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
have 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
Tactic: rw [Finset.sum_insert (by simp only [mem_singleton, H, not_false_eq_true]),
      Finset.sum_singleton, hm, mul_two]
-- 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
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
⊢ ∑
      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
have rw₂ : #d.support + #(↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) d hd) : Perm α).support = #d.support * 2
Tactic: rw [Finset.sum_insert (by simp only [mem_singleton, H, not_false_eq_true]),
      Finset.sum_singleton, hm, mul_two]
-- 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
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
⊢ ∑
      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
have rw₃ : #d.support + #(↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) d hd) : Perm α).support =
  #d.support + #d.support
Tactic: rw [Finset.sum_insert (by simp only [mem_singleton, H, not_false_eq_true]),
      Finset.sum_singleton, hm, mul_two]
-- 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
this : (↑k : Perm α).cycleType.card * 2 = #(↑k : Perm α).support
that : (↑k : Perm α).cycleType.card = #c.support
⊢ (↑k : Perm α).cycleType.card ∈ g.cycleType
have h₁ : #c.support ∈ g.cycleType
Tactic: rw [that]
-- 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
this : (↑k : Perm α).cycleType.card * 2 = #(↑k : Perm α).support
that : (↑k : Perm α).cycleType.card = #c.support
⊢ #c.support ∈ g.cycleType
have h₁ : ∃ a ∈ g.cycleFactorsFinset.val, (card ∘ support) a = #c.support
Tactic: simp only [cycleType_def, Multiset.mem_map]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
⊢ MonoidHom.range (G :=
      Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
        ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))))
      (kerParam g) =
    Subgroup.centralizer {g}
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
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
have h : ∀ (hx : Membership.mem (γ := Subgroup (Perm α)) (Subgroup.centralizer {g}) x),
  x ∈
    MonoidHom.range (G :=
      Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
        ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))))
      (kerParam g)
Tactic: refine ⟨fun hx ↦ kerParam_range_le_centralizer hx, fun hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
x : Perm α
hx : Membership.mem (γ := Subgroup (Perm α)) (Subgroup.centralizer {g}) x
⊢ x ∈
    MonoidHom.range (G :=
      Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
        ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))))
      (kerParam g)
have h : ∃ (x_1 : Membership.mem (γ := Subgroup (Perm α)) (Subgroup.centralizer {g}) x),
  Eq (α := Perm ↥g.cycleFactorsFinset)
    ((toPermHom g : (a : ↥(Subgroup.centralizer {g})) → Perm ↥g.cycleFactorsFinset)
        (Subtype.mk (p := fun (a : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.centralizer {g}) a) x
          sorry) :
      Perm ↥g.cycleFactorsFinset)
    (1 : Perm ↥g.cycleFactorsFinset)
Tactic: simp_rw [kerParam_range_eq, Subgroup.mem_map, MonoidHom.mem_ker, Subgroup.coe_subtype,
    Subtype.exists, exists_and_right, exists_eq_right]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
x : Perm α
hx : Membership.mem (γ := Subgroup (Perm α)) (Subgroup.centralizer {g}) x
⊢ ∃ (x_1 : Membership.mem (γ := Subgroup (Perm α)) (Subgroup.centralizer {g}) x),
    Eq (α := Perm ↥g.cycleFactorsFinset)
      ((toPermHom g : (a : ↥(Subgroup.centralizer {g})) → Perm ↥g.cycleFactorsFinset)
          (Subtype.mk (p := fun (a : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.centralizer {g}) a) x
            ⋯) :
        Perm ↥g.cycleFactorsFinset)
      (1 : Perm ↥g.cycleFactorsFinset)
have h : Eq (α := Perm ↥g.cycleFactorsFinset)
  ((toPermHom g : (a : ↥(Subgroup.centralizer {g})) → Perm ↥g.cycleFactorsFinset)
      (Subtype.mk (p := fun (a : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (Subgroup.centralizer {g}) a) x sorry) :
    Perm ↥g.cycleFactorsFinset)
  (1 : Perm ↥g.cycleFactorsFinset)
Tactic: use hx