awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
rw :
  (↑(↑τ : Perm ↥g.cycleFactorsFinset).support : Set ↥g.cycleFactorsFinset).PairwiseDisjoint (α := Finset α)
    fun (c : ↥g.cycleFactorsFinset) ↦ (↑c : Perm α).support
⊢ Finset.card.{u_1} (α := α) (support ((a.ofPermHom : (a : ↥(range_toPermHom' g)) → Perm α) τ)) =
    ∑ c ∈ (↑τ : Perm ↥g.cycleFactorsFinset).support, #(↑c : Perm α).support

Tactic:
rw [ofPermHom_support, Finset.card_biUnion]

Premises used: Finset.card_biUnion, Equiv.Perm.Basis.ofPermHom_support
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
c : ↥g.cycleFactorsFinset
_ :
  c ∈ (↑(↑τ : Perm ↥g.cycleFactorsFinset).support : Set ↥g.cycleFactorsFinset) →
    ∀ ⦃y : ↥g.cycleFactorsFinset⦄,
      y ∈ (↑(↑τ : Perm ↥g.cycleFactorsFinset).support : Set ↥g.cycleFactorsFinset) →
        c ≠ y →
          Function.onFun (β := Finset α) _root_.Disjoint (fun (c : ↥g.cycleFactorsFinset) ↦ (↑c : Perm α).support) c y
⊢ c ∈ (↑(↑τ : Perm ↥g.cycleFactorsFinset).support : Set ↥g.cycleFactorsFinset) →
    ∀ ⦃y : ↥g.cycleFactorsFinset⦄,
      y ∈ (↑(↑τ : Perm ↥g.cycleFactorsFinset).support : Set ↥g.cycleFactorsFinset) →
        c ≠ y →
          Function.onFun (β := Finset α) _root_.Disjoint (fun (c : ↥g.cycleFactorsFinset) ↦ (↑c : Perm α).support) c y

Tactic:
_
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
c : ↥g.cycleFactorsFinset
h : c ∈ (↑(↑τ : Perm ↥g.cycleFactorsFinset).support : Set ↥g.cycleFactorsFinset)
d : ↥g.cycleFactorsFinset
_ :
  d ∈ (↑(↑τ : Perm ↥g.cycleFactorsFinset).support : Set ↥g.cycleFactorsFinset) →
    c ≠ d → Function.onFun (β := Finset α) _root_.Disjoint (fun (c : ↥g.cycleFactorsFinset) ↦ (↑c : Perm α).support) c d
⊢ d ∈ (↑(↑τ : Perm ↥g.cycleFactorsFinset).support : Set ↥g.cycleFactorsFinset) →
    c ≠ d → Function.onFun (β := Finset α) _root_.Disjoint (fun (c : ↥g.cycleFactorsFinset) ↦ (↑c : Perm α).support) c d

Tactic:
_
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
c : ↥g.cycleFactorsFinset
h_1 : c ∈ (↑(↑τ : Perm ↥g.cycleFactorsFinset).support : Set ↥g.cycleFactorsFinset)
d : ↥g.cycleFactorsFinset
h_2 : d ∈ (↑(↑τ : Perm ↥g.cycleFactorsFinset).support : Set ↥g.cycleFactorsFinset)
h : c ≠ d
h₁ : (↑c : Perm α).Disjoint (↑d : Perm α)
⊢ Function.onFun (β := Finset α) _root_.Disjoint (fun (c : ↥g.cycleFactorsFinset) ↦ (↑c : Perm α).support) c d

Tactic:
apply Equiv.Perm.Disjoint.disjoint_support

Premises used: Equiv.Perm.Disjoint.disjoint_support
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
c : ↥g.cycleFactorsFinset
h_1 : c ∈ (↑(↑τ : Perm ↥g.cycleFactorsFinset).support : Set ↥g.cycleFactorsFinset)
d : ↥g.cycleFactorsFinset
h_2 : d ∈ (↑(↑τ : Perm ↥g.cycleFactorsFinset).support : Set ↥g.cycleFactorsFinset)
h : c ≠ d
⊢ (↑c : Perm α).Disjoint (↑d : Perm α)

Tactic:
apply g.cycleFactorsFinset_pairwise_disjoint c.prop d.prop (Subtype.coe_ne_coe.mpr h)

Premises used: Iff.mpr, Equiv.Perm.cycleFactorsFinset_pairwise_disjoint, Subtype.prop, Subtype.coe_ne_coe
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
rw :
  HMul.hMul (α := Perm α) ((a.ofPermHom : (a : ↥(range_toPermHom' g)) → Perm α) τ : Perm α) g =
    HMul.hMul (β := Perm α) g ((a.ofPermHom : (a : ↥(range_toPermHom' g)) → Perm α) τ : Perm α)
⊢ Membership.mem (α := Perm α) (γ := Subgroup (Perm α)) (centralizer {g})
    ((a.ofPermHom : (a : ↥(range_toPermHom' g)) → Perm α) τ : Perm α)

Tactic:
rw [mem_centralizer_singleton_iff]

Premises used: Subgroup.mem_centralizer_singleton_iff
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
H :
  ∀ (x : α),
    Eq (α := α)
      ((HMul.hMul (α := Perm α) ((a.ofPermHom : (a : ↥(range_toPermHom' g)) → Perm α) τ : Perm α) g : (a : α) → α) x :
        α)
      ((HMul.hMul (β := Perm α) g ((a.ofPermHom : (a : ↥(range_toPermHom' g)) → Perm α) τ : Perm α) : (a : α) → α) x :
        α)
⊢ HMul.hMul (α := Perm α) ((a.ofPermHom : (a : ↥(range_toPermHom' g)) → Perm α) τ : Perm α) g =
    HMul.hMul (β := Perm α) g ((a.ofPermHom : (a : ↥(range_toPermHom' g)) → Perm α) τ : Perm α)

Tactic:
ext x
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
H :
  Eq (α := α)
    ((((a.ofPermHom : (a : ↥(range_toPermHom' g)) → Perm α) τ : Perm α) : (a : α) → α) ((g : (a : α) → α) x : α) : α)
    ((g : (a : α) → α) ((((a.ofPermHom : (a : ↥(range_toPermHom' g)) → Perm α) τ : Perm α) : (a : α) → α) x : α) : α)
⊢ Eq (α := α)
    ((HMul.hMul (α := Perm α) ((a.ofPermHom : (a : ↥(range_toPermHom' g)) → Perm α) τ : Perm α) g : (a : α) → α) x : α)
    ((HMul.hMul (β := Perm α) g ((a.ofPermHom : (a : ↥(range_toPermHom' g)) → Perm α) τ : Perm α) : (a : α) → α) x : α)

Tactic:
simp only [mul_apply]

Premises used: Equiv.Perm.mul_apply
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
⊢ Eq (α := α)
    ((((a.ofPermHom : (a : ↥(range_toPermHom' g)) → Perm α) τ : Perm α) : (a : α) → α) ((g : (a : α) → α) x : α) : α)
    ((g : (a : α) → α) ((((a.ofPermHom : (a : ↥(range_toPermHom' g)) → Perm α) τ : Perm α) : (a : α) → α) x : α) : α)

Tactic:
ofPermHomFun_commute_zpow_apply a τ x 1

Premises used: Set.Mem, setOf, Nat.iterate, dite, Equiv.Perm.Basis.ofPermHomFun_commute_zpow_apply, Equiv.Perm.Basis.ofPermHomFun, OfNat.ofNat
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
⊢ Eq (α := α)
    ((((a.ofPermHom : (a : ↥(range_toPermHom' g)) → Perm α) τ : Perm α) : (a : α) → α) ((g : (a : α) → α) x : α) : α)
    ((g : (a : α) → α) ((((a.ofPermHom : (a : ↥(range_toPermHom' g)) → Perm α) τ : Perm α) : (a : α) → α) x : α) : α)

Tactic:
exact ofPermHomFun_commute_zpow_apply a τ x 1

Premises used: Equiv.Perm.Basis.ofPermHomFun_commute_zpow_apply, OfNat.ofNat
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
⊢ Eq (α := ↥(centralizer {g}))
    (Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (centralizer {g}) x)
        ((a.ofPermHom : (a : ↥(range_toPermHom' g)) → Perm α) 1) ⋯ :
      ↥(centralizer {g}))
    (1 : ↥(centralizer {g}))

Tactic:
simp only [map_one, mk_eq_one]

Premises used: map_one, Subgroup.mk_eq_one
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ_1 σ τ : ↥(range_toPermHom' g)
⊢ Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (centralizer {g}) x)
      ((a.ofPermHom : (a : ↥(range_toPermHom' g)) → Perm α) (σ * τ)) ⋯ =
    HMul.hMul (α := ↥(centralizer {g})) (β := ↥(centralizer {g}))
      (Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (centralizer {g}) x)
          ((a.ofPermHom : (a : ↥(range_toPermHom' g)) → Perm α) σ) ⋯ :
        ↥(centralizer {g}))
      (Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (centralizer {g}) x)
          ((a.ofPermHom : (a : ↥(range_toPermHom' g)) → Perm α) τ) ⋯ :
        ↥(centralizer {g}))

Tactic:
simp only [map_mul, MulMemClass.mk_mul_mk]

Premises used: map_mul, MulMemClass.mk_mul_mk
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
⊢ ((↑((a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(centralizer {g})) τ) : Perm α) : (a : α) → α) x =
    a.ofPermHomFun τ x

Tactic:
rfl

Premises used: dite, Equiv.Perm.Basis.ofPermHomFun, rfl
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
simp :
  (↑((a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(centralizer {g})) τ) : Perm α) * (↑c : Perm α) =
    HMul.hMul (α := Perm α)
      (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)
      (↑((a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(centralizer {g})) τ) : Perm α)
⊢ HSMul.hSMul (α := ↥(centralizer {g}))
      ((a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(centralizer {g})) τ : ↥(centralizer {g})) c =
    ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c

Tactic:
simp only [← Subtype.coe_inj, val_centralizer_smul, InvMemClass.coe_inv, mul_inv_eq_iff_eq_mul]

Premises used: Subtype.coe_inj, Equiv.Perm.OnCycleFactors.val_centralizer_smul, InvMemClass.coe_inv, mul_inv_eq_iff_eq_mul
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
H :
  ∀ (x : α),
    Eq (α := α)
      (((↑((a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(centralizer {g})) τ) : Perm α) * (↑c : Perm α) :
            (a : α) → α)
          x :
        α)
      ((HMul.hMul (α := Perm α)
              (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)
              (↑((a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(centralizer {g})) τ) : Perm α) :
            (a : α) → α)
          x :
        α)
⊢ (↑((a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(centralizer {g})) τ) : Perm α) * (↑c : Perm α) =
    HMul.hMul (α := Perm α)
      (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)
      (↑((a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(centralizer {g})) τ) : Perm α)

Tactic:
ext x
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
x : α
H :
  a.ofPermHomFun τ (((↑c : Perm α) : (a : α) → α) x) =
    ((↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α) :
        (a : α) → α)
      (a.ofPermHomFun τ x)
⊢ Eq (α := α)
    (((↑((a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(centralizer {g})) τ) : Perm α) * (↑c : Perm α) :
          (a : α) → α)
        x :
      α)
    ((HMul.hMul (α := Perm α)
            (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)
            (↑((a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(centralizer {g})) τ) : Perm α) :
          (a : α) → α)
        x :
      α)

Tactic:
simp only [mul_apply, toCentralizer_apply]

Premises used: Equiv.Perm.Basis.toCentralizer_apply, Equiv.Perm.mul_apply
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
x : α
pos :
  ∀ (hx : x ∈ (↑c : Perm α).support),
    a.ofPermHomFun τ (((↑c : Perm α) : (a : α) → α) x) =
      ((↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α) :
          (a : α) → α)
        (a.ofPermHomFun τ x)
neg :
  ∀ (hx : x ∉ (↑c : Perm α).support),
    a.ofPermHomFun τ (((↑c : Perm α) : (a : α) → α) x) =
      ((↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α) :
          (a : α) → α)
        (a.ofPermHomFun τ x)
⊢ a.ofPermHomFun τ (((↑c : Perm α) : (a : α) → α) x) =
    ((↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α) :
        (a : α) → α)
      (a.ofPermHomFun τ x)

Tactic:
by_cases hx : x ∈ c.val.support

Premises used: Equiv.Perm.support, Subtype.val
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ (↑c : Perm α).support
pos :
  a.ofPermHomFun τ ((g : (a : α) → α) x) =
    ((↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α) :
        (a : α) → α)
      (a.ofPermHomFun τ x)
⊢ a.ofPermHomFun τ (((↑c : Perm α) : (a : α) → α) x) =
    ((↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α) :
        (a : α) → α)
      (a.ofPermHomFun τ x)

Tactic:
rw [(mem_cycleFactorsFinset_iff.mp c.prop).2 x hx]

Premises used: And.right, Subtype.prop, Equiv.Perm.mem_cycleFactorsFinset_iff, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ (↑c : Perm α).support
⊢ a.ofPermHomFun τ ((HPow.hPow (β := ℤ) g 1 : (a : α) → α) x) =
    (HPow.hPow (β := ℤ) g 1 : (a : α) → α) (a.ofPermHomFun τ x)

Tactic:
have := ofPermHomFun_commute_zpow_apply a τ x 1
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ (↑c : Perm α).support
this :
  a.ofPermHomFun τ ((HPow.hPow (β := ℤ) g 1 : (a : α) → α) x) =
    (HPow.hPow (β := ℤ) g 1 : (a : α) → α) (a.ofPermHomFun τ x)
⊢ a.ofPermHomFun τ ((g : (a : α) → α) x) = (g : (a : α) → α) (a.ofPermHomFun τ x)

Tactic:
simp only [zpow_one] at this

Premises used: zpow_one
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ (↑c : Perm α).support
this : a.ofPermHomFun τ ((g : (a : α) → α) x) = (g : (a : α) → α) (a.ofPermHomFun τ x)
pos :
  Membership.mem (γ := Finset α)
    (support (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α))
    (a.ofPermHomFun τ x)
⊢ a.ofPermHomFun τ ((g : (a : α) → α) x) =
    ((↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α) :
        (a : α) → α)
      (a.ofPermHomFun τ x)

Tactic:
rw [this, ← (mem_cycleFactorsFinset_iff.mp ((τ : Perm g.cycleFactorsFinset) c).prop).2]

Premises used: And.right, Subtype.prop, Equiv.Perm.mem_cycleFactorsFinset_iff, Iff.mp, Subtype.val, DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ (↑c : Perm α).support
this : a.ofPermHomFun τ ((g : (a : α) → α) x) = (g : (a : α) → α) (a.ofPermHomFun τ x)
pos : x ∈ (↑c : Perm α).support
⊢ Membership.mem (γ := Finset α)
    (support (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α))
    (a.ofPermHomFun τ x)

Tactic:
rw [ofPermHomFun_apply_mem_support_cycle_iff]

Premises used: Equiv.Perm.Basis.ofPermHomFun_apply_mem_support_cycle_iff
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ (↑c : Perm α).support
this : a.ofPermHomFun τ ((g : (a : α) → α) x) = (g : (a : α) → α) (a.ofPermHomFun τ x)
⊢ x ∈ (↑c : Perm α).support

Tactic:
hx
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
x : α
hx : x ∈ (↑c : Perm α).support
this : a.ofPermHomFun τ ((g : (a : α) → α) x) = (g : (a : α) → α) (a.ofPermHomFun τ x)
⊢ x ∈ (↑c : Perm α).support

Tactic:
exact hx
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
x : α
hx neg : x ∉ (↑c : Perm α).support
⊢ a.ofPermHomFun τ (((↑c : Perm α) : (a : α) → α) x) =
    ((↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α) :
        (a : α) → α)
      (a.ofPermHomFun τ x)

Tactic:
rw [notMem_support.mp hx, eq_comm, ← notMem_support,
      ofPermHomFun_apply_mem_support_cycle_iff]

Premises used: Equiv.Perm.notMem_support, eq_comm, Equiv.Perm.Basis.ofPermHomFun_apply_mem_support_cycle_iff, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
x : α
hx : x ∉ (↑c : Perm α).support
⊢ x ∉ (↑c : Perm α).support

Tactic:
hx
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
τ : ↥(range_toPermHom' g)
x : α
hx : x ∉ (↑c : Perm α).support
⊢ x ∉ (↑c : Perm α).support

Tactic:
exact hx
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
H :
  ∀ (x : ↥g.cycleFactorsFinset),
    Eq (α := ↥g.cycleFactorsFinset)
      ((((OnCycleFactors.toPermHom g : (a : ↥(centralizer {g})) → Perm ↥g.cycleFactorsFinset)
                ((a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(centralizer {g})) τ : ↥(centralizer {g})) :
              Perm ↥g.cycleFactorsFinset) :
            (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
          x :
        ↥g.cycleFactorsFinset)
      (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) x :
        ↥g.cycleFactorsFinset)
⊢ (OnCycleFactors.toPermHom g : (a : ↥(centralizer {g})) → Perm ↥g.cycleFactorsFinset)
      ((a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(centralizer {g})) τ : ↥(centralizer {g})) =
    (↑τ : Perm ↥g.cycleFactorsFinset)

Tactic:
apply ext

Premises used: Equiv.Perm.ext
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
c : ↥g.cycleFactorsFinset
H :
  HSMul.hSMul (α := ↥(centralizer {g}))
      ((a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(centralizer {g})) τ : ↥(centralizer {g})) c =
    ((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c
H₁ H₂ :
  Eq (α := ↥g.cycleFactorsFinset)
    (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
      ↥g.cycleFactorsFinset)
    (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
      ↥g.cycleFactorsFinset)
⊢ Eq (α := ↥g.cycleFactorsFinset)
    ((((OnCycleFactors.toPermHom g : (a : ↥(centralizer {g})) → Perm ↥g.cycleFactorsFinset)
              ((a.toCentralizer : (a : ↥(range_toPermHom' g)) → ↥(centralizer {g})) τ : ↥(centralizer {g})) :
            Perm ↥g.cycleFactorsFinset) :
          (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
        c :
      ↥g.cycleFactorsFinset)
    (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
      ↥g.cycleFactorsFinset)

Tactic:
rw [OnCycleFactors.toPermHom_apply, toCentralizer_equivariant]

Premises used: Equiv.Perm.Basis.toCentralizer_equivariant, Equiv.Perm.OnCycleFactors.toPermHom_apply
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
τ : Perm ↥g.cycleFactorsFinset
mp :
  Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (MonoidHom.range (toPermHom g)) τ →
    ∀ (c : ↥g.cycleFactorsFinset),
      Finset.card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)) =
        #(↑c : Perm α).support
mpr :
  (∀ (c : ↥g.cycleFactorsFinset),
      Finset.card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)) =
        #(↑c : Perm α).support) →
    Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (MonoidHom.range (toPermHom g)) τ
⊢ Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (MonoidHom.range (toPermHom g)) τ ↔
    ∀ (c : ↥g.cycleFactorsFinset),
      Finset.card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)) =
        #(↑c : Perm α).support

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
k : ↥(centralizer {g})
c : ↥g.cycleFactorsFinset
mp : #(Finset.map (Equiv.toEmbedding (↑k : Perm α)) (↑c : Perm α).support) = #(↑c : Perm α).support
⊢ Finset.card.{u_1} (α := α)
      (support
        (↑((((toPermHom g : (a : ↥(centralizer {g})) → Perm ↥g.cycleFactorsFinset) k : Perm ↥g.cycleFactorsFinset) :
                (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
              c) :
          Perm α)) =
    #(↑c : Perm α).support

Tactic:
rw [coe_toPermHom, Equiv.Perm.support_conj]

Premises used: Equiv.Perm.OnCycleFactors.coe_toPermHom, Equiv.Perm.support_conj
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
k : ↥(centralizer {g})
c : ↥g.cycleFactorsFinset
⊢ #(Finset.map (Equiv.toEmbedding (↑k : Perm α)) (↑c : Perm α).support) = #(↑c : Perm α).support

Tactic:
apply Finset.card_map

Premises used: Finset.card_map
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
τ : Perm ↥g.cycleFactorsFinset
mpr :
  ∀ (a : g.Basis),
    (∀ (c : ↥g.cycleFactorsFinset),
        Finset.card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)) =
          #(↑c : Perm α).support) →
      Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (MonoidHom.range (toPermHom g)) τ
⊢ (∀ (c : ↥g.cycleFactorsFinset),
      Finset.card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)) =
        #(↑c : Perm α).support) →
    Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (MonoidHom.range (toPermHom g)) τ

Tactic:
obtain ⟨a⟩ := Basis.nonempty g

Premises used: Equiv.Perm.Basis.nonempty
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
τ : Perm ↥g.cycleFactorsFinset
a : g.Basis
⊢ (∀ (c : ↥g.cycleFactorsFinset),
      Finset.card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)) =
        #(↑c : Perm α).support) →
    Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (MonoidHom.range (toPermHom g)) τ

Tactic:
fun hτ ↦ ⟨toCentralizer a ⟨τ, hτ⟩, toPermHom_apply_toCentralizer a ⟨τ, hτ⟩⟩

Premises used: Set.Mem, setOf, Equiv.Perm.Basis.toPermHom_apply_toCentralizer, Subtype.mk, Equiv.Perm.Basis.toCentralizer, Exists.intro, Set.range, DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
τ : Perm ↥g.cycleFactorsFinset
a : g.Basis
⊢ (∀ (c : ↥g.cycleFactorsFinset),
      Finset.card.{u_1} (α := α) (support (↑((τ : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)) =
        #(↑c : Perm α).support) →
    Membership.mem (γ := Subgroup (Perm ↥g.cycleFactorsFinset)) (MonoidHom.range (toPermHom g)) τ

Tactic:
exact fun hτ ↦ ⟨toCentralizer a ⟨τ, hτ⟩, toPermHom_apply_toCentralizer a ⟨τ, hτ⟩⟩