awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup.{u_1} p ↥P
H : Subgroup G
inst_1 : H.Normal
h_cop : (Nat.card.{u_1} ↥H).Coprime H.index
h1 : ¬Nat.card.{u_1} ↥H = 0
h2 : ¬H.index = 0
this : Finite G
h3 : (Nat.card.{u_1} ↥H).Coprime (Nat.card.{u_1} ↥P) ∨ H.index.Coprime (Nat.card.{u_1} ↥P)
h4 : H.index.Coprime (Nat.card.{u_1} ↥P)
⊢ H.relIndex P = 1

Tactic:
exact Nat.eq_one_of_dvd_coprimes h4 (H.relIndex_dvd_index_of_normal P)
      (Subgroup.relIndex_dvd_card H P)

Premises used: Subgroup.relIndex_dvd_index_of_normal, Nat.eq_one_of_dvd_coprimes, Subgroup.relIndex_dvd_card
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup.{u_1} p ↥P
H : Subgroup G
inst_1 : H.Normal
h_cop : (Nat.card.{u_1} ↥H).Coprime H.index
h1 : ¬Nat.card.{u_1} ↥H = 0
h2 : ¬H.index = 0
this : Finite G
h3 : (Nat.card.{u_1} ↥H).Coprime (Nat.card.{u_1} ↥P) ∨ H.index.Coprime (Nat.card.{u_1} ↥P)
h4 : (Nat.card.{u_1} ↥H).Coprime (Nat.card.{u_1} ↥P)
⊢ Disjoint H P

Tactic:
disjoint_iff.mpr (Subgroup.inf_eq_bot_of_coprime h4)

Premises used: Iff.mpr, disjoint_iff, Subgroup.inf_eq_bot_of_coprime
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup.{u_1} p ↥P
H : Subgroup G
inst_1 : H.Normal
h_cop : (Nat.card.{u_1} ↥H).Coprime H.index
h1 : ¬Nat.card.{u_1} ↥H = 0
h2 : ¬H.index = 0
this : Finite G
h3 : (Nat.card.{u_1} ↥H).Coprime (Nat.card.{u_1} ↥P) ∨ H.index.Coprime (Nat.card.{u_1} ↥P)
h4 : (Nat.card.{u_1} ↥H).Coprime (Nat.card.{u_1} ↥P)
⊢ Disjoint H P

Tactic:
exact disjoint_iff.mpr (Subgroup.inf_eq_bot_of_coprime h4)

Premises used: Iff.mpr, disjoint_iff, Subgroup.inf_eq_bot_of_coprime
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
n : ℕ
hGpn : Nat.card G = p ^ n
hn : 0 < n
⊢ Finite G

Tactic:
have : Finite G := Nat.finite_of_card_ne_zero (hGpn ▸ pow_ne_zero n (NeZero.ne p))
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
n : ℕ
hGpn : Nat.card G = p ^ n
hn : 0 < n
this : Finite G
⊢ IsPGroup.{u_1} p ↥(center G)

Tactic:
have hcG := to_subgroup (of_card hGpn) (center G)
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
n : ℕ
hGpn : Nat.card G = p ^ n
hn : 0 < n
this : Finite G
hcG : IsPGroup.{u_1} p ↥(center G)
⊢ ∃ (n : ℕ), Nat.card.{u_1} ↥(center G) = p ^ n

Tactic:
rcases iff_card.1 hcG with _

Premises used: IsPGroup.iff_card, Iff.mp
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
n : ℕ
hGpn : Nat.card G = p ^ n
hn : 0 < n
this : Finite G
hcG : IsPGroup.{u_1} p ↥(center G)
h : ∃ (n : ℕ), Nat.card.{u_1} ↥(center G) = p ^ n
⊢ Nontrivial G

Tactic:
haveI : Nontrivial G := (nontrivial_iff_card <| of_card hGpn).2 ⟨n, hn, hGpn⟩
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
n : ℕ
hGpn : Nat.card G = p ^ n
hn : 0 < n
this_1 : Finite G
hcG : IsPGroup.{u_1} p ↥(center G)
h : ∃ (n : ℕ), Nat.card.{u_1} ↥(center G) = p ^ n
this : Nontrivial G
⊢ ∃ k > 0, Nat.card.{u_1} ↥(center G) = p ^ k

