awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
p : ↥(centralizer {g})
u : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) :=
  (↑p : Perm α).subtypePerm (p := Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α))) ⋯
hp :
  ∀ c ∈ g.cycleFactorsFinset,
    ∃ (hc : ∀ (x : α), Membership.mem (α := α) c.support (((↑p : Perm α) : (a : α) → α) x : α) ↔ x ∈ c.support),
      Membership.mem (α := Perm α) (γ := Subgroup (Perm α)) (zpowers c)
        ((ofSubtype (p := fun (x : α) ↦ x ∈ c.support) : (a : Perm ↥c.support) → Perm α)
            ((↑p : Perm α).subtypePerm (p := Membership.mem c.support) hc) :
          Perm α)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α)) :=
  fun (c : ↥g.cycleFactorsFinset) ↦
    Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (zpowers (↑c : Perm α)) x)
      ((ofSubtype (p := fun (x : α) ↦ x ∈ (↑c : Perm α).support) : (a : Perm ↥(↑c : Perm α).support) → Perm α)
        ((↑p : Perm α).subtypePerm (p := Membership.mem (↑c : Perm α).support) ⋯))
      ⋯
h :
  ∀ (x : α),
    Eq (α := α)
      ((((kerParam g :
                  (a :
                      Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
                        ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α)))) →
                    Perm α)
                (u, v) :
              Perm α) :
            (a : α) → α)
          x :
        α)
      (((↑p : Perm α) : (a : α) → α) x : α)
⊢ (kerParam g :
        (a :
            Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
              ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α)))) →
          Perm α)
      (u, v) =
    (↑p : Perm α)

Tactic:
ext x
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
p : ↥(centralizer {g})
u : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) :=
  (↑p : Perm α).subtypePerm (p := Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α))) ⋯
hp :
  ∀ c ∈ g.cycleFactorsFinset,
    ∃ (hc : ∀ (x : α), Membership.mem (α := α) c.support (((↑p : Perm α) : (a : α) → α) x : α) ↔ x ∈ c.support),
      Membership.mem (α := Perm α) (γ := Subgroup (Perm α)) (zpowers c)
        ((ofSubtype (p := fun (x : α) ↦ x ∈ c.support) : (a : Perm ↥c.support) → Perm α)
            ((↑p : Perm α).subtypePerm (p := Membership.mem c.support) hc) :
          Perm α)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α)) :=
  fun (c : ↥g.cycleFactorsFinset) ↦
    Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (zpowers (↑c : Perm α)) x)
      ((ofSubtype (p := fun (x : α) ↦ x ∈ (↑c : Perm α).support) : (a : Perm ↥(↑c : Perm α).support) → Perm α)
        ((↑p : Perm α).subtypePerm (p := Membership.mem (↑c : Perm α).support) ⋯))
      ⋯
x : α
h :
  Eq (α := α)
    (if hx : g.cycleOf x ∈ g.cycleFactorsFinset then
        ((↑(v (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α) : (a : α) → α)
          x
      else
        (((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x) :
                  (a : Perm { x : α // x ∈ Function.fixedPoints (⇑g : (a : α) → α) }) → Perm α)
                u :
              Perm α) :
            (a : α) → α)
          x :
      α)
    (((↑p : Perm α) : (a : α) → α) x : α)
⊢ Eq (α := α)
    ((((kerParam g :
                (a :
                    Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
                      ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α)))) →
                  Perm α)
              (u, v) :
            Perm α) :
          (a : α) → α)
        x :
      α)
    (((↑p : Perm α) : (a : α) → α) x : α)

Tactic:
rw [kerParam_apply]

Premises used: Equiv.Perm.OnCycleFactors.kerParam_apply
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
p : ↥(centralizer {g})
u : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) :=
  (↑p : Perm α).subtypePerm (p := Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α))) ⋯
