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_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
x : Perm α
hx : 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 : ∀ (c : ↥g.cycleFactorsFinset),
  Eq.{u_1 + 1} (α := Perm α)
    (↑((((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) :
            (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
          c) :
      Perm α)
    (↑((1 : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)
Tactic: ext c : 2
-- 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
c : ↥g.cycleFactorsFinset
⊢ Eq.{u_1 + 1} (α := Perm α)
    (↑((((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) :
            (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
          c) :
      Perm α)
    (↑((1 : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)
have h : ∀
  (h_count :
    ∀ x ∈ g.cycleFactorsFinset.val, ∀ y ∈ g.cycleFactorsFinset.val, (card ∘ support) x = (card ∘ support) y → x = y)
  (x : Perm α) (hx : Membership.mem (γ := Subgroup (Perm α)) (Subgroup.centralizer {g}) x) (c : ↥g.cycleFactorsFinset),
  Eq.{u_1 + 1} (α := Perm α)
    (↑((((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) :
            (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
          c) :
      Perm α)
    (↑((1 : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)
Tactic: rw [← Multiset.nodup_iff_count_le_one, cycleType_def,
    Multiset.nodup_map_iff_inj_on (cycleFactorsFinset g).nodup] at h_count
Cleared hypotheses: h_count, x, hx, c
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
⊢ (∀ ⦃x : Perm α⦄, Membership.mem (γ := Subgroup (Perm α)) (Subgroup.centralizer {g}) x → x ∈ alternatingGroup α) ↔
    (∀ c ∈ g.cycleType, Odd c) ∧ Fintype.card α ≤ g.cycleType.sum + 1 ∧ ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
have mp : (∀ ⦃x : Perm α⦄, Membership.mem (γ := Subgroup (Perm α)) (Subgroup.centralizer {g}) x → x ∈ alternatingGroup α) →
  (∀ c ∈ g.cycleType, Odd c) ∧ Fintype.card α ≤ g.cycleType.sum + 1 ∧ ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
mp :
  (∀ ⦃x : Perm α⦄, Membership.mem (γ := Subgroup (Perm α)) (Subgroup.centralizer {g}) x → x ∈ alternatingGroup α) →
    (∀ c ∈ g.cycleType, Odd c) ∧ Fintype.card α ≤ g.cycleType.sum + 1 ∧ ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
⊢ (∀ ⦃x : Perm α⦄, Membership.mem (γ := Subgroup (Perm α)) (Subgroup.centralizer {g}) x → x ∈ alternatingGroup α) ↔
    (∀ c ∈ g.cycleType, Odd c) ∧ Fintype.card α ≤ g.cycleType.sum + 1 ∧ ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
have mpr : ((∀ c ∈ g.cycleType, Odd c) ∧ Fintype.card α ≤ g.cycleType.sum + 1 ∧ ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1) →
  ∀ ⦃x : Perm α⦄, Membership.mem (γ := Subgroup (Perm α)) (Subgroup.centralizer {g}) x → x ∈ alternatingGroup α
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h_odd : ∀ c ∈ g.cycleType, Odd c
h_fixed : Fintype.card α ≤ g.cycleType.sum + 1
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
x : Perm α
hx : Membership.mem (γ := Subgroup (Perm α)) (Subgroup.centralizer {g}) x
⊢ x ∈ alternatingGroup α
have hx₁ : x ∈
  MonoidHom.range (G :=
    Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
      ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))))
    (kerParam g)
Tactic: rw [← kerParam_range_eq_centralizer_of_count_le_one h_count] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h_odd : ∀ c ∈ g.cycleType, Odd c
h_fixed : Fintype.card α ≤ g.cycleType.sum + 1
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
x : Perm α
hx :
  x ∈
    MonoidHom.range (G :=
      Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
        ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))))
      (kerParam g)
⊢ x ∈ alternatingGroup α
have mpr : ∀ (y : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1))
  (uv : (c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α)))
  (hx :
    Membership.mem (α := Perm α)
      (MonoidHom.range (G :=
        Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
          ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))))
        (kerParam g))
      ((kerParam g :
            (a :
                Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
                  ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α)))) →
              Perm α)
          (y, uv) :
        Perm α)),
  Membership.mem (α := Perm α) (alternatingGroup α)
    ((kerParam g :
          (a :
              Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
                ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α)))) →
            Perm α)
        (y, uv) :
      Perm α)