Tactic:
(nontrivial_iff_card hcG).mp (center_nontrivial (of_card hGpn))

Premises used: IsPGroup.center_nontrivial, IsPGroup.nontrivial_iff_card, Iff.mp, IsPGroup.of_card
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
n : ℕ
hGpn : Nat.card G = p ^ n
hn : 0 < n
this_1 : Finite G
hcG : IsPGroup.{u_1} p ↥(center G)
h : ∃ (n : ℕ), Nat.card.{u_1} ↥(center G) = p ^ n
this : Nontrivial G
⊢ ∃ k > 0, Nat.card.{u_1} ↥(center G) = p ^ k

Tactic:
exact (nontrivial_iff_card hcG).mp (center_nontrivial (of_card hGpn))

Premises used: IsPGroup.center_nontrivial, IsPGroup.nontrivial_iff_card, Iff.mp, IsPGroup.of_card
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
hG : Nat.card G = HPow.hPow (β := ℕ) p 2
apply : Nat.card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) ∣ p
⊢ IsCyclic.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G))

Tactic:
apply isCyclic_of_card_dvd_prime (p := p)

Premises used: isCyclic_of_card_dvd_prime
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
hG : Nat.card G = HPow.hPow (β := ℕ) p 2
rw :
  p * Nat.card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) ∣
    Nat.card.{u_1} ↥(center G) * Subgroup.index (center G)
⊢ Nat.card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) ∣ p

Tactic:
rw [← mul_dvd_mul_iff_left (NeZero.ne p), ← sq, ← hG, ← (center G).card_mul_index]

Premises used: Subgroup.center, sq, mul_dvd_mul_iff_left, Subgroup.card_mul_index, NeZero.ne
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
hG : Nat.card G = HPow.hPow (β := ℕ) p 2
h : p ∣ Nat.card.{u_1} ↥(center G)
⊢ p * Nat.card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (center G)) ∣
    Nat.card.{u_1} ↥(center G) * Subgroup.index (center G)

Tactic:
apply mul_dvd_mul_right

Premises used: mul_dvd_mul_right
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
hG : Nat.card G = HPow.hPow (β := ℕ) p 2
h : ∀ (k : ℕ) (hk0 : k > 0) (hk : Nat.card.{u_1} ↥(center G) = p ^ k), p ∣ Nat.card.{u_1} ↥(center G)
⊢ p ∣ Nat.card.{u_1} ↥(center G)

Tactic:
rcases card_center_eq_prime_pow hG zero_lt_two with ⟨k, hk0, hk⟩

Premises used: IsPGroup.card_center_eq_prime_pow, zero_lt_two
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
hG : Nat.card G = HPow.hPow (β := ℕ) p 2
k : ℕ
hk0 : k > 0
hk : Nat.card.{u_1} ↥(center G) = p ^ k
h : p ∣ p ^ k
⊢ p ∣ Nat.card.{u_1} ↥(center G)

Tactic:
rw [hk]
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
hG : Nat.card G = HPow.hPow (β := ℕ) p 2
k : ℕ
hk0 : k > 0
hk : Nat.card.{u_1} ↥(center G) = p ^ k
⊢ p ∣ p ^ k

Tactic:
dvd_pow_self p hk0.ne'

Premises used: dvd_pow_self, LT.lt.ne'
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
hG : Nat.card G = HPow.hPow (β := ℕ) p 2
k : ℕ
hk0 : k > 0
hk : Nat.card.{u_1} ↥(center G) = p ^ k
⊢ p ∣ p ^ k

Tactic:
exact dvd_pow_self p hk0.ne'

Premises used: dvd_pow_self, LT.lt.ne'
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
hG : Nat.card G = HPow.hPow (β := ℕ) p 2
⊢ ∀ (a b : G), a * b = b * a

Tactic:
(commGroupOfCardEqPrimeSq hG).mul_comm

Premises used: CommGroup.mul_comm
-- Module: Mathlib.GroupTheory.PGroup
Goal:
n : ℕ
G : Type u_2
inst : AddCommGroup G
inst_1 : Module (ZMod n) G
x : G
⊢ HPow.hPow (α := Multiplicative G) ((Multiplicative.ofAdd : (a : G) → Multiplicative G) x : Multiplicative G)
      (HPow.hPow (β := ℕ) n 1) =
    1