hp :
  ∀ c ∈ g.cycleFactorsFinset,
    ∃ (hc : ∀ (x : α), Membership.mem (α := α) c.support (((↑p : Perm α) : (a : α) → α) x : α) ↔ x ∈ c.support),
      Membership.mem (α := Perm α) (γ := Subgroup (Perm α)) (zpowers c)
        ((ofSubtype (p := fun (x : α) ↦ x ∈ c.support) : (a : Perm ↥c.support) → Perm α)
            ((↑p : Perm α).subtypePerm (p := Membership.mem c.support) hc) :
          Perm α)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α)) :=
  fun (c : ↥g.cycleFactorsFinset) ↦
    Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (zpowers (↑c : Perm α)) x)
      ((ofSubtype (p := fun (x : α) ↦ x ∈ (↑c : Perm α).support) : (a : Perm ↥(↑c : Perm α).support) → Perm α)
        ((↑p : Perm α).subtypePerm (p := Membership.mem (↑c : Perm α).support) ⋯))
      ⋯
x : α
pos :
  ∀ (hx : g.cycleOf x ∈ g.cycleFactorsFinset),
    Eq (α := α)
      (((↑(v (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α) : (a : α) → α)
          x :
        α)
      (((↑p : Perm α) : (a : α) → α) x : α)
neg :
  ∀ (hx : g.cycleOf x ∉ g.cycleFactorsFinset),
    Eq (α := α)
      ((((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x) :
                  (a : Perm { x : α // x ∈ Function.fixedPoints (⇑g : (a : α) → α) }) → Perm α)
                u :
              Perm α) :
            (a : α) → α)
          x :
        α)
      (((↑p : Perm α) : (a : α) → α) x : α)
⊢ Eq (α := α)
    (if hx : g.cycleOf x ∈ g.cycleFactorsFinset then
        ((↑(v (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α) : (a : α) → α)
          x
      else
        (((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x) :
                  (a : Perm { x : α // x ∈ Function.fixedPoints (⇑g : (a : α) → α) }) → Perm α)
                u :
              Perm α) :
            (a : α) → α)
          x :
      α)
    (((↑p : Perm α) : (a : α) → α) x : α)

Tactic:
split_ifs with hx
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
p : ↥(centralizer {g})
u : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) :=
  (↑p : Perm α).subtypePerm (p := Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α))) ⋯
hp :
  ∀ c ∈ g.cycleFactorsFinset,
    ∃ (hc : ∀ (x : α), Membership.mem (α := α) c.support (((↑p : Perm α) : (a : α) → α) x : α) ↔ x ∈ c.support),
      Membership.mem (α := Perm α) (γ := Subgroup (Perm α)) (zpowers c)
        ((ofSubtype (p := fun (x : α) ↦ x ∈ c.support) : (a : Perm ↥c.support) → Perm α)
            ((↑p : Perm α).subtypePerm (p := Membership.mem c.support) hc) :
          Perm α)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α)) :=
  fun (c : ↥g.cycleFactorsFinset) ↦
    Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (zpowers (↑c : Perm α)) x)
      ((ofSubtype (p := fun (x : α) ↦ x ∈ (↑c : Perm α).support) : (a : Perm ↥(↑c : Perm α).support) → Perm α)
        ((↑p : Perm α).subtypePerm (p := Membership.mem (↑c : Perm α).support) ⋯))
      ⋯
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ (g : (a : α) → α) x ≠ x

Tactic:
rw [cycleOf_mem_cycleFactorsFinset_iff, mem_support] at hx

Premises used: Equiv.Perm.mem_support, Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
p : ↥(centralizer {g})
u : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) :=
  (↑p : Perm α).subtypePerm (p := Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α))) ⋯