Tactic: obtain ⟨⟨y, uv⟩, rfl⟩ := MonoidHom.mem_range.mp hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h_odd : ∀ c ∈ g.cycleType, Odd c
h_fixed : Fintype.card α ≤ g.cycleType.sum + 1
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
y : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
uv : (c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))
hx :
  Membership.mem (α := Perm α)
    (MonoidHom.range (G :=
      Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
        ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))))
      (kerParam g))
    ((kerParam g :
          (a :
              Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
                ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α)))) →
            Perm α)
        (y, uv) :
      Perm α)
⊢ Membership.mem (α := Perm α) (alternatingGroup α)
    ((kerParam g :
          (a :
              Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
                ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α)))) →
            Perm α)
        (y, uv) :
      Perm α)
have mpr : HMul.hMul (α := ℤˣ) (β := ℤˣ)
    (((sign : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) →* ℤˣ) :
          (a : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)) → ℤˣ)
        y :
      ℤˣ)
    (∏ c : ↥g.cycleFactorsFinset, ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (↑(uv c) : Perm α) : ℤˣ) =
  1
Tactic: rw [mem_alternatingGroup, sign_kerParam_apply_apply (g := g) y uv]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h_odd : ∀ c ∈ g.cycleType, Odd c
h_fixed : Fintype.card α ≤ g.cycleType.sum + 1
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
y : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
uv : (c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))
hx :
  Membership.mem (α := Perm α)
    (MonoidHom.range (G :=
      Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
        ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))))
      (kerParam g))
    ((kerParam g :
          (a :
              Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
                ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α)))) →
            Perm α)
        (y, uv) :
      Perm α)
⊢ HMul.hMul (α := ℤˣ) (β := ℤˣ)
      (((sign : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) →* ℤˣ) :
            (a : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)) → ℤˣ)
          y :
        ℤˣ)
      (∏ c : ↥g.cycleFactorsFinset, ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (↑(uv c) : Perm α) : ℤˣ) =
    1
have h : Eq (α := ℤˣ) (∏ c : ↥g.cycleFactorsFinset, ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (↑(uv c) : Perm α)) 1
Tactic: convert! mul_one _
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h_odd : ∀ c ∈ g.cycleType, Odd c
h_fixed : Fintype.card α ≤ g.cycleType.sum + 1
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
y : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
uv : (c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))
hx :
  Membership.mem (α := Perm α)
    (MonoidHom.range (G :=
      Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
        ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))))
      (kerParam g))
    ((kerParam g :
          (a :
              Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
                ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α)))) →
            Perm α)
        (y, uv) :
      Perm α)
h : Eq (α := ℤˣ) (∏ c : ↥g.cycleFactorsFinset, ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (↑(uv c) : Perm α)) 1
⊢ HMul.hMul (α := ℤˣ) (β := ℤˣ)
      (((sign : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) →* ℤˣ) :
            (a : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)) → ℤˣ)
          y :
        ℤˣ)
      (∏ c : ↥g.cycleFactorsFinset, ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (↑(uv c) : Perm α) : ℤˣ) =
    1
have h₁ : Eq (α := ℤˣ) (1 : ℤˣ)
  (((sign : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) →* ℤˣ) :
        (a : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)) → ℤˣ)
      y :
    ℤˣ)
Tactic: convert! mul_one _
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h_odd : ∀ c ∈ g.cycleType, Odd c
h_fixed : Fintype.card α ≤ g.cycleType.sum + 1
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
y : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
uv : (c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))
hx :
  Membership.mem (α := Perm α)
    (MonoidHom.range (G :=
      Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
        ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))))
      (kerParam g))
    ((kerParam g :
          (a :
              Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
                ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α)))) →
            Perm α)
        (y, uv) :
      Perm α)
