awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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
⊢ 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 : α)
have 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) :
              α))
          sorry) :
      α) :
    α)
  (((↑p : Perm α) : (a : α) → α) x : α)
Tactic: rwa [ofSubtype_apply_of_mem, subtypePerm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
⊢ MonoidHom.range (G :=
      Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
        ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))))
      (kerParam g) ≤
    centralizer {g}
have rw : map (Subgroup.subtype (centralizer {g})) (MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (toPermHom g)) ≤
  centralizer {g}
Tactic: rw [kerParam_range_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
⊢ 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
have 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
Tactic: rw [Fintype.card_coeSort_range (kerParam_injective g)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
⊢ 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
have rw : (Fintype.card α - g.cycleType.sum)! * ∏ i : ↥g.cycleFactorsFinset, Fintype.card.{u_1} ↥(zpowers (↑i : Perm α)) =
  (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod
Tactic: rw [Fintype.card_prod, Fintype.card_perm, Fintype.card_pi, card_fixedPoints]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
⊢ (Fintype.card α - g.cycleType.sum)! * ∏ i : ↥g.cycleFactorsFinset, Fintype.card.{u_1} ↥(zpowers (↑i : Perm α)) =
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod
have h : ∏ i : ↥g.cycleFactorsFinset, Fintype.card.{u_1} ↥(zpowers (↑i : Perm α)) = g.cycleType.prod
Tactic: apply congr_arg
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
⊢ ∏ i : ↥g.cycleFactorsFinset, Fintype.card.{u_1} ↥(zpowers (↑i : Perm α)) = g.cycleType.prod
have h : Eq (α := ℕ) (∏ x ∈ g.cycleFactorsFinset, Fintype.card.{u_1} ↥(zpowers x))
  (∏ a ∈ g.cycleFactorsFinset, (Finset.card ∘ support) a)
Tactic: rw [Finset.univ_eq_attach, g.cycleFactorsFinset.prod_attach (fun i ↦ Fintype.card (zpowers i)),
    cycleType, Finset.prod_map_val]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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)
have h : ∀ (x : Perm α) (hx : x ∈ g.cycleFactorsFinset), Fintype.card.{u_1} ↥(zpowers x) = (Finset.card ∘ support) x
Tactic: refine Finset.prod_congr rfl (fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g x : Perm α
hx : x ∈ g.cycleFactorsFinset
⊢ Fintype.card.{u_1} ↥(zpowers x) = (Finset.card ∘ support) x
have h : orderOf x = (Finset.card ∘ support) x
Tactic: rw [Fintype.card_zpowers, (mem_cycleFactorsFinset_iff.mp hx).1.orderOf, Function.comp_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g x : Perm α
hx : x ∈ g.cycleFactorsFinset
h : orderOf x = (Finset.card ∘ support) x
⊢ Fintype.card.{u_1} ↥(zpowers x) = (Finset.card ∘ support) x
have h₁ : #x.support = (Finset.card ∘ support) x
Tactic: rw [Fintype.card_zpowers, (mem_cycleFactorsFinset_iff.mp hx).1.orderOf, Function.comp_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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
⊢ Fintype.card.{u_1} ↥(zpowers x) = (Finset.card ∘ support) x
have h₂ : #x.support = #x.support
Tactic: rw [Fintype.card_zpowers, (mem_cycleFactorsFinset_iff.mp hx).1.orderOf, Function.comp_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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 α))
⊢ ((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 α) : ℤˣ)
have 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 α))
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]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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
⊢ (fun (i j : ↥g.cycleFactorsFinset) ↦ (↑(v i) : Perm α).Disjoint (↑(v j) : Perm α)) c d
have obtain : ∀ (m : ℤ) (hm : (fun (x : ℤ) ↦ (↑c : Perm α) ^ x) m = (↑(v c) : Perm α)), (↑(v c) : Perm α).Disjoint (↑(v d) : Perm α)
Tactic: obtain ⟨m, hm⟩ := (v c).prop
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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
m : ℤ
hm : (fun (x : ℤ) ↦ (↑c : Perm α) ^ x) m = (↑(v c) : Perm α)
⊢ (↑(v c) : Perm α).Disjoint (↑(v d) : Perm α)
have obtain : ∀ (n : ℤ) (hn : (fun (x : ℤ) ↦ (↑d : Perm α) ^ x) n = (↑(v d) : Perm α)), (↑(v c) : Perm α).Disjoint (↑(v d) : Perm α)
Tactic: obtain ⟨n, hn⟩ := (v d).prop
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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
m : ℤ
hm : (fun (x : ℤ) ↦ (↑c : Perm α) ^ x) m = (↑(v c) : Perm α)
n : ℤ
hn : (fun (x : ℤ) ↦ (↑d : Perm α) ^ x) n = (↑(v d) : Perm α)
⊢ (↑(v c) : Perm α).Disjoint (↑(v d) : Perm α)
have simp : ((↑c : Perm α) ^ m).Disjoint ((↑d : Perm α) ^ n)
Tactic: simp only [← hm, ← hn]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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
m : ℤ
hm : (fun (x : ℤ) ↦ (↑c : Perm α) ^ x) m = (↑(v c) : Perm α)
n : ℤ
hn : (fun (x : ℤ) ↦ (↑d : Perm α) ^ x) n = (↑(v d) : Perm α)
⊢ ((↑c : Perm α) ^ m).Disjoint ((↑d : Perm α) ^ n)
have hστ : (↑c : Perm α).Disjoint (↑d : Perm α)
Tactic: apply Disjoint.zpow_disjoint_zpow
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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
m : ℤ
hm : (fun (x : ℤ) ↦ (↑c : Perm α) ^ x) m = (↑(v c) : Perm α)
n : ℤ
hn : (fun (x : ℤ) ↦ (↑d : Perm α) ^ x) n = (↑(v d) : Perm α)
⊢ (↑c : Perm α).Disjoint (↑d : Perm α)
have hστ : (↑c : Perm α) ≠ (↑d : Perm α)
Tactic: apply cycleFactorsFinset_pairwise_disjoint g c.prop d.prop
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (hypothesis)
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)
⊢ cycleType.{u_1} (α := α)
      ((kerParam g :
          (a :
              Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
                ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α)))) →
            Perm α)
        (k, v)) =
    k.cycleType + ∑ c : ↥g.cycleFactorsFinset, (↑(v c) : Perm α).cycleType
