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)
x : α
c : ↥g.cycleFactorsFinset
hx : Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
d : ↥g.cycleFactorsFinset
hx' : x ∈ (↑d : Perm α).support
inl : ∀ (hx : x ∉ g.support) (d : ↥g.cycleFactorsFinset) (hx' : x ∈ (↑d : Perm α).support), False
⊢ False

Tactic:
rw [Function.mem_fixedPoints_iff, ← notMem_support] at hx

Premises used: Equiv.Perm.notMem_support, Function.mem_fixedPoints_iff
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hx : x ∉ g.support
d : ↥g.cycleFactorsFinset
hx' : x ∈ (↑d : Perm α).support
inl : x ∈ g.support
⊢ False

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

Tactic:
mem_cycleFactorsFinset_support_le d.prop hx'

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

Tactic:
exact mem_cycleFactorsFinset_support_le d.prop hx'

Premises used: Subtype.prop, Equiv.Perm.mem_cycleFactorsFinset_support_le
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c d : ↥g.cycleFactorsFinset
hd : x ∈ (↑d : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) d : α) = x
inr :
  Membership.mem (α := α) (γ := Finset α)
      (support
        (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α))
      ((g ^ m : (a : α) → α)
          ((a : (a : ↥g.cycleFactorsFinset) → α)
              (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) d :
                ↥g.cycleFactorsFinset) :
            α) :
        α) ↔
    x ∈ (↑c : Perm α).support
⊢ Membership.mem (γ := Finset α)
      (support
        (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α))
      (a.ofPermHomFun τ x) ↔
    x ∈ (↑c : Perm α).support

Tactic:
rw [ofPermHomFun_apply_of_cycleOf_mem a τ hd hm]

Premises used: Equiv.Perm.Basis.ofPermHomFun_apply_of_cycleOf_mem
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c d : ↥g.cycleFactorsFinset
hd : x ∈ (↑d : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) d : α) = x
inr :
  Membership.mem (α := α) (γ := Finset α)
      (support
        (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α))
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) d :
            ↥g.cycleFactorsFinset) :
        α) ↔
    x ∈ (↑c : Perm α).support
⊢ Membership.mem (α := α) (γ := Finset α)
      (support
        (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α))
      ((g ^ m : (a : α) → α)
          ((a : (a : ↥g.cycleFactorsFinset) → α)
              (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) d :
                ↥g.cycleFactorsFinset) :
            α) :
        α) ↔
    x ∈ (↑c : Perm α).support

Tactic:
rw [zpow_apply_mem_support_of_mem_cycleFactorsFinset_iff]

Premises used: Equiv.Perm.zpow_apply_mem_support_of_mem_cycleFactorsFinset_iff
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c d : ↥g.cycleFactorsFinset
hd : x ∈ (↑d : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) d : α) = x
pos :
  ∀ (h : c = d),
    Membership.mem (α := α) (γ := Finset α)
        (support
          (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α))
        ((a : (a : ↥g.cycleFactorsFinset) → α)
            (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) d :
              ↥g.cycleFactorsFinset) :
          α) ↔
      x ∈ (↑c : Perm α).support
neg :
  ∀ (h : ¬c = d),
    Membership.mem (α := α) (γ := Finset α)
        (support
          (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α))
        ((a : (a : ↥g.cycleFactorsFinset) → α)
            (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) d :
              ↥g.cycleFactorsFinset) :
          α) ↔
      x ∈ (↑c : Perm α).support
⊢ Membership.mem (α := α) (γ := Finset α)
      (support
        (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α))
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) d :
            ↥g.cycleFactorsFinset) :
        α) ↔
    x ∈ (↑c : Perm α).support

Tactic:
by_cases h : c = d
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c d : ↥g.cycleFactorsFinset
hd : x ∈ (↑d : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) d : α) = x
h : c = d
⊢ Membership.mem (α := α) (γ := Finset α)
      (support
        (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α))
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) d :
            ↥g.cycleFactorsFinset) :
        α) ↔
    x ∈ (↑c : Perm α).support

Tactic:
simp only [h, hd, mem_support_self]

Premises used: Equiv.Perm.Basis.mem_support_self
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c d : ↥g.cycleFactorsFinset
hd : x ∈ (↑d : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) d : α) = x
h : ¬c = d
⊢ (↑c : Perm α).Disjoint (↑d : Perm α)