hp :
  ∀ c ∈ g.cycleFactorsFinset,
    ∃ (hc : ∀ (x : α), Membership.mem (α := α) c.support (((↑p : Perm α) : (a : α) → α) x : α) ↔ x ∈ c.support),
      Membership.mem (α := Perm α) (γ := Subgroup (Perm α)) (zpowers c)
        ((ofSubtype (p := fun (x : α) ↦ x ∈ c.support) : (a : Perm ↥c.support) → Perm α)
            ((↑p : Perm α).subtypePerm (p := Membership.mem c.support) hc) :
          Perm α)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α)) :=
  fun (c : ↥g.cycleFactorsFinset) ↦
    Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (zpowers (↑c : Perm α)) x)
      ((ofSubtype (p := fun (x : α) ↦ x ∈ (↑c : Perm α).support) : (a : Perm ↥(↑c : Perm α).support) → Perm α)
        ((↑p : Perm α).subtypePerm (p := Membership.mem (↑c : Perm α).support) ⋯))
      ⋯
x : α
hx_1 : g.cycleOf x ∈ g.cycleFactorsFinset
hx : (g : (a : α) → α) x ≠ x
pos : x ∈ (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx_1) : Perm α).support
⊢ Eq (α := α)
    (((↑(v (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx_1)) : Perm α) : (a : α) → α)
        x :
      α)
    (((↑p : Perm α) : (a : α) → α) x : α)

Tactic:
rw [ofSubtype_apply_of_mem, subtypePerm_apply]

Premises used: Equiv.Perm.ofSubtype_apply_of_mem, Equiv.Perm.subtypePerm_apply
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
p : ↥(centralizer {g})
u : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) :=
  (↑p : Perm α).subtypePerm (p := Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α))) ⋯
hp :
  ∀ c ∈ g.cycleFactorsFinset,
    ∃ (hc : ∀ (x : α), Membership.mem (α := α) c.support (((↑p : Perm α) : (a : α) → α) x : α) ↔ x ∈ c.support),
      Membership.mem (α := Perm α) (γ := Subgroup (Perm α)) (zpowers c)
        ((ofSubtype (p := fun (x : α) ↦ x ∈ c.support) : (a : Perm ↥c.support) → Perm α)
            ((↑p : Perm α).subtypePerm (p := Membership.mem c.support) hc) :
          Perm α)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α)) :=
  fun (c : ↥g.cycleFactorsFinset) ↦
    Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (zpowers (↑c : Perm α)) x)
      ((ofSubtype (p := fun (x : α) ↦ x ∈ (↑c : Perm α).support) : (a : Perm ↥(↑c : Perm α).support) → Perm α)
        ((↑p : Perm α).subtypePerm (p := Membership.mem (↑c : Perm α).support) ⋯))
      ⋯
x : α
hx_1 : g.cycleOf x ∈ g.cycleFactorsFinset
hx : (g : (a : α) → α) x ≠ x
pos :
  ((↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx_1) : Perm α) : (a : α) → α) x ≠ x
pos₁ : (g : (a : α) → α) x ≠ x
pos₂ pos₃ pos₄ pos₅ : ¬(g : (a : α) → α) x = x
⊢ x ∈ (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx_1) : Perm α).support

Tactic:
rwa [mem_support, cycleOf_apply_self, ne_eq]

Premises used: Equiv.Perm.mem_support, ne_eq, Equiv.Perm.cycleOf_apply_self
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
p : ↥(centralizer {g})
u : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) :=
  (↑p : Perm α).subtypePerm (p := Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α))) ⋯
hp :
  ∀ c ∈ g.cycleFactorsFinset,
    ∃ (hc : ∀ (x : α), Membership.mem (α := α) c.support (((↑p : Perm α) : (a : α) → α) x : α) ↔ x ∈ c.support),
      Membership.mem (α := Perm α) (γ := Subgroup (Perm α)) (zpowers c)
        ((ofSubtype (p := fun (x : α) ↦ x ∈ c.support) : (a : Perm ↥c.support) → Perm α)
            ((↑p : Perm α).subtypePerm (p := Membership.mem c.support) hc) :
          Perm α)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α)) :=
  fun (c : ↥g.cycleFactorsFinset) ↦
    Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (zpowers (↑c : Perm α)) x)
      ((ofSubtype (p := fun (x : α) ↦ x ∈ (↑c : Perm α).support) : (a : Perm ↥(↑c : Perm α).support) → Perm α)
        ((↑p : Perm α).subtypePerm (p := Membership.mem (↑c : Perm α).support) ⋯))
      ⋯
