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_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 (α := ℤˣ) 1 k = 1

Tactic:
one_zpow k

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

Tactic:
convert! one_zpow k

Premises used: one_zpow
-- 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 : Odd #(↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc) : Perm α).support
h₁ : (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc) : Perm α).IsCycle
⊢ Eq (α := ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ)
        (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc) : Perm α) :
      ℤˣ)
    (1 : ℤˣ)

Tactic:
rw [IsCycle.sign, Odd.neg_one_pow, neg_neg]

Premises used: neg_neg, Equiv.Perm.IsCycle.sign, Odd.neg_one_pow
-- 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 : #(↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc) : Perm α).support ∈ g.cycleType
⊢ Odd #(↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc) : Perm α).support

Tactic:
apply h_odd
-- 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 :
  ∃ a ∈ g.cycleFactorsFinset.val,
    (card ∘ support) a = #(↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc) : Perm α).support
⊢ #(↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc) : Perm α).support ∈ g.cycleType

Tactic:
rw [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_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 α)
⊢ ∃ a ∈ g.cycleFactorsFinset.val,
    (card ∘ support) a = #(↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc) : Perm α).support

Tactic:
⟨c, hc, rfl⟩

Premises used: And.intro, Exists.intro, 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 α)
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 α)
⊢ ∃ a ∈ g.cycleFactorsFinset.val,
    (card ∘ support) a = #(↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc) : Perm α).support

Tactic:
exact ⟨c, hc, 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 α)
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 :
  ∀ (hc_1 : c.IsCycle ∧ ∀ a ∈ c.support, Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)),
    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 α).IsCycle
⊢ (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc) : Perm α).IsCycle

Tactic:
rw [mem_cycleFactorsFinset_iff] at hc

Premises used: Equiv.Perm.mem_cycleFactorsFinset_iff
-- 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_1 : c ∈ g.cycleFactorsFinset
hc : c.IsCycle ∧ ∀ a ∈ c.support, Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
h :
  Membership.mem (γ := Finset ↥g.cycleFactorsFinset) univ
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc_1)
k : ℤ
hk :
  (fun (x : ℤ) ↦ (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc_1) : Perm α) ^ x) k =
    (↑(uv (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc_1)) : Perm α)
⊢ (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc_1) : Perm α).IsCycle

Tactic:
hc.left

Premises used: And.left
-- 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_1 : c ∈ g.cycleFactorsFinset
hc : c.IsCycle ∧ ∀ a ∈ c.support, Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
h :
  Membership.mem (γ := Finset ↥g.cycleFactorsFinset) univ
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc_1)
k : ℤ
hk :
  (fun (x : ℤ) ↦ (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc_1) : Perm α) ^ x) k =
    (↑(uv (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc_1)) : Perm α)
⊢ (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc_1) : Perm α).IsCycle

Tactic:
exact hc.left

Premises used: And.left
-- 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 α)
this : y = 1
⊢ Eq (α := ℤˣ) (1 : ℤˣ)
    (((sign : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) →* ℤˣ) :
          (a : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)) → ℤˣ)
        y :
      ℤˣ)

Tactic:
simp [this]
-- 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 : y = 1
⊢ Eq (α := ℤˣ) (1 : ℤˣ)
    (((sign : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) →* ℤˣ) :
          (a : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)) → ℤˣ)
        y :
      ℤˣ)

Tactic:
suffices y = 1 by simp [this]
-- 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 α)
⊢ Fintype.card.{u_1} (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) = Fintype.card α - g.cycleType.sum

Tactic:
have := card_fixedPoints g
-- 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 α)
this : Fintype.card.{u_1} (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) = Fintype.card α - g.cycleType.sum
⊢ Fintype.card.{u_1} (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ≤ 1

Tactic:
lia
-- 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 α)
this : Fintype.card.{u_1} (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) = Fintype.card α - g.cycleType.sum
⊢ y = 1

Tactic:
exact card_support_le_one.mp <| le_trans (Finset.card_le_univ _) (by lia)

Premises used: Equiv.Perm.card_support_le_one, Finset.card_le_univ, Iff.mp, le_trans
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
g : ↥(alternatingGroup α)
hg : (↑g : Perm α).IsThreeCycle
hg₁ : IsConj g (HPow.hPow (β := ℕ) g 2)
⊢ Membership.mem (γ := Set ↥(alternatingGroup α)) (commutatorSet ↥(alternatingGroup α)) g

Tactic:
apply mem_commutatorSet_of_isConj_sq

Premises used: mem_commutatorSet_of_isConj_sq
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
g : ↥(alternatingGroup α)
hg : (↑g : Perm α).IsThreeCycle
hg₁ : (↑(HPow.hPow (β := ℕ) g 2) : Perm α).IsThreeCycle
⊢ IsConj g (HPow.hPow (β := ℕ) g 2)

Tactic:
apply alternatingGroup.isThreeCycle_isConj h5 hg

Premises used: alternatingGroup.isThreeCycle_isConj
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
g : ↥(alternatingGroup α)
hg : (↑g : Perm α).IsThreeCycle
⊢ (↑(HPow.hPow (β := ℕ) g 2) : Perm α).IsThreeCycle

Tactic:
simpa [sq] using hg.isThreeCycle_sq

Premises used: sq, Equiv.Perm.IsThreeCycle.isThreeCycle_sq
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
g : ↥(alternatingGroup α)
hg : (↑g : Perm α).IsThreeCycle
rw : Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (Subgroup.closure (commutatorSet ↥(alternatingGroup α))) g
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) g

Tactic:
rw [commutator_eq_closure]

Premises used: commutator_eq_closure
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
g : ↥(alternatingGroup α)
hg : (↑g : Perm α).IsThreeCycle
a : Membership.mem (γ := Set ↥(alternatingGroup α)) (commutatorSet ↥(alternatingGroup α)) g
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (Subgroup.closure (commutatorSet ↥(alternatingGroup α))) g

Tactic:
apply Subgroup.subset_closure

Premises used: Subgroup.subset_closure
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
g : ↥(alternatingGroup α)
hg : (↑g : Perm α).IsThreeCycle
⊢ Membership.mem (γ := Set ↥(alternatingGroup α)) (commutatorSet ↥(alternatingGroup α)) g

Tactic:
hg.mem_commutatorSet_alternatingGroup h5

Premises used: Equiv.Perm.IsThreeCycle.mem_commutatorSet_alternatingGroup