⊢ Eq (α := ℤˣ) (∏ c : ↥g.cycleFactorsFinset, ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (↑(uv c) : Perm α)) 1
have h : ∀ (x : ↥g.cycleFactorsFinset),
  Membership.mem (γ := Finset ↥g.cycleFactorsFinset) univ x →
    Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (↑(uv x) : Perm α) : ℤˣ) (1 : ℤˣ)
Tactic: apply Finset.prod_eq_one
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h_odd : ∀ c ∈ g.cycleType, Odd c
h_fixed : Fintype.card α ≤ g.cycleType.sum + 1
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
y : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
uv : (c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))
hx :
  Membership.mem (α := Perm α)
    (MonoidHom.range (G :=
      Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
        ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))))
      (kerParam g))
    ((kerParam g :
          (a :
              Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
                ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α)))) →
            Perm α)
        (y, uv) :
      Perm α)
c : Perm α
hc : c ∈ g.cycleFactorsFinset
h :
  Membership.mem (γ := Finset ↥g.cycleFactorsFinset) univ
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc)
⊢ Eq (α := ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ)
        (↑(uv (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc)) : Perm α) :
      ℤˣ)
    (1 : ℤˣ)
have h : ∀ (k : ℤ)
  (hk :
    (fun (x : ℤ) ↦ (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc) : Perm α) ^ x) k =
      (↑(uv (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc)) : Perm α)),
  Eq (α := ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ)
        (↑(uv (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc)) : Perm α) :
      ℤˣ)
    (1 : ℤˣ)
Tactic: obtain ⟨k, hk⟩ := (uv _).prop
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h_odd : ∀ c ∈ g.cycleType, Odd c
h_fixed : Fintype.card α ≤ g.cycleType.sum + 1
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
y : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
uv : (c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))
hx :
  Membership.mem (α := Perm α)
    (MonoidHom.range (G :=
      Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
        ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))))
      (kerParam g))
    ((kerParam g :
          (a :
              Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
                ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α)))) →
            Perm α)
        (y, uv) :
      Perm α)
c : Perm α
hc : c ∈ g.cycleFactorsFinset
h :
  Membership.mem (γ := Finset ↥g.cycleFactorsFinset) univ
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc)
k : ℤ
hk :
  (fun (x : ℤ) ↦ (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc) : Perm α) ^ x) k =
    (↑(uv (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc)) : Perm α)
⊢ Eq (α := ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ)
        (↑(uv (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc)) : Perm α) :
      ℤˣ)
    (1 : ℤˣ)
have h : HPow.hPow (α := ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ)
        (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc) : Perm α) :
      ℤˣ)
    k =
  1
Tactic: rw [← hk, map_zpow]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h_odd : ∀ c ∈ g.cycleType, Odd c
h_fixed : Fintype.card α ≤ g.cycleType.sum + 1
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
y : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
uv : (c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))
hx :
  Membership.mem (α := Perm α)
    (MonoidHom.range (G :=
      Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
        ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))))
      (kerParam g))
    ((kerParam g :
          (a :
              Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
                ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α)))) →
            Perm α)
        (y, uv) :
      Perm α)
c : Perm α
hc : c ∈ g.cycleFactorsFinset
h :
  Membership.mem (γ := Finset ↥g.cycleFactorsFinset) univ
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc)
k : ℤ
hk :
  (fun (x : ℤ) ↦ (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc) : Perm α) ^ x) k =
    (↑(uv (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc)) : Perm α)
⊢ HPow.hPow (α := ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ)
          (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc) : Perm α) :
        ℤˣ)
      k =
    1
have h : Eq (α := ℤˣ)
  (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ)
      (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc) : Perm α) :
    ℤˣ)
  (1 : ℤˣ)
