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_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

Tactic:
⟨fun hx ↦ kerParam_range_le_centralizer hx, fun hx ↦ ?_⟩

Premises used: Iff.intro, Equiv.Perm.OnCycleFactors.kerParam_range_le_centralizer
-- 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
x : Perm α
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)
⊢ 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:
refine ⟨fun hx ↦ kerParam_range_le_centralizer hx, fun hx ↦ ?_⟩
-- 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
x : Perm α
hx : Membership.mem (γ := Subgroup (Perm α)) (Subgroup.centralizer {g}) x
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
            ⋯) :
        Perm ↥g.cycleFactorsFinset)
      (1 : Perm ↥g.cycleFactorsFinset)
⊢ x ∈
    MonoidHom.range (G :=
      Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
        ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))))
      (kerParam g)

Tactic:
simp_rw [kerParam_range_eq, Subgroup.mem_map, MonoidHom.mem_ker, Subgroup.coe_subtype,
    Subtype.exists, exists_and_right, exists_eq_right]

Premises used: Subgroup.coe_subtype, Subtype.exists, exists_eq_right, MonoidHom.mem_ker, exists_and_right, Subgroup.mem_map, Equiv.Perm.OnCycleFactors.kerParam_range_eq
-- 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
x : Perm α
hx : Membership.mem (γ := Subgroup (Perm α)) (Subgroup.centralizer {g}) x
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
          ⋯) :
      Perm ↥g.cycleFactorsFinset)
    (1 : Perm ↥g.cycleFactorsFinset)
⊢ ∃ (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)

Tactic:
use hx
-- 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
x : Perm α
hx : Membership.mem (γ := Subgroup (Perm α)) (Subgroup.centralizer {g}) x
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 ⋯) :
                Perm ↥g.cycleFactorsFinset) :
              (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
            c) :
        Perm α)
      (↑((1 : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)
⊢ 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)

Tactic:
ext c : 2
-- 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
x : Perm α
hx : Membership.mem (γ := Subgroup (Perm α)) (Subgroup.centralizer {g}) x
c : ↥g.cycleFactorsFinset
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 ⋯) :
                Perm ↥g.cycleFactorsFinset) :
              (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
            c) :
        Perm α)
      (↑((1 : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)
⊢ 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 α)

Tactic:
rw [← Multiset.nodup_iff_count_le_one, cycleType_def,
    Multiset.nodup_map_iff_inj_on (cycleFactorsFinset g).nodup] at h_count

Premises used: Multiset.nodup_iff_count_le_one, Equiv.Perm.cycleFactorsFinset, Finset.nodup, Multiset.nodup_map_iff_inj_on, Equiv.Perm.cycleType_def
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
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
⊢ (↑((((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 α) ∈
    g.cycleFactorsFinset.val

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
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
⊢ Membership.mem (α := Perm ↥g.cycleFactorsFinset) (γ := Subgroup (Perm ↥g.cycleFactorsFinset))
    (MonoidHom.range (toPermHom g))
    ((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)

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
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 ⋯) :
              Perm ↥g.cycleFactorsFinset) :
            (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
          c) :
      Perm α)
    (↑((1 : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)

Tactic:
exact h_count _ (by simp) _ c.prop (mem_range_toPermHom_iff.mp (by simp) c)

Premises used: Subtype.prop, Equiv.Perm.OnCycleFactors.mem_range_toPermHom_iff, Iff.mp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
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
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 α
⊢ (∀ ⦃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
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h : ∀ ⦃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:
⟨odd_of_centralizer_le_alternatingGroup h,
      card_le_of_centralizer_le_alternating h,
      count_le_one_of_centralizer_le_alternating h⟩

Premises used: Equiv.Perm.count_le_one_of_centralizer_le_alternating, And.intro, Equiv.Perm.card_le_of_centralizer_le_alternating, 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 : ∀ ⦃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:
exact ⟨odd_of_centralizer_le_alternatingGroup h,
      card_le_of_centralizer_le_alternating h,
      count_le_one_of_centralizer_le_alternating h⟩
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
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 ∈
    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

Premises used: Equiv.Perm.OnCycleFactors.kerParam_range_eq_centralizer_of_count_le_one
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
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)
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 α)
⊢ x ∈ alternatingGroup α

Tactic:
obtain ⟨⟨y, uv⟩, rfl⟩ := MonoidHom.mem_range.mp hx

Premises used: MonoidHom.mem_range, Iff.mp, rfl
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
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 α)
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
⊢ 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:
rw [mem_alternatingGroup, sign_kerParam_apply_apply (g := g) y uv]

Premises used: Equiv.Perm.mem_alternatingGroup, Equiv.Perm.OnCycleFactors.sign_kerParam_apply_apply
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
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 :
        ℤˣ)
      (1 : ℤˣ) =
    ((sign : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) →* ℤˣ) :
        (a : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)) → ℤˣ)
      y

Tactic:
mul_one _

Premises used: mul_one
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
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
h₁ :
  Eq (α := ℤˣ) (1 : ℤˣ)
    (((sign : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) →* ℤˣ) :
          (a : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)) → ℤˣ)
        y :
      ℤˣ)
⊢ 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:
convert! mul_one _

Premises used: mul_one
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
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 :
  ∀ (x : ↥g.cycleFactorsFinset),
    Membership.mem (γ := Finset ↥g.cycleFactorsFinset) univ x →
      Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (↑(uv x) : Perm α) : ℤˣ) (1 : ℤˣ)
⊢ Eq (α := ℤˣ) (∏ c : ↥g.cycleFactorsFinset, ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (↑(uv c) : Perm α)) 1

Tactic:
apply Finset.prod_eq_one

Premises used: Finset.prod_eq_one
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
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)
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 : ℤˣ)
⊢ 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

Premises used: Subtype.prop
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
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 :
  HPow.hPow (α := ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ)
          (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc) : Perm α) :
        ℤˣ)
      k =
    1
⊢ Eq (α := ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ)
        (↑(uv (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc)) : Perm α) :
      ℤˣ)
    (1 : ℤˣ)

Tactic:
rw [← hk, map_zpow]

Premises used: map_zpow