x : α
hx : g.cycleOf x ∉ g.cycleFactorsFinset
⊢ (g : (a : α) → α) x = x

Tactic:
rw [cycleOf_mem_cycleFactorsFinset_iff, notMem_support] at hx

Premises used: Equiv.Perm.notMem_support, Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
p : ↥(centralizer {g})
u : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) :=
  (↑p : Perm α).subtypePerm (p := Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α))) ⋯
hp :
  ∀ c ∈ g.cycleFactorsFinset,
    ∃ (hc : ∀ (x : α), Membership.mem (α := α) c.support (((↑p : Perm α) : (a : α) → α) x : α) ↔ x ∈ c.support),
      Membership.mem (α := Perm α) (γ := Subgroup (Perm α)) (zpowers c)
        ((ofSubtype (p := fun (x : α) ↦ x ∈ c.support) : (a : Perm ↥c.support) → Perm α)
            ((↑p : Perm α).subtypePerm (p := Membership.mem c.support) hc) :
          Perm α)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α)) :=
  fun (c : ↥g.cycleFactorsFinset) ↦
    Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (zpowers (↑c : Perm α)) x)
      ((ofSubtype (p := fun (x : α) ↦ x ∈ (↑c : Perm α).support) : (a : Perm ↥(↑c : Perm α).support) → Perm α)
        ((↑p : Perm α).subtypePerm (p := Membership.mem (↑c : Perm α).support) ⋯))
      ⋯
x : α
hx : (g : (a : α) → α) x = x
neg :
  Eq (α := α)
    ((↑((u :
              (a : { x : α // x ∈ Function.fixedPoints (⇑g : (a : α) → α) }) →
                { x : α // x ∈ Function.fixedPoints (⇑g : (a : α) → α) })
            (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x) x
              hx)) :
        α) :
      α)
    (((↑p : Perm α) : (a : α) → α) x : α)
neg₁ : Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
neg₂ :
  Eq (α := α)
    ((↑(Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x)
            (((↑p : Perm α) : (a : α) → α)
              (↑(Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x)
                    x hx) :
                α))
            ⋯) :
        α) :
      α)
    (((↑p : Perm α) : (a : α) → α) x : α)
neg₃ : Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
neg₄ :
  Eq (α := α)
    ((↑(Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x)
            (((↑p : Perm α) : (a : α) → α)
              (↑(Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x)
                    x hx) :
                α))
            ⋯) :
        α) :
      α)
    (((↑p : Perm α) : (a : α) → α) x : α)
neg₅ neg₆ neg₇ : Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
⊢ Eq (α := α)
    ((((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x) :
                (a : Perm { x : α // x ∈ Function.fixedPoints (⇑g : (a : α) → α) }) → Perm α)
              u :
            Perm α) :
          (a : α) → α)
        x :
      α)
    (((↑p : Perm α) : (a : α) → α) x : α)

Tactic:
rwa [ofSubtype_apply_of_mem, subtypePerm_apply]

Premises used: Equiv.Perm.ofSubtype_apply_of_mem, Equiv.Perm.subtypePerm_apply
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
rw :
  map (Subgroup.subtype (centralizer {g})) (MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (toPermHom g)) ≤
    centralizer {g}
⊢ MonoidHom.range (G :=
      Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
        ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))))
      (kerParam g) ≤
    centralizer {g}

Tactic:
rw [kerParam_range_eq]

Premises used: Equiv.Perm.OnCycleFactors.kerParam_range_eq
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
⊢ map (Subgroup.subtype (centralizer {g})) (MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (toPermHom g)) ≤
    centralizer {g}