Tactic:
simp [← ofAdd_nsmul, ZModModule.char_nsmul_eq_zero]

Premises used: ZModModule.char_nsmul_eq_zero, ofAdd_nsmul
-- Module: Mathlib.GroupTheory.PGroup
Goal:
n : ℕ
G : Type u_2
inst : AddCommGroup G
inst_1 : Module (ZMod n) G
⊢ IsPGroup.{u_2} n (Multiplicative G)

Tactic:
simpa [IsPGroup, Multiplicative.forall] using
    fun _ ↦ ⟨1, by simp [← ofAdd_nsmul, ZModModule.char_nsmul_eq_zero]⟩

Premises used: IsPGroup, Multiplicative.forall
-- Module: Mathlib.GroupTheory.Perm.Basic
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : MulAction.{u, v} (Perm α) β
i j : α
x : β
⊢ swap i j • swap i j • x = x

Tactic:
simp [smul_smul]

Premises used: smul_smul
-- Module: Mathlib.GroupTheory.Perm.Basic
Goal:
α : Type u
β : Type v
inst : DecidableEq α
inst_1 : MulAction.{u, v} (Perm α) β
i j : α
⊢ Function.Involutive fun (x : β) ↦ swap i j • x

Tactic:
swap_smul_self_smul i j

Premises used: Function.Involutive, Equiv.swap_smul_self_smul
-- Module: Mathlib.GroupTheory.Perm.Basic
Goal:
α : Type u_1
f : Perm α
s : Set α
hf : BijOn (⇑f : (a : α) → α) s s
⊢ BijOn (⇑f⁻¹ : (a : α) → α) s s

Tactic:
hf.symm f.invOn

Premises used: Equiv.invOn, Set.BijOn.symm
-- Module: Mathlib.GroupTheory.Perm.Basic
Goal:
α : Type u_1
f : Perm α
s : Set α
simp_rw : MapsTo (⇑f : (a : α) → α) s s → ∀ (n : ℕ), MapsTo (⇑f : (a : α) → α)^[n] s s
⊢ MapsTo (⇑f : (a : α) → α) s s → ∀ (n : ℕ), MapsTo (⇑(f ^ n) : (a : α) → α) s s

Tactic:
simp_rw [Equiv.Perm.coe_pow]

Premises used: Equiv.Perm.coe_pow
-- Module: Mathlib.GroupTheory.Perm.Basic
Goal:
α : Type u_1
f : Perm α
s : Set α
⊢ MapsTo (⇑f : (a : α) → α) s s → ∀ (n : ℕ), MapsTo (⇑f : (a : α) → α)^[n] s s

Tactic:
MapsTo.iterate

Premises used: Set.MapsTo.iterate
-- Module: Mathlib.GroupTheory.Perm.Basic
Goal:
α : Type u_1
f : Perm α
s : Set α
⊢ MapsTo (⇑f : (a : α) → α) s s → ∀ (n : ℕ), MapsTo (⇑f : (a : α) → α)^[n] s s

Tactic:
exact MapsTo.iterate

Premises used: Set.MapsTo.iterate
-- Module: Mathlib.GroupTheory.Perm.Basic
Goal:
α : Type u_1
f : Perm α
s : Set α
simp_rw : SurjOn (⇑f : (a : α) → α) s s → ∀ (n : ℕ), SurjOn (⇑f : (a : α) → α)^[n] s s
⊢ SurjOn (⇑f : (a : α) → α) s s → ∀ (n : ℕ), SurjOn (⇑(f ^ n) : (a : α) → α) s s

Tactic:
simp_rw [Equiv.Perm.coe_pow]

Premises used: Equiv.Perm.coe_pow
-- Module: Mathlib.GroupTheory.Perm.Basic
Goal:
α : Type u_1
f : Perm α
s : Set α
⊢ SurjOn (⇑f : (a : α) → α) s s → ∀ (n : ℕ), SurjOn (⇑f : (a : α) → α)^[n] s s

Tactic:
SurjOn.iterate

