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 α
sc : (c : ↥g.cycleFactorsFinset) → ℕ := fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support
hsc : sc = fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support
this :
  Fintype.card.{u_1} ↥(MonoidHom.range (toPermHom g)) =
    Fintype.card.{u_1}
      (↑{k : Perm ↥g.cycleFactorsFinset | sc ∘ (⇑k : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) = sc} :
        Type u_1)
⊢ Eq (α := ℕ)
    (∏ i ∈ Finset.image (fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support) g.cycleFactorsFinset.attach,
      (Fintype.card.{u_1} { a : ↥g.cycleFactorsFinset // #(↑a : Perm α).support = i })!)
    (∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!)
have simp_rw : Eq (α := ℕ)
  (∏ x ∈ Finset.image (fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support) g.cycleFactorsFinset.attach,
    (Multiset.count x g.cycleType)!)
  (∏ x ∈ g.cycleType.toFinset, (Multiset.count x g.cycleType)!)
Tactic: simp_rw [← CycleType.count_def]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
sc : (c : ↥g.cycleFactorsFinset) → ℕ := fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support
hsc : sc = fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support
this :
  Fintype.card.{u_1} ↥(MonoidHom.range (toPermHom g)) =
    Fintype.card.{u_1}
      (↑{k : Perm ↥g.cycleFactorsFinset | sc ∘ (⇑k : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) = sc} :
        Type u_1)
⊢ Eq (α := ℕ)
    (∏ x ∈ Finset.image (fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support) g.cycleFactorsFinset.attach,
      (Multiset.count x g.cycleType)!)
    (∏ x ∈ g.cycleType.toFinset, (Multiset.count x g.cycleType)!)
have apply : Finset.image (fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support) g.cycleFactorsFinset.attach =
  g.cycleType.toFinset
Tactic: apply Finset.prod_congr _ (fun _ _ => rfl)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
sc : (c : ↥g.cycleFactorsFinset) → ℕ := fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support
hsc : sc = fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support
this :
  Fintype.card.{u_1} ↥(MonoidHom.range (toPermHom g)) =
    Fintype.card.{u_1}
      (↑{k : Perm ↥g.cycleFactorsFinset | sc ∘ (⇑k : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) = sc} :
        Type u_1)
⊢ Finset.image (fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support) g.cycleFactorsFinset.attach =
    g.cycleType.toFinset
have h : ∀ (n : ℕ),
  Membership.mem (γ := Finset ℕ)
      (Finset.image (fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support) g.cycleFactorsFinset.attach) n ↔
    n ∈ g.cycleType.toFinset
Tactic: ext n
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
sc : (c : ↥g.cycleFactorsFinset) → ℕ := fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support
hsc : sc = fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support
this :
  Fintype.card.{u_1} ↥(MonoidHom.range (toPermHom g)) =
    Fintype.card.{u_1}
      (↑{k : Perm ↥g.cycleFactorsFinset | sc ∘ (⇑k : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) = sc} :
        Type u_1)
n : ℕ
⊢ Membership.mem (γ := Finset ℕ)
      (Finset.image (fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support) g.cycleFactorsFinset.attach) n ↔
    n ∈ g.cycleType.toFinset
have h : (∃ a ∈ g.cycleFactorsFinset, #a.support = n) ↔ n ∈ g.cycleType
Tactic: simp only [Finset.mem_image, Finset.mem_attach,
        true_and, Subtype.exists, exists_prop, Multiset.mem_toFinset]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
sc : (c : ↥g.cycleFactorsFinset) → ℕ := fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support
hsc : sc = fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support
⊢ Nat.card.{u_1} ↥(MonoidHom.range (toPermHom g)) = ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
have suffices : Fintype.card.{u_1} ↥(MonoidHom.range (toPermHom g)) =
  Fintype.card.{u_1}
    (↑{k : Perm ↥g.cycleFactorsFinset | sc ∘ (⇑k : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) = sc} :
      Type u_1)
Tactic: suffices Fintype.card (toPermHom g).range =
    Fintype.card { k : Perm g.cycleFactorsFinset | sc ∘ k = sc } by
    simp only [Nat.card_eq_fintype_card, this, Set.coe_setOf, DomMulAct.stabilizer_card', hsc,
      Finset.univ_eq_attach]
    simp_rw [← CycleType.count_def]
    apply Finset.prod_congr _ (fun _ _ => rfl)
    ext n
    simp only [Finset.mem_image, Finset.mem_attach,
        true_and, Subtype.exists, exists_prop, Multiset.mem_toFinset]
    simp only [cycleType_def, Function.comp_apply, Multiset.mem_map, Finset.mem_val]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
sc : (c : ↥g.cycleFactorsFinset) → ℕ := fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support
hsc : sc = fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support
⊢ Fintype.card.{u_1} ↥(MonoidHom.range (toPermHom g)) =
    Fintype.card.{u_1}
      (↑{k : Perm ↥g.cycleFactorsFinset | sc ∘ (⇑k : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) = sc} :
        Type u_1)
have simp : Nat.card.{u_1} ↥(MonoidHom.range (toPermHom g)) =
  Nat.card.{u_1}
    (↑{k : Perm ↥g.cycleFactorsFinset | sc ∘ (⇑k : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) = sc} :
      Type u_1)
Tactic: simp only [Fintype.card_eq_nat_card]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
sc : (c : ↥g.cycleFactorsFinset) → ℕ := fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support
hsc : sc = fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support
⊢ Nat.card.{u_1} ↥(MonoidHom.range (toPermHom g)) =
    Nat.card.{u_1}
      (↑{k : Perm ↥g.cycleFactorsFinset | sc ∘ (⇑k : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) = sc} :
        Type u_1)
have e_α : Eq.{u_1 + 1} (α := Perm ↥g.cycleFactorsFinset → Prop)
  (fun (x : Perm ↥g.cycleFactorsFinset) ↦
    Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (MonoidHom.range (toPermHom g)) x)
  fun (x : Perm ↥g.cycleFactorsFinset) ↦
  Membership.mem (γ := Set (Perm ↥g.cycleFactorsFinset))
    {k : Perm ↥g.cycleFactorsFinset | sc ∘ (⇑k : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) = sc} x
Tactic: congr
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
sc : (c : ↥g.cycleFactorsFinset) → ℕ := fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support
hsc : sc = fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support
⊢ Eq.{u_1 + 1} (α := Perm ↥g.cycleFactorsFinset → Prop)
    (fun (x : Perm ↥g.cycleFactorsFinset) ↦
      Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (MonoidHom.range (toPermHom g)) x)
    fun (x : Perm ↥g.cycleFactorsFinset) ↦
    Membership.mem (γ := Set (Perm ↥g.cycleFactorsFinset))
      {k : Perm ↥g.cycleFactorsFinset | sc ∘ (⇑k : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) = sc} x
have e_α : ∀ (x : Perm ↥g.cycleFactorsFinset),
  Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (MonoidHom.range (toPermHom g)) x ↔
    Membership.mem (γ := Set (Perm ↥g.cycleFactorsFinset))
      {k : Perm ↥g.cycleFactorsFinset | sc ∘ (⇑k : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) = sc} x
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
sc : (c : ↥g.cycleFactorsFinset) → ℕ := fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support
hsc : sc = fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support
x : Perm ↥g.cycleFactorsFinset
⊢ Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (MonoidHom.range (toPermHom g)) x ↔
    Membership.mem (γ := Set (Perm ↥g.cycleFactorsFinset))
      {k : Perm ↥g.cycleFactorsFinset | sc ∘ (⇑k : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) = sc} x
have e_α : (Eq (α := ↥g.cycleFactorsFinset → ℕ)
    ((fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support) ∘
      (⇑x : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset))
    fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support) ↔
  Membership.mem (γ := Set (Perm ↥g.cycleFactorsFinset))
    {k : Perm ↥g.cycleFactorsFinset | sc ∘ (⇑k : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) = sc} x
Tactic: rw [mem_range_toPermHom_iff', Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
sc : (c : ↥g.cycleFactorsFinset) → ℕ := fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support
hsc : sc = fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support
x : Perm ↥g.cycleFactorsFinset
e_α :
  (Eq (α := ↥g.cycleFactorsFinset → ℕ)
      ((fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support) ∘
        (⇑x : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset))
      fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support) ↔
    Membership.mem (γ := Set (Perm ↥g.cycleFactorsFinset))
      {k : Perm ↥g.cycleFactorsFinset | sc ∘ (⇑k : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) = sc} x
⊢ Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (MonoidHom.range (toPermHom g)) x ↔
    Membership.mem (γ := Set (Perm ↥g.cycleFactorsFinset))
      {k : Perm ↥g.cycleFactorsFinset | sc ∘ (⇑k : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) = sc} x
have e_α₁ : (Eq (α := ↥g.cycleFactorsFinset → ℕ)
    ((fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support) ∘
      (⇑x : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset))
    fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support) ↔
  sc ∘ (⇑x : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) = sc
Tactic: rw [mem_range_toPermHom_iff', Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
set set₁ : Nat.card.{u_1} ↥(MonoidHom.range (toPermHom g)) = ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
⊢ Nat.card.{u_1} ↥(MonoidHom.range (toPermHom g)) = ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
have set₂ : let sc : (c : ↥g.cycleFactorsFinset) → ℕ := fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support;
∀ (hsc : sc = fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support),
  Nat.card.{u_1} ↥(MonoidHom.range (toPermHom g)) = ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
Tactic: classical
  set sc := fun (c : g.cycleFactorsFinset) ↦ #c.val.support with hsc
  suffices Fintype.card (toPermHom g).range =
    Fintype.card { k : Perm g.cycleFactorsFinset | sc ∘ k = sc } by
    simp only [Nat.card_eq_fintype_card, this, Set.coe_setOf, DomMulAct.stabilizer_card', hsc,
      Finset.univ_eq_attach]
    simp_rw [← CycleType.count_def]
    apply Finset.prod_congr _ (fun _ _ => rfl)
    ext n
    simp only [Finset.mem_image, Finset.mem_attach,
        true_and, Subtype.exists, exists_prop, Multiset.mem_toFinset]
    simp only [cycleType_def, Function.comp_apply, Multiset.mem_map, Finset.mem_val]
  simp only [Fintype.card_eq_nat_card]
  congr
  ext
  rw [mem_range_toPermHom_iff', Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
set set₁ : Nat.card.{u_1} ↥(MonoidHom.range (toPermHom g)) = ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
set₂ :
  let sc : (c : ↥g.cycleFactorsFinset) → ℕ := fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support;
  ∀ (hsc : sc = fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support),
    Nat.card.{u_1} ↥(MonoidHom.range (toPermHom g)) = ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
⊢ Nat.card.{u_1} ↥(MonoidHom.range (toPermHom g)) = ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
have set₃ : let sc : (c : ↥g.cycleFactorsFinset) → ℕ := fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support;
∀ (hsc : sc = fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support),
  Fintype.card.{u_1} ↥(MonoidHom.range (toPermHom g)) =
    Fintype.card.{u_1}
      (↑{k : Perm ↥g.cycleFactorsFinset | sc ∘ (⇑k : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) = sc} :
        Type u_1)
Tactic: classical
  set sc := fun (c : g.cycleFactorsFinset) ↦ #c.val.support with hsc
  suffices Fintype.card (toPermHom g).range =
    Fintype.card { k : Perm g.cycleFactorsFinset | sc ∘ k = sc } by
    simp only [Nat.card_eq_fintype_card, this, Set.coe_setOf, DomMulAct.stabilizer_card', hsc,
      Finset.univ_eq_attach]
    simp_rw [← CycleType.count_def]
    apply Finset.prod_congr _ (fun _ _ => rfl)
    ext n
    simp only [Finset.mem_image, Finset.mem_attach,
        true_and, Subtype.exists, exists_prop, Multiset.mem_toFinset]
    simp only [cycleType_def, Function.comp_apply, Multiset.mem_map, Finset.mem_val]
  simp only [Fintype.card_eq_nat_card]
  congr
  ext
  rw [mem_range_toPermHom_iff', Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
set set₁ : Nat.card.{u_1} ↥(MonoidHom.range (toPermHom g)) = ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
set₂ :
  let sc : (c : ↥g.cycleFactorsFinset) → ℕ := fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support;
  ∀ (hsc : sc = fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support),
    Nat.card.{u_1} ↥(MonoidHom.range (toPermHom g)) = ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
set₃ :
  let sc : (c : ↥g.cycleFactorsFinset) → ℕ := fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support;
  ∀ (hsc : sc = fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support),
    Fintype.card.{u_1} ↥(MonoidHom.range (toPermHom g)) =
      Fintype.card.{u_1}
        (↑{k : Perm ↥g.cycleFactorsFinset | sc ∘ (⇑k : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) = sc} :
          Type u_1)
⊢ Nat.card.{u_1} ↥(MonoidHom.range (toPermHom g)) = ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
have set₄ : let sc : (c : ↥g.cycleFactorsFinset) → ℕ := fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support;
∀ (hsc : sc = fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support),
  Nat.card.{u_1} ↥(MonoidHom.range (toPermHom g)) =
    Nat.card.{u_1}
      (↑{k : Perm ↥g.cycleFactorsFinset | sc ∘ (⇑k : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) = sc} :
        Type u_1)
Tactic: classical
  set sc := fun (c : g.cycleFactorsFinset) ↦ #c.val.support with hsc
  suffices Fintype.card (toPermHom g).range =
    Fintype.card { k : Perm g.cycleFactorsFinset | sc ∘ k = sc } by
    simp only [Nat.card_eq_fintype_card, this, Set.coe_setOf, DomMulAct.stabilizer_card', hsc,
      Finset.univ_eq_attach]
    simp_rw [← CycleType.count_def]
    apply Finset.prod_congr _ (fun _ _ => rfl)
    ext n
    simp only [Finset.mem_image, Finset.mem_attach,
        true_and, Subtype.exists, exists_prop, Multiset.mem_toFinset]
    simp only [cycleType_def, Function.comp_apply, Multiset.mem_map, Finset.mem_val]
  simp only [Fintype.card_eq_nat_card]
  congr
  ext
  rw [mem_range_toPermHom_iff', Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
set set₁ : Nat.card.{u_1} ↥(MonoidHom.range (toPermHom g)) = ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
set₂ :
  let sc : (c : ↥g.cycleFactorsFinset) → ℕ := fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support;
  ∀ (hsc : sc = fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support),
    Nat.card.{u_1} ↥(MonoidHom.range (toPermHom g)) = ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
set₃ :
  let sc : (c : ↥g.cycleFactorsFinset) → ℕ := fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support;
  ∀ (hsc : sc = fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support),
    Fintype.card.{u_1} ↥(MonoidHom.range (toPermHom g)) =
      Fintype.card.{u_1}
        (↑{k : Perm ↥g.cycleFactorsFinset | sc ∘ (⇑k : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) = sc} :
          Type u_1)
set₄ :
  let sc : (c : ↥g.cycleFactorsFinset) → ℕ := fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support;
  ∀ (hsc : sc = fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support),
    Nat.card.{u_1} ↥(MonoidHom.range (toPermHom g)) =
      Nat.card.{u_1}
        (↑{k : Perm ↥g.cycleFactorsFinset | sc ∘ (⇑k : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) = sc} :
          Type u_1)
⊢ Nat.card.{u_1} ↥(MonoidHom.range (toPermHom g)) = ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
have e_α : let sc : (c : ↥g.cycleFactorsFinset) → ℕ := fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support;
∀ (hsc : sc = fun (c : ↥g.cycleFactorsFinset) ↦ #(↑c : Perm α).support),
  Eq.{u_1 + 1} (α := Perm ↥g.cycleFactorsFinset → Prop)
    (fun (x : Perm ↥g.cycleFactorsFinset) ↦
      Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (MonoidHom.range (toPermHom g)) x)
    fun (x : Perm ↥g.cycleFactorsFinset) ↦
    Membership.mem (γ := Set (Perm ↥g.cycleFactorsFinset))
      {k : Perm ↥g.cycleFactorsFinset | sc ∘ (⇑k : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) = sc} x
Tactic: classical
  set sc := fun (c : g.cycleFactorsFinset) ↦ #c.val.support with hsc
  suffices Fintype.card (toPermHom g).range =
    Fintype.card { k : Perm g.cycleFactorsFinset | sc ∘ k = sc } by
    simp only [Nat.card_eq_fintype_card, this, Set.coe_setOf, DomMulAct.stabilizer_card', hsc,
      Finset.univ_eq_attach]
    simp_rw [← CycleType.count_def]
    apply Finset.prod_congr _ (fun _ _ => rfl)
    ext n
    simp only [Finset.mem_image, Finset.mem_attach,
        true_and, Subtype.exists, exists_prop, Multiset.mem_toFinset]
    simp only [cycleType_def, Function.comp_apply, Multiset.mem_map, Finset.mem_val]
  simp only [Fintype.card_eq_nat_card]
  congr
  ext
  rw [mem_range_toPermHom_iff', Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
u : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))
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 :
      α)
    (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 :
      α)
have pos : ∀ (hx : g.cycleOf x ∈ g.cycleFactorsFinset),
  Eq (α := α)
    ((((kerParam g :
                (a :
                    Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
                      ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α)))) →
                  Perm α)
              (u, v) :
            Perm α) :
          (a : α) → α)
        x :
      α)
    (((↑(v (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α) : (a : α) → α)
        x :
      α)
Tactic: split_ifs with hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
u : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))
x : α
pos :
  ∀ (hx : g.cycleOf x ∈ g.cycleFactorsFinset),
    Eq (α := α)
      ((((kerParam g :
                  (a :
                      Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
                        ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α)))) →
                    Perm α)
                (u, v) :
              Perm α) :
            (a : α) → α)
          x :
        α)
      (((↑(v (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : 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 :
      α)
    (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 :
      α)
have neg : ∀ (hx : g.cycleOf x ∉ g.cycleFactorsFinset),
  Eq (α := α)
    ((((kerParam g :
                (a :
                    Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
                      ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α)))) →
                  Perm α)
              (u, v) :
            Perm α) :
          (a : α) → α)
        x :
      α)
    ((((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 :
      α)
Tactic: split_ifs with hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
u : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
v : (c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α))
x : α
hx hx' : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ Eq (α := α)
    ((((kerParam g :
                (a :
                    Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
                      ((c : ↥g.cycleFactorsFinset) → ↥(zpowers (↑c : Perm α)))) →
                  Perm α)
              (u, v) :
            Perm α) :
          (a : α) → α)
        x :
      α)
    (((↑(v (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx)) : Perm α) : (a : α) → α)
        x :
      α)
have hx'₁ : x ∉ Function.fixedPoints (⇑g : (a : α) → α)
Tactic: rw [cycleOf_mem_cycleFactorsFinset_iff, mem_support, Ne, ← Function.mem_fixedPoints_iff] at hx'
Cleared hypotheses: hx'