awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
m : ℤ
hm : (fun (x : ℤ) ↦ (↑c : Perm α) ^ x) m = (↑(v c) : Perm α)
obtain :
  ∀ (n : ℤ) (hn : (fun (x : ℤ) ↦ (↑d : Perm α) ^ x) n = (↑(v d) : Perm α)), (↑(v c) : Perm α).Disjoint (↑(v d) : Perm α)
⊢ (↑(v c) : Perm α).Disjoint (↑(v d) : Perm α)

Tactic:
obtain ⟨n, hn⟩ := (v d).prop

Premises used: Subtype.prop
-- 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
m : ℤ
hm : (fun (x : ℤ) ↦ (↑c : Perm α) ^ x) m = (↑(v c) : Perm α)
n : ℤ
hn : (fun (x : ℤ) ↦ (↑d : Perm α) ^ x) n = (↑(v d) : Perm α)
simp : ((↑c : Perm α) ^ m).Disjoint ((↑d : Perm α) ^ n)
⊢ (↑(v c) : Perm α).Disjoint (↑(v d) : Perm α)

Tactic:
simp only [← hm, ← hn]
-- 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
m : ℤ
hm : (fun (x : ℤ) ↦ (↑c : Perm α) ^ x) m = (↑(v c) : Perm α)
n : ℤ
hn : (fun (x : ℤ) ↦ (↑d : Perm α) ^ x) n = (↑(v d) : Perm α)
hστ : (↑c : Perm α).Disjoint (↑d : Perm α)
⊢ ((↑c : Perm α) ^ m).Disjoint ((↑d : Perm α) ^ n)

Tactic:
apply Disjoint.zpow_disjoint_zpow

Premises used: Equiv.Perm.Disjoint.zpow_disjoint_zpow
-- 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
m : ℤ
hm : (fun (x : ℤ) ↦ (↑c : Perm α) ^ x) m = (↑(v c) : Perm α)
n : ℤ
hn : (fun (x : ℤ) ↦ (↑d : Perm α) ^ x) n = (↑(v d) : Perm α)
hστ : (↑c : Perm α) ≠ (↑d : Perm α)
⊢ (↑c : Perm α).Disjoint (↑d : Perm α)

Tactic:
apply cycleFactorsFinset_pairwise_disjoint g c.prop d.prop

Premises used: Equiv.Perm.cycleFactorsFinset_pairwise_disjoint, Subtype.prop
-- 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
m : ℤ
hm : (fun (x : ℤ) ↦ (↑c : Perm α) ^ x) m = (↑(v c) : Perm α)
n : ℤ
hn : (fun (x : ℤ) ↦ (↑d : Perm α) ^ x) n = (↑(v d) : Perm α)
⊢ (↑c : Perm α) ≠ (↑d : Perm α)

Tactic:
Subtype.coe_ne_coe.mpr h

Premises used: Iff.mpr, Subtype.coe_ne_coe
-- 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
m : ℤ
hm : (fun (x : ℤ) ↦ (↑c : Perm α) ^ x) m = (↑(v c) : Perm α)
n : ℤ
hn : (fun (x : ℤ) ↦ (↑d : Perm α) ^ x) n = (↑(v d) : Perm α)
⊢ (↑c : Perm α) ≠ (↑d : Perm α)

Tactic:
exact Subtype.coe_ne_coe.mpr h

Premises used: Iff.mpr, Subtype.coe_ne_coe
-- 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)
⊢ 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
-- 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)
hU : U.Pairwise fun (i j : ↥g.cycleFactorsFinset) ↦ (↑(v i) : Perm α).Disjoint (↑(v j) : Perm α)
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
⊢ 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

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]

Premises used: Prod.fst_mul_snd, Equiv.Perm.disjoint_ofSubtype_noncommPiCoprod, MonoidHom.noncommCoprod_apply, Equiv.Perm.Disjoint.commute, Subgroup.noncommPiCoprod_apply, Prod.mk, Finset.univ_eq_attach, Equiv.Perm.OnCycleFactors.kerParam, Prod.mk_mul_mk, Equiv.Perm.Disjoint.cycleType_mul, Set.Pairwise.imp, mul_one, Equiv.Perm.Disjoint.cycleType_noncommProd, one_mul
-- 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)
hU : U.Pairwise fun (i j : ↥g.cycleFactorsFinset) ↦ (↑(v i) : Perm α).Disjoint (↑(v j) : Perm α)
⊢ 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:
congr_arg₂ _ cycleType_ofSubtype rfl