Premises used: Set.SurjOn.iterate
-- Module: Mathlib.GroupTheory.Perm.Basic
Goal:
α : Type u_1
f : Perm α
s : Set α
⊢ SurjOn (⇑f : (a : α) → α) s s → ∀ (n : ℕ), SurjOn (⇑f : (a : α) → α)^[n] s s

Tactic:
exact SurjOn.iterate

Premises used: Set.SurjOn.iterate
-- Module: Mathlib.GroupTheory.Perm.Basic
Goal:
α : Type u_1
f : Perm α
s : Set α
simp_rw : BijOn (⇑f : (a : α) → α) s s → ∀ (n : ℕ), BijOn (⇑f : (a : α) → α)^[n] s s
⊢ BijOn (⇑f : (a : α) → α) s s → ∀ (n : ℕ), BijOn (⇑(f ^ n) : (a : α) → α) s s

Tactic:
simp_rw [Equiv.Perm.coe_pow]

Premises used: Equiv.Perm.coe_pow
-- Module: Mathlib.GroupTheory.Perm.Basic
Goal:
α : Type u_1
f : Perm α
s : Set α
⊢ BijOn (⇑f : (a : α) → α) s s → ∀ (n : ℕ), BijOn (⇑f : (a : α) → α)^[n] s s

Tactic:
BijOn.iterate

Premises used: Set.BijOn.iterate
-- Module: Mathlib.GroupTheory.Perm.Basic
Goal:
α : Type u_1
f : Perm α
s : Set α
⊢ BijOn (⇑f : (a : α) → α) s s → ∀ (n : ℕ), BijOn (⇑f : (a : α) → α)^[n] s s

Tactic:
exact BijOn.iterate

Premises used: Set.BijOn.iterate
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g k c : Perm α
k_mem : Membership.mem (γ := Subgroup (Perm α)) (centralizer {g}) k
c_mem : c ∈ g.cycleFactorsFinset
this :
  (↑g.cycleFactorsFinset : Set (Perm α)) =
    HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
      (↑g.cycleFactorsFinset : Set (Perm α))
rw :
  HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α)) c ∈
    HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
      (↑g.cycleFactorsFinset : Set (Perm α))
⊢ HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α)) c ∈
    g.cycleFactorsFinset

Tactic:
rw [← Finset.mem_coe, this]

Premises used: Finset.mem_coe
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g k c : Perm α
k_mem : Membership.mem (γ := Subgroup (Perm α)) (centralizer {g}) k
c_mem : c ∈ g.cycleFactorsFinset
this :
  (↑g.cycleFactorsFinset : Set (Perm α)) =
    HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
      (↑g.cycleFactorsFinset : Set (Perm α))
⊢ HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α)) c ∈
    HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
      (↑g.cycleFactorsFinset : Set (Perm α))

Tactic:
simp only [Set.smul_mem_smul_set_iff, Finset.mem_coe, c_mem]

Premises used: Set.smul_mem_smul_set_iff, Finset.mem_coe
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g k c : Perm α
k_mem : Membership.mem (γ := Subgroup (Perm α)) (centralizer {g}) k
c_mem : c ∈ g.cycleFactorsFinset
suffices :
  (↑g.cycleFactorsFinset : Set (Perm α)) =
    HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
      (↑g.cycleFactorsFinset : Set (Perm α))
⊢ HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α)) c ∈
    g.cycleFactorsFinset

Tactic:
suffices (g.cycleFactorsFinset : Set (Perm α)) =
    (ConjAct.toConjAct k) • g.cycleFactorsFinset by
    rw [← Finset.mem_coe, this]
    simp only [Set.smul_mem_smul_set_iff, Finset.mem_coe, c_mem]
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g k c : Perm α
k_mem : Membership.mem (γ := Subgroup (Perm α)) (centralizer {g}) k
c_mem : c ∈ g.cycleFactorsFinset
⊢ (HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
        g).cycleFactorsFinset =
    HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
      g.cycleFactorsFinset

Tactic:
have this := cycleFactorsFinset_conj_eq (ConjAct.toConjAct (k : Perm α)) g
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g k c : Perm α
k_mem : Membership.mem (γ := Subgroup (Perm α)) (centralizer {g}) k
c_mem : c ∈ g.cycleFactorsFinset
this :
  (HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
        g).cycleFactorsFinset =
    HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
      g.cycleFactorsFinset
