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 α
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)!
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)!
⊢ 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}
      ↥(map (Subgroup.subtype (centralizer {g}))
          (MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (OnCycleFactors.toPermHom 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)!
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)!
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}
        ↥(map (Subgroup.subtype (centralizer {g}))
            (MonoidHom.ker (M := Perm ↥g.cycleFactorsFinset) (OnCycleFactors.toPermHom 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.ker (M := Perm ↥g.cycleFactorsFinset) (OnCycleFactors.toPermHom 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 α
⊢ Nat.card.{u_1} (↑{h : Perm α | IsConj g h} : Type u_1) *
      ((Fintype.card α - g.cycleType.sum)! * g.cycleType.prod *
        ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!) =
    (Fintype.card α)!
have rw : Fintype.card.{u_1} (↑{h : Perm α | IsConj g h} : Type u_1) * Nat.card.{u_1} ↥(centralizer {g}) = (Fintype.card α)!
Tactic: rw [Nat.card_eq_fintype_card, ← nat_card_centralizer 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} (↑{h : Perm α | IsConj g h} : Type u_1) * Nat.card.{u_1} ↥(centralizer {g}) = (Fintype.card α)!
have rw : Fintype.card.{u_1} (↑{h : Perm α | IsConj g h} : Type u_1) * Fintype.card.{u_1} ↥(stabilizer (ConjAct (Perm α)) g) =
  (Fintype.card α)!
Tactic: rw [Subgroup.nat_card_centralizer_nat_card_stabilizer, Nat.card_eq_fintype_card]
-- 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} (↑{h : Perm α | IsConj g h} : Type u_1) * Fintype.card.{u_1} ↥(stabilizer (ConjAct (Perm α)) g) =
    (Fintype.card α)!
have h : {h : Perm α | IsConj g h} = orbit (ConjAct (Perm α)) g
Tactic: convert! MulAction.card_orbit_mul_card_stabilizer_eq_card_group (ConjAct (Perm α)) g
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
h : {h : Perm α | IsConj g h} = orbit (ConjAct (Perm α)) g
⊢ Fintype.card.{u_1} (↑{h : Perm α | IsConj g h} : Type u_1) * Fintype.card.{u_1} ↥(stabilizer (ConjAct (Perm α)) g) =
    (Fintype.card α)!
have h₁ : (Fintype.card α)! = Fintype.card.{u_1} (ConjAct (Perm α))
Tactic: convert! MulAction.card_orbit_mul_card_stabilizer_eq_card_group (ConjAct (Perm α)) g
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
⊢ {h : Perm α | IsConj g h} = orbit (ConjAct (Perm α)) g
have h : ∀ (h : Perm α), Membership.mem (γ := Set (Perm α)) {h : Perm α | IsConj g h} h ↔ h ∈ orbit (ConjAct (Perm α)) g
Tactic: ext h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
⊢ (Fintype.card α)! = Fintype.card.{u_1} (ConjAct (Perm α))
have h : (Fintype.card α)! = Fintype.card.{u_1} (Perm α)
Tactic: rw [ConjAct.card, Fintype.card_perm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
h : (Fintype.card α)! = Fintype.card.{u_1} (Perm α)
⊢ (Fintype.card α)! = Fintype.card.{u_1} (ConjAct (Perm α))
have h₁ : (Fintype.card α)! = (Fintype.card α)!
Tactic: rw [ConjAct.card, Fintype.card_perm]
-- 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} (↑{h : Perm α | IsConj g h} : Type u_1) *
      ((Fintype.card α - g.cycleType.sum)! * g.cycleType.prod *
        ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!) =
    (Fintype.card α)!
have rw : Fintype.card.{u_1} (↑{h : Perm α | IsConj g h} : Type u_1) *
    ((Fintype.card α - g.cycleType.sum)! * g.cycleType.prod *
      ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!) =
  (Fintype.card α)!
Tactic: classical
  rw [Nat.card_eq_fintype_card, ← nat_card_centralizer g]
  rw [Subgroup.nat_card_centralizer_nat_card_stabilizer, Nat.card_eq_fintype_card]
  convert! MulAction.card_orbit_mul_card_stabilizer_eq_card_group (ConjAct (Perm α)) g
  · ext h
    simp only [Set.mem_setOf_eq, ConjAct.mem_orbit_conjAct, isConj_comm]
  · rw [ConjAct.card, Fintype.card_perm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
rw :
  Fintype.card.{u_1} (↑{h : Perm α | IsConj g h} : Type u_1) *
      ((Fintype.card α - g.cycleType.sum)! * g.cycleType.prod *
        ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!) =
    (Fintype.card α)!
⊢ Nat.card.{u_1} (↑{h : Perm α | IsConj g h} : Type u_1) *
      ((Fintype.card α - g.cycleType.sum)! * g.cycleType.prod *
        ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!) =
    (Fintype.card α)!
have rw₁ : Fintype.card.{u_1} (↑{h : Perm α | IsConj g h} : Type u_1) * Nat.card.{u_1} ↥(centralizer {g}) = (Fintype.card α)!
Tactic: classical
  rw [Nat.card_eq_fintype_card, ← nat_card_centralizer g]
  rw [Subgroup.nat_card_centralizer_nat_card_stabilizer, Nat.card_eq_fintype_card]
  convert! MulAction.card_orbit_mul_card_stabilizer_eq_card_group (ConjAct (Perm α)) g
  · ext h
    simp only [Set.mem_setOf_eq, ConjAct.mem_orbit_conjAct, isConj_comm]
  · rw [ConjAct.card, Fintype.card_perm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
rw :
  Fintype.card.{u_1} (↑{h : Perm α | IsConj g h} : Type u_1) *
      ((Fintype.card α - g.cycleType.sum)! * g.cycleType.prod *
        ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!) =
    (Fintype.card α)!
rw₁ rw₂ rw₃ :
  Fintype.card.{u_1} (↑{h : Perm α | IsConj g h} : Type u_1) * Nat.card.{u_1} ↥(centralizer {g}) = (Fintype.card α)!
⊢ Nat.card.{u_1} (↑{h : Perm α | IsConj g h} : Type u_1) *
      ((Fintype.card α - g.cycleType.sum)! * g.cycleType.prod *
        ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!) =
    (Fintype.card α)!
have rw₄ : Fintype.card.{u_1} (↑{h : Perm α | IsConj g h} : Type u_1) * Fintype.card.{u_1} ↥(stabilizer (ConjAct (Perm α)) g) =
  (Fintype.card α)!
Tactic: classical
  rw [Nat.card_eq_fintype_card, ← nat_card_centralizer g]
  rw [Subgroup.nat_card_centralizer_nat_card_stabilizer, Nat.card_eq_fintype_card]
  convert! MulAction.card_orbit_mul_card_stabilizer_eq_card_group (ConjAct (Perm α)) g
  · ext h
    simp only [Set.mem_setOf_eq, ConjAct.mem_orbit_conjAct, isConj_comm]
  · rw [ConjAct.card, Fintype.card_perm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
rw :
  Fintype.card.{u_1} (↑{h : Perm α | IsConj g h} : Type u_1) *
      ((Fintype.card α - g.cycleType.sum)! * g.cycleType.prod *
        ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!) =
    (Fintype.card α)!
rw₁ rw₂ rw₃ :
  Fintype.card.{u_1} (↑{h : Perm α | IsConj g h} : Type u_1) * Nat.card.{u_1} ↥(centralizer {g}) = (Fintype.card α)!
rw₄ :
  Fintype.card.{u_1} (↑{h : Perm α | IsConj g h} : Type u_1) * Fintype.card.{u_1} ↥(stabilizer (ConjAct (Perm α)) g) =
    (Fintype.card α)!
⊢ Nat.card.{u_1} (↑{h : Perm α | IsConj g h} : Type u_1) *
      ((Fintype.card α - g.cycleType.sum)! * g.cycleType.prod *
        ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!) =
    (Fintype.card α)!
have h : {h : Perm α | IsConj g h} = orbit (ConjAct (Perm α)) g
Tactic: classical
  rw [Nat.card_eq_fintype_card, ← nat_card_centralizer g]
  rw [Subgroup.nat_card_centralizer_nat_card_stabilizer, Nat.card_eq_fintype_card]
  convert! MulAction.card_orbit_mul_card_stabilizer_eq_card_group (ConjAct (Perm α)) g
  · ext h
    simp only [Set.mem_setOf_eq, ConjAct.mem_orbit_conjAct, isConj_comm]
  · rw [ConjAct.card, Fintype.card_perm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
rw :
  Fintype.card.{u_1} (↑{h : Perm α | IsConj g h} : Type u_1) *
      ((Fintype.card α - g.cycleType.sum)! * g.cycleType.prod *
        ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!) =
    (Fintype.card α)!
rw₁ rw₂ rw₃ :
  Fintype.card.{u_1} (↑{h : Perm α | IsConj g h} : Type u_1) * Nat.card.{u_1} ↥(centralizer {g}) = (Fintype.card α)!
rw₄ :
  Fintype.card.{u_1} (↑{h : Perm α | IsConj g h} : Type u_1) * Fintype.card.{u_1} ↥(stabilizer (ConjAct (Perm α)) g) =
    (Fintype.card α)!
h : {h : Perm α | IsConj g h} = orbit (ConjAct (Perm α)) g
⊢ Nat.card.{u_1} (↑{h : Perm α | IsConj g h} : Type u_1) *
      ((Fintype.card α - g.cycleType.sum)! * g.cycleType.prod *
        ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!) =
    (Fintype.card α)!
have h₁ : (Fintype.card α)! = Fintype.card.{u_1} (ConjAct (Perm α))
Tactic: classical
  rw [Nat.card_eq_fintype_card, ← nat_card_centralizer g]
  rw [Subgroup.nat_card_centralizer_nat_card_stabilizer, Nat.card_eq_fintype_card]
  convert! MulAction.card_orbit_mul_card_stabilizer_eq_card_group (ConjAct (Perm α)) g
  · ext h
    simp only [Set.mem_setOf_eq, ConjAct.mem_orbit_conjAct, isConj_comm]
  · rw [ConjAct.card, Fintype.card_perm]
-- 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} (↑{h : Perm α | IsConj g h} : Type u_1) =
    (Fintype.card α)! /
      ((Fintype.card α - g.cycleType.sum)! * g.cycleType.prod *
        ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!)
have rw : Nat.card.{u_1} (↑{h : Perm α | IsConj g h} : Type u_1) *
    ((Fintype.card α - g.cycleType.sum)! * g.cycleType.prod *
      ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!) =
  Nat.card.{u_1} (↑{h : Perm α | IsConj g h} : Type u_1) *
    ((Fintype.card α - g.cycleType.sum)! * g.cycleType.prod *
      ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!)
Tactic: rw [← card_isConj_mul_eq g, Nat.div_eq_of_eq_mul_left _]
-- 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} (↑{h : Perm α | IsConj g h} : Type u_1) *
      ((Fintype.card α - g.cycleType.sum)! * g.cycleType.prod *
        ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!) =
    Nat.card.{u_1} (↑{h : Perm α | IsConj g h} : Type u_1) *
      ((Fintype.card α - g.cycleType.sum)! * g.cycleType.prod *
        ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!)
⊢ Nat.card.{u_1} (↑{h : Perm α | IsConj g h} : Type u_1) =
    (Fintype.card α)! /
      ((Fintype.card α - g.cycleType.sum)! * g.cycleType.prod *
        ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!)
have rw₁ : 0 < (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod * ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
Tactic: rw [← card_isConj_mul_eq g, Nat.div_eq_of_eq_mul_left _]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
⊢ 0 <
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod * ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!
have rw : 0 < Nat.card.{u_1} ↥(centralizer {g})
Tactic: rw [← nat_card_centralizer g]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
⊢ Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} = 0 ↔ ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
have rw : (∀ ⦃x : Perm α⦄, Membership.mem (γ := Finset (Perm α)) Finset.univ x → ¬x.cycleType = m) ↔
  ∀ (x : Perm α), ¬x.cycleType = m
Tactic: rw [Finset.card_eq_zero, Finset.filter_eq_empty_iff,
    ← exists_with_cycleType_iff, not_exists]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
⊢ Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} *
      ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) =
    if m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then (Fintype.card α)! else 0
have pos : ∀ (hm : m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a),
  Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} *
      ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) =
    (Fintype.card α)!
Tactic: split_ifs with hm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
pos :
  ∀ (hm : m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a),
    Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} *
        ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) =
      (Fintype.card α)!