have hU : U.Pairwise fun (i j : ↥g.cycleFactorsFinset) ↦ (↑(v i) : Perm α).Disjoint (↑(v j) : Perm α)
Tactic: have hU : U.Pairwise fun i j ↦ (v i).val.Disjoint (v j).val := fun c _ d _ h ↦ by
    obtain ⟨m, hm⟩ := (v c).prop
    obtain ⟨n, hn⟩ := (v d).prop
    simp only [← hm, ← hn]
    apply Disjoint.zpow_disjoint_zpow
    apply cycleFactorsFinset_pairwise_disjoint g c.prop d.prop
    exact Subtype.coe_ne_coe.mpr h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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)
hU : U.Pairwise fun (i j : ↥g.cycleFactorsFinset) ↦ (↑(v i) : Perm α).Disjoint (↑(v j) : Perm α)
⊢ cycleType.{u_1} (α := α)
      ((kerParam g :
          (a :
              Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
                ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α)))) →
            Perm α)
        (k, v)) =
    k.cycleType + ∑ c : ↥g.cycleFactorsFinset, (↑(v c) : Perm α).cycleType
have rw : cycleType.{u_1} (α := α)
      ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x) :
          (a : Perm { x : α // x ∈ Function.fixedPoints (⇑g : (a : α) → α) }) → Perm α)
        k) +
    ∑ i ∈ g.cycleFactorsFinset.attach, (↑(v i) : Perm α).cycleType =
  k.cycleType + ∑ c ∈ g.cycleFactorsFinset.attach, (↑(v c) : Perm α).cycleType
Tactic: rw [kerParam, MonoidHom.noncommCoprod_apply, ← Prod.fst_mul_snd ⟨k, v⟩, Prod.mk_mul_mk, mul_one,
    one_mul, Finset.univ_eq_attach,
    Disjoint.cycleType_mul (disjoint_ofSubtype_noncommPiCoprod g k v),
    Subgroup.noncommPiCoprod_apply, Disjoint.cycleType_noncommProd hU, Finset.univ_eq_attach]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
⊢ Nat.card.{u_1} ↥(centralizer {g}) =
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod * ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
have rw : Nat.card.{u_1} ↥(MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (OnCycleFactors.toPermHom g)) *
    (MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (OnCycleFactors.toPermHom g)).index =
  (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod * ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
Tactic: rw [← (toPermHom g).ker.card_mul_index, index_ker, nat_card_range_toPermHom,
    ← kerParam_range_card, ← Nat.card_eq_fintype_card, kerParam_range_eq, card_subtype]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
rw :
  Nat.card.{u_1} ↥(MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (OnCycleFactors.toPermHom g)) *
      (MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (OnCycleFactors.toPermHom g)).index =
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod * ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
⊢ Nat.card.{u_1} ↥(centralizer {g}) =
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod * ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
have rw₁ : Nat.card.{u_1} ↥(MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (OnCycleFactors.toPermHom g)) *
    Nat.card.{u_1} ↥(MonoidHom.range (OnCycleFactors.toPermHom g)) =
  (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod * ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
Tactic: rw [← (toPermHom g).ker.card_mul_index, index_ker, nat_card_range_toPermHom,
    ← kerParam_range_card, ← Nat.card_eq_fintype_card, kerParam_range_eq, card_subtype]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
rw :
  Nat.card.{u_1} ↥(MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (OnCycleFactors.toPermHom g)) *
      (MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (OnCycleFactors.toPermHom g)).index =
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod * ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
rw₁ :
  Nat.card.{u_1} ↥(MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (OnCycleFactors.toPermHom g)) *
      Nat.card.{u_1} ↥(MonoidHom.range (OnCycleFactors.toPermHom g)) =
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod * ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
⊢ Nat.card.{u_1} ↥(centralizer {g}) =
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod * ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
have rw₂ : Nat.card.{u_1} ↥(MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (OnCycleFactors.toPermHom g)) *
    ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)! =
  (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod * ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
Tactic: rw [← (toPermHom g).ker.card_mul_index, index_ker, nat_card_range_toPermHom,
    ← kerParam_range_card, ← Nat.card_eq_fintype_card, kerParam_range_eq, card_subtype]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
rw :
  Nat.card.{u_1} ↥(MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (OnCycleFactors.toPermHom g)) *
      (MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (OnCycleFactors.toPermHom g)).index =
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod * ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
rw₁ :
  Nat.card.{u_1} ↥(MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (OnCycleFactors.toPermHom g)) *
      Nat.card.{u_1} ↥(MonoidHom.range (OnCycleFactors.toPermHom g)) =
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod * ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
rw₂ :
  Nat.card.{u_1} ↥(MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (OnCycleFactors.toPermHom g)) *
      ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)! =
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod * ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
⊢ Nat.card.{u_1} ↥(centralizer {g}) =
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod * ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
have rw₃ : Nat.card.{u_1} ↥(MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (OnCycleFactors.toPermHom g)) *
    ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)! =
  Fintype.card.{u_1}
      ↥(MonoidHom.range (G :=
          Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
            ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))))
          (kerParam g)) *
    ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