⊢ (g * (k * k⁻¹)).cycleFactorsFinset =
    HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
      g.cycleFactorsFinset

Tactic:
rw [ConjAct.toConjAct_smul, mem_centralizer_singleton_iff.mp k_mem, mul_assoc] at this

Premises used: mul_assoc, Subgroup.mem_centralizer_singleton_iff, ConjAct.toConjAct_smul, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g k c : Perm α
k_mem : Membership.mem (γ := Subgroup (Perm α)) (centralizer {g}) k
c_mem : c ∈ g.cycleFactorsFinset
this :
  (g * (k * k⁻¹)).cycleFactorsFinset =
    HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
      g.cycleFactorsFinset
⊢ g.cycleFactorsFinset =
    HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
      g.cycleFactorsFinset

Tactic:
simp only [mul_inv_cancel, mul_one] at this

Premises used: mul_inv_cancel, mul_one
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g k c : Perm α
k_mem : Membership.mem (γ := Subgroup (Perm α)) (centralizer {g}) k
c_mem : c ∈ g.cycleFactorsFinset
this :
  g.cycleFactorsFinset =
    HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
      g.cycleFactorsFinset
rw :
  (↑(HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
        g.cycleFactorsFinset) :
    Set (Perm α))
| (↑g.cycleFactorsFinset : Set (Perm α))

Tactic:
rw [this]
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g k c : Perm α
k_mem : Membership.mem (γ := Subgroup (Perm α)) (centralizer {g}) k
c_mem : c ∈ g.cycleFactorsFinset
this :
  g.cycleFactorsFinset =
    HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
      g.cycleFactorsFinset
conv_lhs :
  (↑(HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
          g.cycleFactorsFinset) :
      Set (Perm α)) =
    HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
      (↑g.cycleFactorsFinset : Set (Perm α))
⊢ (↑g.cycleFactorsFinset : Set (Perm α)) =
    HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
      (↑g.cycleFactorsFinset : Set (Perm α))

Tactic:
conv_lhs => rw [this]
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g k c : Perm α
k_mem : Membership.mem (γ := Subgroup (Perm α)) (centralizer {g}) k
c_mem : c ∈ g.cycleFactorsFinset
this :
  g.cycleFactorsFinset =
    HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
      g.cycleFactorsFinset
⊢ (↑(HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
          g.cycleFactorsFinset) :
      Set (Perm α)) =
    HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) k : ConjAct (Perm α))
      (↑g.cycleFactorsFinset : Set (Perm α))

Tactic:
simp only [Finset.coe_smul_finset]

Premises used: Finset.coe_smul_finset
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
k l : ↥(centralizer {g})
c : ↥g.cycleFactorsFinset
simp : (↑((k * l) • c) : Perm α) = (↑(k • l • c) : Perm α)
⊢ (k * l) • c = k • l • c

Tactic:
simp only [← Subtype.coe_inj]

Premises used: Subtype.coe_inj
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
k l : ↥(centralizer {g})
c : ↥g.cycleFactorsFinset
⊢ HSMul.hSMul (α := ConjAct (Perm α))
      ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) ((↑k : Perm α) * (↑l : Perm α)) : ConjAct (Perm α))
      (↑c : Perm α) =
    HSMul.hSMul (α := ConjAct (Perm α))
      ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) (↑k : Perm α) : ConjAct (Perm α))
      (HSMul.hSMul (α := ConjAct (Perm α))
        ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) (↑l : Perm α) : ConjAct (Perm α)) (↑c : Perm α))

Tactic:
simp only [map_mul, mul_smul]

Premises used: map_mul, SemigroupAction.mul_smul
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
c : ↥g.cycleFactorsFinset
rw : (↑(HSMul.hSMul (α := ↥(centralizer {g})) 1 c) : Perm α) = (↑c : Perm α)
⊢ HSMul.hSMul (α := ↥(centralizer {g})) 1 c = c

Tactic:
rw [← Subtype.coe_inj]