Tactic:
have H : Disjoint c.val d.val :=
        cycleFactorsFinset_pairwise_disjoint g c.prop d.prop (Subtype.coe_ne_coe.mpr h)
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c d : ↥g.cycleFactorsFinset
hd : x ∈ (↑d : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) d : α) = x
h : ¬c = d
H : (↑c : Perm α).Disjoint (↑d : Perm α)
h' :
  Eq.{u_1 + 1} (α := Perm α)
    (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)
    (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) d) : Perm α)
apply : c = d
⊢ False

Tactic:
apply h
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c d : ↥g.cycleFactorsFinset
hd : x ∈ (↑d : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) d : α) = x
h : ¬c = d
H : (↑c : Perm α).Disjoint (↑d : Perm α)
h' :
  Eq.{u_1 + 1} (α := Perm α)
    (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)
    (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) d) : Perm α)
⊢ c = d

Tactic:
simpa only [Subtype.coe_inj, EmbeddingLike.apply_eq_iff_eq] using h'

Premises used: Subtype.coe_inj, EmbeddingLike.apply_eq_iff_eq
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c d : ↥g.cycleFactorsFinset
hd : x ∈ (↑d : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) d : α) = x
h : ¬c = d
H : (↑c : Perm α).Disjoint (↑d : Perm α)
⊢ Disjoint.{u_1} (α := α)
    (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)
    (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) d) : Perm α)

Tactic:
have H' : Disjoint ((τ : Perm g.cycleFactorsFinset) c : Perm α)
        ((τ : Perm g.cycleFactorsFinset) d : Perm α) :=
        cycleFactorsFinset_pairwise_disjoint g ((τ : Perm g.cycleFactorsFinset) c).prop
          ((τ : Perm g.cycleFactorsFinset) d).prop (by
          intro h'; apply h
          simpa only [Subtype.coe_inj, EmbeddingLike.apply_eq_iff_eq] using h')
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c d : ↥g.cycleFactorsFinset
hd : x ∈ (↑d : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) d : α) = x
h : ¬c = d
H : (↑c : Perm α).Disjoint (↑d : Perm α)
H' :
  Disjoint.{u_1} (α := α)
    (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)
    (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) d) : Perm α)
⊢ ∀ ⦃a : α⦄, a ∈ (↑d : Perm α).support → a ∉ (↑c : Perm α).support

Tactic:
rw [disjoint_iff_disjoint_support, Finset.disjoint_right] at H H'

Premises used: Finset.disjoint_right, Equiv.Perm.disjoint_iff_disjoint_support
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c d : ↥g.cycleFactorsFinset
hd : x ∈ (↑d : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) d : α) = x
h : ¬c = d
H : (↑c : Perm α).Disjoint (↑d : Perm α)
H' :
  Disjoint.{u_1} (α := α)
    (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)
    (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) d) : Perm α)
H₁ : ∀ ⦃a : α⦄, a ∈ (↑d : Perm α).support → a ∉ (↑c : Perm α).support
⊢ ∀ ⦃a : α⦄,
    Membership.mem (γ := Finset α)
        (support
          (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) d) : Perm α))
        a →
      a ∉
        support
          (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)

Tactic:
rw [disjoint_iff_disjoint_support, Finset.disjoint_right] at H H'

Premises used: Finset.disjoint_right, Equiv.Perm.disjoint_iff_disjoint_support
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c d : ↥g.cycleFactorsFinset
hd : x ∈ (↑d : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) d : α) = x
h : ¬c = d
H : ∀ ⦃a : α⦄, a ∈ (↑d : Perm α).support → a ∉ (↑c : Perm α).support
H' :
  ∀ ⦃a : α⦄,
    Membership.mem (γ := Finset α)
        (support
          (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) d) : Perm α))
        a →
      a ∉
        support
          (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α)
⊢ Membership.mem (α := α) (γ := Finset α)
      (support
        (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α))
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) d :
            ↥g.cycleFactorsFinset) :
        α) ↔
    x ∈ (↑c : Perm α).support