Tactic: rw [← (toPermHom g).ker.card_mul_index, index_ker, nat_card_range_toPermHom,
    ← kerParam_range_card, ← Nat.card_eq_fintype_card, kerParam_range_eq, card_subtype]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
rw :
  Nat.card.{u_1} ↥(MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (OnCycleFactors.toPermHom g)) *
      (MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (OnCycleFactors.toPermHom g)).index =
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod * ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
rw₁ :
  Nat.card.{u_1} ↥(MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (OnCycleFactors.toPermHom g)) *
      Nat.card.{u_1} ↥(MonoidHom.range (OnCycleFactors.toPermHom g)) =
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod * ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
rw₂ :
  Nat.card.{u_1} ↥(MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (OnCycleFactors.toPermHom g)) *
      ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)! =
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod * ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
rw₃ :
  Nat.card.{u_1} ↥(MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (OnCycleFactors.toPermHom g)) *
      ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)! =
    Fintype.card.{u_1}
        ↥(MonoidHom.range (G :=
            Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
              ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))))
            (kerParam g)) *
      ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
⊢ Nat.card.{u_1} ↥(centralizer {g}) =
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod * ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
have rw₄ : Nat.card.{u_1} ↥(MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (OnCycleFactors.toPermHom g)) *
    ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)! =
  Nat.card.{u_1}
      ↥(MonoidHom.range (G :=
          Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
            ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))))
          (kerParam g)) *
    ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
Tactic: rw [← (toPermHom g).ker.card_mul_index, index_ker, nat_card_range_toPermHom,
    ← kerParam_range_card, ← Nat.card_eq_fintype_card, kerParam_range_eq, card_subtype]