Premises used: Subtype.coe_inj
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
c : ↥g.cycleFactorsFinset
⊢ HSMul.hSMul (α := ConjAct (Perm α)) ((ConjAct.toConjAct : (a : Perm α) → ConjAct (Perm α)) 1 : ConjAct (Perm α))
      (↑c : Perm α) =
    (↑c : Perm α)

Tactic:
simp only [map_one, one_smul]

Premises used: one_smul, map_one
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
k : ↥(centralizer {g})
c : ↥g.cycleFactorsFinset
⊢ k • c =
    Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) ((↑k : Perm α) * (↑c : Perm α) * (↑k⁻¹ : Perm α)) ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
k : ↥(centralizer {g})
c : ↥g.cycleFactorsFinset
⊢ (↑(k • c) : Perm α) = (↑k : Perm α) * (↑c : Perm α) * (↑k⁻¹ : Perm α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
k : ↥(centralizer {g})
c : ↥g.cycleFactorsFinset
⊢ (((toPermHom g : (a : ↥(centralizer {g})) → Perm ↥g.cycleFactorsFinset) k : Perm ↥g.cycleFactorsFinset) :
        (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
      c =
    k • c

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
k : ↥(centralizer {g})
c : ↥g.cycleFactorsFinset
⊢ (↑((((toPermHom g : (a : ↥(centralizer {g})) → Perm ↥g.cycleFactorsFinset) k : Perm ↥g.cycleFactorsFinset) :
            (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
          c) :
      Perm α) =
    (↑k : Perm α) * (↑c : Perm α) * (↑k : Perm α)⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a b : Perm ↥g.cycleFactorsFinset
hσ :
  Membership.mem (γ := Set (Perm ↥g.cycleFactorsFinset))
    {τ : Perm ↥g.cycleFactorsFinset |
      ∀ (c : ↥g.cycleFactorsFinset),
        Finset.card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)) =
          #(↑c : Perm α).support}
    a
hτ :
  Membership.mem (γ := Set (Perm ↥g.cycleFactorsFinset))
    {τ : Perm ↥g.cycleFactorsFinset |
      ∀ (c : ↥g.cycleFactorsFinset),
        Finset.card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)) =
          #(↑c : Perm α).support}
    b
simp :
  ∀ (a_1 : Perm α) (b_1 : a_1 ∈ g.cycleFactorsFinset),
    Finset.card.{u_1} (α := α)
        (support
          (↑((a : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
                ((b : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
                  (Subtype.mk (p := fun (a : Perm α) ↦ a ∈ g.cycleFactorsFinset) a_1 b_1))) :
            Perm α)) =
      #a_1.support
⊢ Membership.mem (γ := Set (Perm ↥g.cycleFactorsFinset))
    {τ : Perm ↥g.cycleFactorsFinset |
      ∀ (c : ↥g.cycleFactorsFinset),
        Finset.card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)) =
          #(↑c : Perm α).support}
    (a * b)

Tactic:
simp only [Subtype.forall, Set.mem_setOf_eq, coe_mul, Function.comp_apply]

Premises used: Equiv.Perm.coe_mul, Subtype.forall, Set.mem_setOf_eq, Function.comp_apply
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a b : Perm ↥g.cycleFactorsFinset
hσ :
  Membership.mem (γ := Set (Perm ↥g.cycleFactorsFinset))
    {τ : Perm ↥g.cycleFactorsFinset |
      ∀ (c : ↥g.cycleFactorsFinset),
        Finset.card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)) =
          #(↑c : Perm α).support}
    a
hτ :
  Membership.mem (γ := Set (Perm ↥g.cycleFactorsFinset))
    {τ : Perm ↥g.cycleFactorsFinset |
      ∀ (c : ↥g.cycleFactorsFinset),
        Finset.card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)) =
          #(↑c : Perm α).support}
    b
⊢ ∀ (a_1 : Perm α) (b : a_1 ∈ g.cycleFactorsFinset),
    Finset.card.{u_1} (α := α)
        (support
          (↑((a : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
                (Subtype.mk (p := fun (a : Perm α) ↦ a ∈ g.cycleFactorsFinset) a_1 b)) :
            Perm α)) =
      #a_1.support

Tactic:
simp only [Subtype.forall, Set.mem_setOf_eq] at hσ hτ

Premises used: Subtype.forall, Set.mem_setOf_eq