⊢ Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} *
      ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) =
    if m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then (Fintype.card α)! else 0
have neg : ∀ (hm : ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)),
  Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} *
      ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) =
    0
Tactic: split_ifs with hm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hm : m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
⊢ Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} *
      ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) =
    (Fintype.card α)!
have pos : ∀ (g : Perm α) (hm : g.cycleType.sum ≤ Fintype.card α ∧ ∀ a ∈ g.cycleType, 2 ≤ a),
  Finset.card.{u_1} (α := Perm α) {g_1 : Perm α | g_1.cycleType = g.cycleType} *
      ((Fintype.card α - g.cycleType.sum)! * g.cycleType.prod *
        ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!) =
    (Fintype.card α)!
Tactic: obtain ⟨g, rfl⟩ := (exists_with_cycleType_iff α).mpr hm
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
hm : g.cycleType.sum ≤ Fintype.card α ∧ ∀ a ∈ g.cycleType, 2 ≤ a
⊢ Finset.card.{u_1} (α := Perm α) {g_1 : Perm α | g_1.cycleType = g.cycleType} *
      ((Fintype.card α - g.cycleType.sum)! * g.cycleType.prod *
        ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!) =
    (Fintype.card α)!
have h : Finset.card.{u_1} (α := Perm α) {g_1 : Perm α | g_1.cycleType = g.cycleType} =
  Nat.card.{u_1} (↑{h : Perm α | IsConj g h} : Type u_1)