Tactic:
map_subtype_le (toPermHom g).ker

Premises used: MonoidHom.ker, Subgroup.map_subtype_le, Equiv.Perm.OnCycleFactors.toPermHom
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
⊢ map (Subgroup.subtype (centralizer {g})) (MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (toPermHom g)) ≤
    centralizer {g}

Tactic:
exact map_subtype_le (toPermHom g).ker

Premises used: MonoidHom.ker, Subgroup.map_subtype_le, Equiv.Perm.OnCycleFactors.toPermHom
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
rw :
  Fintype.card.{u_1}
      (Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
        ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α)))) =
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod
⊢ Fintype.card.{u_1}
      ↥(MonoidHom.range (G :=
          Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
            ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))))
          (kerParam g)) =
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod

Tactic:
rw [Fintype.card_coeSort_range (kerParam_injective g)]

Premises used: Fintype.card_coeSort_range, Equiv.Perm.OnCycleFactors.kerParam_injective
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
rw :
  (Fintype.card α - g.cycleType.sum)! * ∏ i : ↥g.cycleFactorsFinset, Fintype.card.{u_1} ↥(zpowers (↑i : Perm α)) =
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod
⊢ Fintype.card.{u_1}
      (Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
        ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α)))) =
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod

Tactic:
rw [Fintype.card_prod, Fintype.card_perm, Fintype.card_pi, card_fixedPoints]

Premises used: Fintype.card_pi, Fintype.card_perm, Fintype.card_prod, Equiv.Perm.card_fixedPoints
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
h : ∏ i : ↥g.cycleFactorsFinset, Fintype.card.{u_1} ↥(zpowers (↑i : Perm α)) = g.cycleType.prod
⊢ (Fintype.card α - g.cycleType.sum)! * ∏ i : ↥g.cycleFactorsFinset, Fintype.card.{u_1} ↥(zpowers (↑i : Perm α)) =
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod

Tactic:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
h :
  Eq (α := ℕ) (∏ x ∈ g.cycleFactorsFinset, Fintype.card.{u_1} ↥(zpowers x))
    (∏ a ∈ g.cycleFactorsFinset, (Finset.card ∘ support) a)
⊢ ∏ i : ↥g.cycleFactorsFinset, Fintype.card.{u_1} ↥(zpowers (↑i : Perm α)) = g.cycleType.prod

Tactic:
rw [Finset.univ_eq_attach, g.cycleFactorsFinset.prod_attach (fun i ↦ Fintype.card (zpowers i)),
    cycleType, Finset.prod_map_val]

Premises used: Equiv.Perm.cycleType, Equiv.Perm.cycleFactorsFinset, Membership.mem, Fintype.card, Subtype, Finset.prod_map_val, Finset.univ_eq_attach, Subgroup.zpowers, Finset.prod_attach
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
⊢ Eq (α := ℕ) (∏ x ∈ g.cycleFactorsFinset, Fintype.card.{u_1} ↥(zpowers x))
    (∏ a ∈ g.cycleFactorsFinset, (Finset.card ∘ support) a)

Tactic:
Finset.prod_congr rfl (fun x hx ↦ ?_)

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
h : ∀ (x : Perm α) (hx : x ∈ g.cycleFactorsFinset), Fintype.card.{u_1} ↥(zpowers x) = (Finset.card ∘ support) x
⊢ Eq (α := ℕ) (∏ x ∈ g.cycleFactorsFinset, Fintype.card.{u_1} ↥(zpowers x))
    (∏ a ∈ g.cycleFactorsFinset, (Finset.card ∘ support) a)

Tactic:
refine Finset.prod_congr rfl (fun x hx ↦ ?_)

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g x : Perm α
hx : x ∈ g.cycleFactorsFinset
h : orderOf x = (Finset.card ∘ support) x
h₁ : #x.support = (Finset.card ∘ support) x
h₂ h₃ : #x.support = #x.support
⊢ Fintype.card.{u_1} ↥(zpowers x) = (Finset.card ∘ support) x