Tactic: convert! one_zpow k
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h_odd : ∀ c ∈ g.cycleType, Odd c
h_fixed : Fintype.card α ≤ g.cycleType.sum + 1
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
y : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
uv : (c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))
hx :
  Membership.mem (α := Perm α)
    (MonoidHom.range (G :=
      Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
        ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))))
      (kerParam g))
    ((kerParam g :
          (a :
              Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
                ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α)))) →
            Perm α)
        (y, uv) :
      Perm α)
c : Perm α
hc : c ∈ g.cycleFactorsFinset
h :
  Membership.mem (γ := Finset ↥g.cycleFactorsFinset) univ
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc)
k : ℤ
hk :
  (fun (x : ℤ) ↦ (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc) : Perm α) ^ x) k =
    (↑(uv (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc)) : Perm α)
⊢ Eq (α := ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ)
        (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc) : Perm α) :
      ℤˣ)
    (1 : ℤˣ)
have h : Odd #(↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc) : Perm α).support
Tactic: rw [IsCycle.sign, Odd.neg_one_pow, neg_neg]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h_odd : ∀ c ∈ g.cycleType, Odd c
h_fixed : Fintype.card α ≤ g.cycleType.sum + 1
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
y : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
uv : (c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))
hx :
  Membership.mem (α := Perm α)
    (MonoidHom.range (G :=
      Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
        ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))))
      (kerParam g))
    ((kerParam g :
          (a :
              Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
                ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α)))) →
            Perm α)
        (y, uv) :
      Perm α)
c : Perm α
hc : c ∈ g.cycleFactorsFinset
h_1 :
  Membership.mem (γ := Finset ↥g.cycleFactorsFinset) univ
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc)
k : ℤ
hk :
  (fun (x : ℤ) ↦ (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc) : Perm α) ^ x) k =
    (↑(uv (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc)) : Perm α)
h : Odd #(↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc) : Perm α).support
⊢ Eq (α := ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ)
        (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc) : Perm α) :
      ℤˣ)
    (1 : ℤˣ)
have h₁ : (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc) : Perm α).IsCycle
Tactic: rw [IsCycle.sign, Odd.neg_one_pow, neg_neg]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h_odd : ∀ c ∈ g.cycleType, Odd c
h_fixed : Fintype.card α ≤ g.cycleType.sum + 1
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
y : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
uv : (c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))
hx :
  Membership.mem (α := Perm α)
    (MonoidHom.range (G :=
      Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
        ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))))
      (kerParam g))
    ((kerParam g :
          (a :
              Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
                ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α)))) →
            Perm α)
        (y, uv) :
      Perm α)
c : Perm α
hc : c ∈ g.cycleFactorsFinset
h :
  Membership.mem (γ := Finset ↥g.cycleFactorsFinset) univ
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc)
k : ℤ
hk :
  (fun (x : ℤ) ↦ (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc) : Perm α) ^ x) k =
    (↑(uv (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc)) : Perm α)
⊢ Odd #(↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc) : Perm α).support
have h : #(↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc) : Perm α).support ∈ g.cycleType
Tactic: apply h_odd
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h_odd : ∀ c ∈ g.cycleType, Odd c
h_fixed : Fintype.card α ≤ g.cycleType.sum + 1
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
y : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
uv : (c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))
hx :
  Membership.mem (α := Perm α)
    (MonoidHom.range (G :=
      Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
        ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))))
      (kerParam g))
    ((kerParam g :
          (a :
              Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
                ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α)))) →
            Perm α)
        (y, uv) :
      Perm α)
c : Perm α
hc : c ∈ g.cycleFactorsFinset
h :
  Membership.mem (γ := Finset ↥g.cycleFactorsFinset) univ
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc)
k : ℤ
hk :
  (fun (x : ℤ) ↦ (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc) : Perm α) ^ x) k =
    (↑(uv (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc)) : Perm α)
⊢ #(↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc) : Perm α).support ∈ g.cycleType
have h : ∃ a ∈ g.cycleFactorsFinset.val,
  (card ∘ support) a = #(↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc) : Perm α).support
Tactic: rw [cycleType_def, Multiset.mem_map]