Premises used: Equiv.Perm.cycleType_ofSubtype, rfl, congr_arg₂
-- 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)
hU : U.Pairwise fun (i j : ↥g.cycleFactorsFinset) ↦ (↑(v i) : Perm α).Disjoint (↑(v j) : Perm α)
⊢ 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:
exact congr_arg₂ _ cycleType_ofSubtype rfl

Premises used: Equiv.Perm.cycleType_ofSubtype, rfl, congr_arg₂
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
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 α)!

Tactic:
rw [Nat.card_eq_fintype_card, ← nat_card_centralizer g]

Premises used: Nat.card_eq_fintype_card, Equiv.Perm.nat_card_centralizer
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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.{u_1} ↥(stabilizer (ConjAct (Perm α)) g) =
    (Fintype.card α)!
⊢ Fintype.card.{u_1} (↑{h : Perm α | IsConj g h} : Type u_1) * Nat.card.{u_1} ↥(centralizer {g}) = (Fintype.card α)!

Tactic:
rw [Subgroup.nat_card_centralizer_nat_card_stabilizer, Nat.card_eq_fintype_card]

Premises used: Subgroup.nat_card_centralizer_nat_card_stabilizer, Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
⊢ Fintype.card.{u_1} (↑(orbit (ConjAct (Perm α)) g) : Type u_1) *
      Fintype.card.{u_1} ↥(stabilizer (ConjAct (Perm α)) g) =
    Fintype.card.{u_1} (ConjAct (Perm α))

Tactic:
MulAction.card_orbit_mul_card_stabilizer_eq_card_group (ConjAct (Perm α)) g

Premises used: Equiv.Perm, MulAction.card_orbit_mul_card_stabilizer_eq_card_group, ConjAct
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
h : {h : Perm α | IsConj g h} = orbit (ConjAct (Perm α)) g
h₁ : (Fintype.card α)! = Fintype.card.{u_1} (ConjAct (Perm α))
⊢ Fintype.card.{u_1} (↑{h : Perm α | IsConj g h} : Type u_1) * Fintype.card.{u_1} ↥(stabilizer (ConjAct (Perm α)) g) =
    (Fintype.card α)!

Tactic:
convert! MulAction.card_orbit_mul_card_stabilizer_eq_card_group (ConjAct (Perm α)) g

Premises used: Equiv.Perm, MulAction.card_orbit_mul_card_stabilizer_eq_card_group, ConjAct
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
h : ∀ (h : Perm α), Membership.mem (γ := Set (Perm α)) {h : Perm α | IsConj g h} h ↔ h ∈ orbit (ConjAct (Perm α)) g
⊢ {h : Perm α | IsConj g h} = orbit (ConjAct (Perm α)) g

Tactic:
ext h
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g h : Perm α
⊢ Membership.mem (γ := Set (Perm α)) {h : Perm α | IsConj g h} h ↔ h ∈ orbit (ConjAct (Perm α)) g

Tactic:
simp only [Set.mem_setOf_eq, ConjAct.mem_orbit_conjAct, isConj_comm]

Premises used: Set.mem_setOf_eq, ConjAct.mem_orbit_conjAct, isConj_comm
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
h : (Fintype.card α)! = Fintype.card.{u_1} (Perm α)
h₁ h₂ : (Fintype.card α)! = (Fintype.card α)!
⊢ (Fintype.card α)! = Fintype.card.{u_1} (ConjAct (Perm α))

Tactic:
rw [ConjAct.card, Fintype.card_perm]

Premises used: Fintype.card_perm, ConjAct.card
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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
h₁ h₂ : (Fintype.card α)! = Fintype.card.{u_1} (ConjAct (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 α)!

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]

Premises used: Fintype.card_perm, ConjAct.card, Set.mem_setOf_eq, ConjAct.mem_orbit_conjAct, Subgroup.nat_card_centralizer_nat_card_stabilizer, Nat.card_eq_fintype_card, Equiv.Perm.nat_card_centralizer, isConj_comm
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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)!)
rw₁ :
  0 <
    (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)!)

Tactic:
rw [← card_isConj_mul_eq g, Nat.div_eq_of_eq_mul_left _]

Premises used: Nat.div_eq_of_eq_mul_left, Equiv.Perm.card_isConj_mul_eq
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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)!) =
    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:
rfl
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
rw : 0 < Nat.card.{u_1} ↥(centralizer {g})
⊢ 0 <
    (Fintype.card α - g.cycleType.sum)! * g.cycleType.prod * ∏ n ∈ g.cycleType.toFinset, (Multiset.count n g.cycleType)!

Tactic:
rw [← nat_card_centralizer g]

Premises used: Equiv.Perm.nat_card_centralizer
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
⊢ 0 < Nat.card.{u_1} ↥(centralizer {g})

Tactic:
apply Nat.card_pos

Premises used: Nat.card_pos
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
rw :
  (∀ ⦃x : Perm α⦄, Membership.mem (γ := Finset (Perm α)) Finset.univ x → ¬x.cycleType = m) ↔
    ∀ (x : Perm α), ¬x.cycleType = m
⊢ Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} = 0 ↔ ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)

Tactic:
rw [Finset.card_eq_zero, Finset.filter_eq_empty_iff,
    ← exists_with_cycleType_iff, not_exists]

Premises used: not_exists, Finset.filter_eq_empty_iff, Finset.card_eq_zero, Equiv.Perm.exists_with_cycleType_iff
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
⊢ (∀ ⦃x : Perm α⦄, Membership.mem (γ := Finset (Perm α)) Finset.univ x → ¬x.cycleType = m) ↔
    ∀ (x : Perm α), ¬x.cycleType = m

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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 α)!
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
⊢ 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

Tactic:
split_ifs with hm
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hm : m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
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 α)!
⊢ 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:
obtain ⟨g, rfl⟩ := (exists_with_cycleType_iff α).mpr hm

Premises used: Iff.mpr, Equiv.Perm.exists_with_cycleType_iff, rfl
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
hm : g.cycleType.sum ≤ Fintype.card α ∧ ∀ a ∈ g.cycleType, 2 ≤ a
⊢ 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 α)!

Tactic:
card_isConj_mul_eq g

Premises used: Equiv.Perm.card_isConj_mul_eq
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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} : Type u_1)
⊢ 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:
convert! card_isConj_mul_eq g

Premises used: Equiv.Perm.card_isConj_mul_eq
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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 }
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 }
h₄ :
  Fintype.card.{u_1} { x : Perm α // True ∧ x.cycleType = g.cycleType } =
    Fintype.card.{u_1} { h : Perm α // IsConj g h }
h₅ : Fintype.card.{u_1} { x : Perm α // x.cycleType = g.cycleType } = Fintype.card.{u_1} { h : Perm α // IsConj g h }
h₆ : Fintype.card.{u_1} { x : Perm α // IsConj x g } = 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)

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)]

Premises used: Finset.mem_univ, Equiv.Perm.isConj_iff_cycleType_eq, Finset.mem_filter, Set.coe_setOf, Fintype.card_coe, true_and, Nat.card_eq_fintype_card, isConj_comm
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hm : m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
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 α)!
h :
  ∀ (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)
⊢ 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:
classical
    obtain ⟨g, rfl⟩ := (exists_with_cycleType_iff α).mpr hm
    convert! card_isConj_mul_eq g
    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)]

Premises used: Iff.mpr, Finset.mem_univ, Equiv.Perm.isConj_iff_cycleType_eq, Finset.mem_filter, Set.coe_setOf, Equiv.Perm.exists_with_cycleType_iff, Fintype.card_coe, rfl, true_and, Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hm : ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)
neg : 0 * ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) = 0
neg₁ neg₂ : Eq (α := ℕ) 0 0
⊢ 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:
rw [(card_of_cycleType_eq_zero_iff α).mpr hm, zero_mul]

Premises used: Iff.mpr, MulZeroClass.zero_mul, Equiv.Perm.card_of_cycleType_eq_zero_iff
-- Module: Mathlib.GroupTheory.Perm.Centralizer
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 α)! / ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
neg :
  ∀ (hm : ¬(m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a)),
    Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} = 0
⊢ Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} =
    if m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a then
      (Fintype.card α)! / ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)
    else 0

Tactic:
split_ifs with hm
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
m : Multiset ℕ
hm : m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a
pos :
  (Fintype.card α)! / ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!) =
    Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m}
⊢ Finset.card.{u_1} (α := Perm α) {g : Perm α | g.cycleType = m} =
    (Fintype.card α)! / ((Fintype.card α - m.sum)! * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m)!)

Tactic:
apply symm

Premises used: symm