Tactic:
rw [Fintype.card_zpowers, (mem_cycleFactorsFinset_iff.mp hx).1.orderOf, Function.comp_apply]

Premises used: Equiv.Perm.IsCycle.orderOf, And.left, Equiv.Perm.mem_cycleFactorsFinset_iff, Iff.mp, Function.comp_apply, Fintype.card_zpowers
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
k : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))
rw :
  Eq (α := ℤˣ)
    (∏ i ∈ g.cycleFactorsFinset.attach,
      ((MonoidHom.comp sign (Subgroup.subtype (zpowers (↑i : Perm α))) : ↥(zpowers (↑i : Perm α)) →* ℤˣ) :
          (a : ↥(zpowers (↑i : Perm α))) → ℤˣ)
        (((k, v).1, (k, v).2).2 i))
    (∏ c ∈ g.cycleFactorsFinset.attach, ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (↑(v c) : Perm α))
⊢ ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ)
      ((kerParam g :
          (a :
              Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
                ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α)))) →
            Perm α)
        (k, v)) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ)
      (((sign : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) →* ℤˣ) :
            (a : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)) → ℤˣ)
          k :
        ℤˣ)
      (∏ c : ↥g.cycleFactorsFinset, ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (↑(v c) : Perm α) : ℤˣ)

Tactic:
rw [kerParam, MonoidHom.noncommCoprod_apply, ← Prod.fst_mul_snd ⟨k, v⟩, Prod.mk_mul_mk, mul_one,
    one_mul, map_mul, sign_ofSubtype, Finset.univ_eq_attach, mul_right_inj, ← MonoidHom.comp_apply,
    Subgroup.noncommPiCoprod, MonoidHom.comp_noncommPiCoprod _, MonoidHom.noncommPiCoprod_apply,
    Finset.univ_eq_attach, Finset.noncommProd_eq_prod]

Premises used: Prod.fst_mul_snd, MonoidHom.noncommCoprod_apply, Finset.noncommProd_eq_prod, MonoidHom.noncommPiCoprod_apply, Prod.mk, map_mul, mul_right_inj, forall_imp, Finset.univ_eq_attach, MonoidHom.comp_noncommPiCoprod, Equiv.Perm.OnCycleFactors.kerParam, Prod.mk_mul_mk, Subgroup.noncommPiCoprod, mul_one, MonoidHom.comp_noncommPiCoprod._proof_1, one_mul, Equiv.Perm.sign_ofSubtype, Pairwise.mono, MonoidHom.comp_apply
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
k : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))
⊢ Eq (α := ℤˣ)
    (∏ i ∈ g.cycleFactorsFinset.attach,
      ((MonoidHom.comp sign (Subgroup.subtype (zpowers (↑i : Perm α))) : ↥(zpowers (↑i : Perm α)) →* ℤˣ) :
          (a : ↥(zpowers (↑i : Perm α))) → ℤˣ)
        (((k, v).1, (k, v).2).2 i))
    (∏ c ∈ g.cycleFactorsFinset.attach, ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (↑(v c) : Perm α))

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
k : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))
U : Set ↥g.cycleFactorsFinset := (↑Finset.univ : Set ↥g.cycleFactorsFinset)
c : ↥g.cycleFactorsFinset
h_1 : c ∈ U
d : ↥g.cycleFactorsFinset
h_2 : d ∈ U
h : c ≠ d
obtain :
  ∀ (m : ℤ) (hm : (fun (x : ℤ) ↦ (↑c : Perm α) ^ x) m = (↑(v c) : Perm α)), (↑(v c) : Perm α).Disjoint (↑(v d) : Perm α)
⊢ (↑(v c) : Perm α).Disjoint (↑(v d) : Perm α)

Tactic:
obtain ⟨m, hm⟩ := (v c).prop

Premises used: Subtype.prop