Tactic: convert! card_isConj_mul_eq g
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
hm : g.cycleType.sum ≤ Fintype.card α ∧ ∀ a ∈ g.cycleType, 2 ≤ a
⊢ Finset.card.{u_1} (α := Perm α) {g_1 : Perm α | g_1.cycleType = g.cycleType} =
    Nat.card.{u_1} (↑{h : Perm α | IsConj g h} : Type u_1)
have h : Finset.card.{u_1} (α := Perm α) {g_1 : Perm α | g_1.cycleType = g.cycleType} =
  Nat.card.{u_1} { h : Perm α // IsConj g h }
Tactic: simp_rw [Set.coe_setOf, Nat.card_eq_fintype_card, ← Fintype.card_coe, Finset.mem_filter,
      Finset.mem_univ, true_and, ← isConj_iff_cycleType_eq, isConj_comm (g := g)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
hm : g.cycleType.sum ≤ Fintype.card α ∧ ∀ a ∈ g.cycleType, 2 ≤ a
h :
  Finset.card.{u_1} (α := Perm α) {g_1 : Perm α | g_1.cycleType = g.cycleType} =
    Nat.card.{u_1} { h : Perm α // IsConj g h }
⊢ Finset.card.{u_1} (α := Perm α) {g_1 : Perm α | g_1.cycleType = g.cycleType} =
    Nat.card.{u_1} (↑{h : Perm α | IsConj g h} : Type u_1)
have h₁ : Finset.card.{u_1} (α := Perm α) {g_1 : Perm α | g_1.cycleType = g.cycleType} =
  Fintype.card.{u_1} { h : Perm α // IsConj g h }
Tactic: simp_rw [Set.coe_setOf, Nat.card_eq_fintype_card, ← Fintype.card_coe, Finset.mem_filter,
      Finset.mem_univ, true_and, ← isConj_iff_cycleType_eq, isConj_comm (g := g)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
hm : g.cycleType.sum ≤ Fintype.card α ∧ ∀ a ∈ g.cycleType, 2 ≤ a
h :
  Finset.card.{u_1} (α := Perm α) {g_1 : Perm α | g_1.cycleType = g.cycleType} =
    Nat.card.{u_1} { h : Perm α // IsConj g h }
h₁ :
  Finset.card.{u_1} (α := Perm α) {g_1 : Perm α | g_1.cycleType = g.cycleType} =
    Fintype.card.{u_1} { h : Perm α // IsConj g h }
⊢ Finset.card.{u_1} (α := Perm α) {g_1 : Perm α | g_1.cycleType = g.cycleType} =
    Nat.card.{u_1} (↑{h : Perm α | IsConj g h} : Type u_1)
have h₂ : Fintype.card.{u_1} ↥{g_1 : Perm α | g_1.cycleType = g.cycleType} = Fintype.card.{u_1} { h : Perm α // IsConj g h }
Tactic: simp_rw [Set.coe_setOf, Nat.card_eq_fintype_card, ← Fintype.card_coe, Finset.mem_filter,
      Finset.mem_univ, true_and, ← isConj_iff_cycleType_eq, isConj_comm (g := g)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
hm : g.cycleType.sum ≤ Fintype.card α ∧ ∀ a ∈ g.cycleType, 2 ≤ a
h :
  Finset.card.{u_1} (α := Perm α) {g_1 : Perm α | g_1.cycleType = g.cycleType} =
    Nat.card.{u_1} { h : Perm α // IsConj g h }
h₁ :
  Finset.card.{u_1} (α := Perm α) {g_1 : Perm α | g_1.cycleType = g.cycleType} =
    Fintype.card.{u_1} { h : Perm α // IsConj g h }
h₂ : Fintype.card.{u_1} ↥{g_1 : Perm α | g_1.cycleType = g.cycleType} = Fintype.card.{u_1} { h : Perm α // IsConj g h }
⊢ Finset.card.{u_1} (α := Perm α) {g_1 : Perm α | g_1.cycleType = g.cycleType} =
    Nat.card.{u_1} (↑{h : Perm α | IsConj g h} : Type u_1)
have h₃ : Fintype.card.{u_1} { x : Perm α // Membership.mem (γ := Finset (Perm α)) Finset.univ x ∧ x.cycleType = g.cycleType } =
  Fintype.card.{u_1} { h : Perm α // IsConj g h }
Tactic: simp_rw [Set.coe_setOf, Nat.card_eq_fintype_card, ← Fintype.card_coe, Finset.mem_filter,
      Finset.mem_univ, true_and, ← isConj_iff_cycleType_eq, isConj_comm (g := g)]