Tactic:
simp only [H hd, H' (mem_support_self a _)]

Premises used: Equiv.Perm.Basis.mem_support_self
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
inl :
  ∀ (hx : Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x),
    a.ofPermHomFun τ ((g ^ j : (a : α) → α) x) = (g ^ j : (a : α) → α) (a.ofPermHomFun τ x)
inr :
  ∀
    (hx :
      ∃ (c : ↥g.cycleFactorsFinset) (_ : x ∈ (↑c : Perm α).support) (m : ℤ),
        (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x),
    a.ofPermHomFun τ ((g ^ j : (a : α) → α) x) = (g ^ j : (a : α) → α) (a.ofPermHomFun τ x)
⊢ a.ofPermHomFun τ ((g ^ j : (a : α) → α) x) = (g ^ j : (a : α) → α) (a.ofPermHomFun τ x)

Tactic:
rcases mem_fixedPoints_or_exists_zpow_eq a x with (hx | hx)

Premises used: Equiv.Perm.Basis.mem_fixedPoints_or_exists_zpow_eq
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
hx : Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
inl : Membership.mem (α := α) (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) ((g ^ j : (a : α) → α) x : α)
⊢ a.ofPermHomFun τ ((g ^ j : (a : α) → α) x) = (g ^ j : (a : α) → α) (a.ofPermHomFun τ x)

Tactic:
rw [ofPermHomFun_apply_of_mem_fixedPoints a τ hx, ofPermHomFun_apply_of_mem_fixedPoints]

Premises used: Equiv.Perm.Basis.ofPermHomFun_apply_of_mem_fixedPoints
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
hx : Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
inl : Eq (α := α) ((g ^ (j + 1) : (a : α) → α) x : α) ((g ^ j : (a : α) → α) x : α)
⊢ Eq (α := α) ((g : (a : α) → α) ((g ^ j : (a : α) → α) x : α) : α) ((g ^ j : (a : α) → α) x : α)

Tactic:
simp only [← mul_apply, ← zpow_one_add, add_comm]

Premises used: zpow_one_add, add_comm, 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 : α
j : ℤ
hx : Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
rw : ((g ^ (j + 1) : (a : α) → α) x : α)
| ((g ^ j : (a : α) → α) x : α)

Tactic:
rw [← hx, ← mul_apply, ← zpow_add_one]

Premises used: zpow_add_one, 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 : α
j : ℤ
hx : Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
conv_rhs : Eq (α := α) ((g ^ (j + 1) : (a : α) → α) x : α) ((g ^ j : (a : α) → α) x : α)
inl : Eq (α := α) ((g ^ (j + 1) : (a : α) → α) x : α) ((g ^ (j + 1) : (a : α) → α) x : α)
⊢ Eq (α := α) ((g ^ (j + 1) : (a : α) → α) x : α) ((g ^ j : (a : α) → α) x : α)

Tactic:
conv_rhs => rw [← hx, ← mul_apply, ← zpow_add_one]

Premises used: zpow_add_one, 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 : α
j : ℤ
hx :
  ∃ (c : ↥g.cycleFactorsFinset) (_ : x ∈ (↑c : Perm α).support) (m : ℤ),
    (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
inr :
  ∀ (c : ↥g.cycleFactorsFinset) (hc : x ∈ (↑c : Perm α).support) (m : ℤ)
    (hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x),
    a.ofPermHomFun τ ((g ^ j : (a : α) → α) x) = (g ^ j : (a : α) → α) (a.ofPermHomFun τ x)
⊢ a.ofPermHomFun τ ((g ^ j : (a : α) → α) x) = (g ^ j : (a : α) → α) (a.ofPermHomFun τ x)

Tactic:
obtain ⟨c, hc, m, hm⟩ := hx
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
rw :
  Eq (α := α) ((g ^ j * g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) : α)
    ((g ^ j : (a : α) → α) x : α)
rw₁ :
  Eq (α := α) ((g ^ j : (a : α) → α) ((g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) : α) : α)
    ((g ^ j : (a : α) → α) x : α)
rw₂ rw₃ : Eq (α := α) ((g ^ j : (a : α) → α) x : α) ((g ^ j : (a : α) → α) x : α)
⊢ Eq (α := α) ((g ^ (j + m) : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) : α)
    ((g ^ j : (a : α) → α) x : α)

Tactic:
rw [zpow_add, mul_apply, hm]

Premises used: zpow_add, 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 : α
j : ℤ
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
⊢ Eq (α := α) ((g ^ (j + m) : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) : α)
    ((g ^ j : (a : α) → α) x : α)

Tactic:
have hm' : (g ^ (j + m)) (a c) = (g ^ j) x := by rw [zpow_add, mul_apply, hm]
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
hm' :
  Eq (α := α) ((g ^ (j + m) : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) : α)
    ((g ^ j : (a : α) → α) x : α)
rw : Membership.mem (α := α) (↑c : Perm α).support ((g ^ j : (a : α) → α) x : α)
⊢ a.ofPermHomFun τ ((g ^ j : (a : α) → α) x) = (g ^ j : (a : α) → α) (a.ofPermHomFun τ x)

Tactic:
rw [ofPermHomFun_apply_of_cycleOf_mem a τ hc hm, ofPermHomFun_apply_of_cycleOf_mem a τ _ hm',
      ← mul_apply, ← zpow_add]

Premises used: zpow_add, Equiv.Perm.Basis.ofPermHomFun_apply_of_cycleOf_mem, 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 : α
j : ℤ
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
hm' :
  Eq (α := α) ((g ^ (j + m) : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) : α)
    ((g ^ j : (a : α) → α) x : α)
⊢ Membership.mem (α := α) (↑c : Perm α).support ((g ^ j : (a : α) → α) x : α)

Tactic:
zpow_apply_mem_support_of_mem_cycleFactorsFinset_iff.mpr hc

Premises used: Iff.mpr, Equiv.Perm.zpow_apply_mem_support_of_mem_cycleFactorsFinset_iff
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
hm' :
  Eq (α := α) ((g ^ (j + m) : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) : α)
    ((g ^ j : (a : α) → α) x : α)
⊢ Membership.mem (α := α) (↑c : Perm α).support ((g ^ j : (a : α) → α) x : α)

Tactic:
exact zpow_apply_mem_support_of_mem_cycleFactorsFinset_iff.mpr hc

Premises used: Iff.mpr, Equiv.Perm.zpow_apply_mem_support_of_mem_cycleFactorsFinset_iff
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
σ τ : ↥(range_toPermHom' g)
x : α
inl :
  ∀ (hx : Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x),
    a.ofPermHomFun (σ * τ) x = a.ofPermHomFun σ (a.ofPermHomFun τ x)
inr :
  ∀ (c : ↥g.cycleFactorsFinset) (hc : x ∈ (↑c : Perm α).support) (m : ℤ)
    (hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x),
    a.ofPermHomFun (σ * τ) x = a.ofPermHomFun σ (a.ofPermHomFun τ x)
⊢ a.ofPermHomFun (σ * τ) x = a.ofPermHomFun σ (a.ofPermHomFun τ x)

Tactic:
rcases mem_fixedPoints_or_exists_zpow_eq a x with (hx | ⟨c, hc, m, hm⟩)

Premises used: Equiv.Perm.Basis.mem_fixedPoints_or_exists_zpow_eq
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
σ τ : ↥(range_toPermHom' g)
x : α
hx : Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
⊢ a.ofPermHomFun (σ * τ) x = a.ofPermHomFun σ (a.ofPermHomFun τ x)

Tactic:
simp only [ofPermHomFun_apply_of_mem_fixedPoints a _ hx]

Premises used: Equiv.Perm.Basis.ofPermHomFun_apply_of_mem_fixedPoints
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
σ τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
inr :
  (g ^ m : (a : α) → α)
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          (((↑(σ * τ) : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
            ↥g.cycleFactorsFinset) :
        α) =
    a.ofPermHomFun σ
      ((g ^ m : (a : α) → α)
        ((a : (a : ↥g.cycleFactorsFinset) → α)
            (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
              ↥g.cycleFactorsFinset) :
          α))
⊢ a.ofPermHomFun (σ * τ) x = a.ofPermHomFun σ (a.ofPermHomFun τ x)

Tactic:
simp only [ofPermHomFun_apply_of_cycleOf_mem a _ hc hm]

Premises used: Equiv.Perm.Basis.ofPermHomFun_apply_of_cycleOf_mem
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
σ τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
inr :
  Eq (α := α)
    ((g ^ m : (a : α) → α)
        ((a : (a : ↥g.cycleFactorsFinset) → α)
            (((↑(σ * τ) : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
              ↥g.cycleFactorsFinset) :
          α) :
      α)
    ((g ^ m : (a : α) → α)
        ((a : (a : ↥g.cycleFactorsFinset) → α)
            (((↑σ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
                (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) :
              ↥g.cycleFactorsFinset) :
          α) :
      α)
rw :
  Membership.mem (α := α) (γ := Finset α)
    (support (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α))
    ((g ^ m : (a : α) → α)
        ((a : (a : ↥g.cycleFactorsFinset) → α)
            (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
              ↥g.cycleFactorsFinset) :
          α) :
      α)
⊢ (g ^ m : (a : α) → α)
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          (((↑(σ * τ) : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
            ↥g.cycleFactorsFinset) :
        α) =
    a.ofPermHomFun σ
      ((g ^ m : (a : α) → α)
        ((a : (a : ↥g.cycleFactorsFinset) → α)
            (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
              ↥g.cycleFactorsFinset) :
          α))

Tactic:
rw [ofPermHomFun_apply_of_cycleOf_mem a _ _ rfl]

Premises used: Equiv.Perm.Basis.ofPermHomFun_apply_of_cycleOf_mem, rfl