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
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
rw : g.SameCycle x x ∧ g.cycleOf x ∈ g.cycleFactorsFinset
⊢ x ∈ (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx) : Perm α).support

Tactic:
rw [mem_support_cycleOf_iff, ← cycleOf_mem_cycleFactorsFinset_iff]

Premises used: Equiv.Perm.mem_support_cycleOf_iff, Equiv.Perm.cycleOf_mem_cycleFactorsFinset_iff
-- Module: Mathlib.GroupTheory.Perm.Centralizer
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
x : α
hx : g.cycleOf x ∈ g.cycleFactorsFinset
⊢ g.SameCycle x x ∧ g.cycleOf x ∈ g.cycleFactorsFinset

Tactic:
simp [SameCycle.rfl, hx, and_self]

Premises used: Equiv.Perm.SameCycle.rfl, and_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 : ↥g.cycleFactorsFinset
hx : x ∈ (↑c : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
⊢ (↑c : Perm α) = g.cycleOf x

Tactic:
have hx' : c = g.cycleOf x := cycle_is_cycleOf hx (Subtype.prop c)
-- 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 ∈ (↑c : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
hx' : (↑c : Perm α) = g.cycleOf x
⊢ g.cycleOf x ∈ g.cycleFactorsFinset

Tactic:
have hx'' : g.cycleOf x ∈ g.cycleFactorsFinset := hx' ▸ c.prop
-- 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 ∈ (↑c : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
hx' : (↑c : Perm α) = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ :=
  Nat.find (p := fun (n : ℕ) ↦
    (g ^ n : (a : α) → α)
        ((a : (a : ↥g.cycleFactorsFinset) → α)
            (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx'') :
          α) =
      x)
    ⋯
rw :
  Eq (α := α) ((g ^ n : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) : α)
    ((g ^
            Nat.find (p := fun (n : ℕ) ↦
              (g ^ n : (a : α) → α)
                  ((a : (a : ↥g.cycleFactorsFinset) → α)
                      (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx'') :
                    α) =
                x)
              ⋯ :
          (a : α) → α)
        ((a : (a : ↥g.cycleFactorsFinset) → α)
            (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx'') :
          α) :
      α)
⊢ (HPow.hPow (β := ℤ) g (↑n : ℤ) : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x

Tactic:
rw [← Nat.find_spec (a.sameCycle hx'').exists_nat_pow_eq, zpow_natCast]

Premises used: zpow_natCast, Equiv.Perm.SameCycle.exists_nat_pow_eq, Equiv.Perm.Basis.sameCycle, Nat.find_spec
-- 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 ∈ (↑c : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
hx' : (↑c : Perm α) = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ :=
  Nat.find (p := fun (n : ℕ) ↦
    (g ^ n : (a : α) → α)
        ((a : (a : ↥g.cycleFactorsFinset) → α)
            (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx'') :
          α) =
      x)
    ⋯
h : c = Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx''
⊢ Eq (α := α) ((g ^ n : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) : α)
    ((g ^
            Nat.find (p := fun (n : ℕ) ↦
              (g ^ n : (a : α) → α)
                  ((a : (a : ↥g.cycleFactorsFinset) → α)
                      (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx'') :
                    α) =
                x)
              ⋯ :
          (a : α) → α)
        ((a : (a : ↥g.cycleFactorsFinset) → α)
            (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx'') :
          α) :
      α)

Tactic:
congr
-- 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 ∈ (↑c : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
hx' : (↑c : Perm α) = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ :=
  Nat.find (p := fun (n : ℕ) ↦
    (g ^ n : (a : α) → α)
        ((a : (a : ↥g.cycleFactorsFinset) → α)
            (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx'') :
          α) =
      x)
    ⋯
h : (↑c : Perm α) = (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx'') : Perm α)
h₁ h₂ : g.cycleOf x = (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx'') : Perm α)
⊢ c = Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx''

Tactic:
rw [← Subtype.coe_inj, hx']

Premises used: Subtype.coe_inj
-- 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 ∈ (↑c : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
hx' : (↑c : Perm α) = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ :=
  Nat.find (p := fun (n : ℕ) ↦
    (g ^ n : (a : α) → α)
        ((a : (a : ↥g.cycleFactorsFinset) → α)
            (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx'') :
          α) =
      x)
    ⋯
⊢ (HPow.hPow (β := ℤ) g (↑n : ℤ) : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x

Tactic:
have hn : (g ^ (n : ℤ)) (a c) = x := by
    rw [← Nat.find_spec (a.sameCycle hx'').exists_nat_pow_eq, zpow_natCast]
    congr
    rw [← Subtype.coe_inj, 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 ∈ (↑c : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
hx' : (↑c : Perm α) = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ :=
  Nat.find (p := fun (n : ℕ) ↦
    (g ^ n : (a : α) → α)
        ((a : (a : ↥g.cycleFactorsFinset) → α)
            (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx'') :
          α) =
      x)
    ⋯
hn : (HPow.hPow (β := ℤ) g (↑n : ℤ) : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
this :
  a.ofPermHomFun τ x =
    (HPow.hPow (β := ℤ) g (↑n : ℤ) : (a : α) → α)
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
            ↥g.cycleFactorsFinset) :
        α)
rw :
  (↑n : ℤ) ≡ m [ZMOD
    (↑(Finset.card.{u_1} (α := α)
          (support
            (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) :
              Perm α))) :
      ℤ)]
⊢ a.ofPermHomFun τ x =
    (g ^ m : (a : α) → α)
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
            ↥g.cycleFactorsFinset) :
        α)

Tactic:
rw [this, IsCycleOn.zpow_apply_eq_zpow_apply
      (isCycleOn_support_of_mem_cycleFactorsFinset ((τ : Perm g.cycleFactorsFinset) c).prop)
      (mem_support_self a ((τ : Perm g.cycleFactorsFinset) c))]

Premises used: Equiv.Perm.Basis.mem_support_self, Subtype.prop, Equiv.Perm.IsCycleOn.zpow_apply_eq_zpow_apply, Equiv.Perm.isCycleOn_support_of_mem_cycleFactorsFinset, Subtype.val, DFunLike.coe
-- 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 ∈ (↑c : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
hx' : (↑c : Perm α) = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ :=
  Nat.find (p := fun (n : ℕ) ↦
    (g ^ n : (a : α) → α)
        ((a : (a : ↥g.cycleFactorsFinset) → α)
            (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx'') :
          α) =
      x)
    ⋯
hn : (HPow.hPow (β := ℤ) g (↑n : ℤ) : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
this :
  a.ofPermHomFun τ x =
    (HPow.hPow (β := ℤ) g (↑n : ℤ) : (a : α) → α)
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
            ↥g.cycleFactorsFinset) :
        α)
simp : (↑n : ℤ) ≡ m [ZMOD (↑(#(↑c : Perm α).support) : ℤ)]
⊢ (↑n : ℤ) ≡ m [ZMOD
    (↑(Finset.card.{u_1} (α := α)
          (support
            (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) :
              Perm α))) :
      ℤ)]

Tactic:
simp only [τ.prop c]

Premises used: Subtype.prop
-- 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 ∈ (↑c : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
hx' : (↑c : Perm α) = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ :=
  Nat.find (p := fun (n : ℕ) ↦
    (g ^ n : (a : α) → α)
        ((a : (a : ↥g.cycleFactorsFinset) → α)
            (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx'') :
          α) =
      x)
    ⋯
hn : (HPow.hPow (β := ℤ) g (↑n : ℤ) : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
this :
  a.ofPermHomFun τ x =
    (HPow.hPow (β := ℤ) g (↑n : ℤ) : (a : α) → α)
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
            ↥g.cycleFactorsFinset) :
        α)
rw :
  Eq (α := α) ((HPow.hPow (β := ℤ) g (↑n : ℤ) : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) : α)
    ((g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) : α)
⊢ (↑n : ℤ) ≡ m [ZMOD (↑(#(↑c : Perm α).support) : ℤ)]

Tactic:
rw [← IsCycleOn.zpow_apply_eq_zpow_apply
      (isCycleOn_support_of_mem_cycleFactorsFinset c.prop) (mem_support_self a c)]

Premises used: Equiv.Perm.Basis.mem_support_self, Subtype.prop, Equiv.Perm.IsCycleOn.zpow_apply_eq_zpow_apply, Equiv.Perm.isCycleOn_support_of_mem_cycleFactorsFinset
-- 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 ∈ (↑c : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
hx' : (↑c : Perm α) = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ :=
  Nat.find (p := fun (n : ℕ) ↦
    (g ^ n : (a : α) → α)
        ((a : (a : ↥g.cycleFactorsFinset) → α)
            (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx'') :
          α) =
      x)
    ⋯
hn : (HPow.hPow (β := ℤ) g (↑n : ℤ) : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
this :
  a.ofPermHomFun τ x =
    (HPow.hPow (β := ℤ) g (↑n : ℤ) : (a : α) → α)
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
            ↥g.cycleFactorsFinset) :
        α)
rw : x = (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α)
rw₁ rw₂ : x = x
⊢ Eq (α := α) ((HPow.hPow (β := ℤ) g (↑n : ℤ) : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) : α)
    ((g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) : α)

Tactic:
rw [hn, hm]
-- 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 ∈ (↑c : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
hx' : (↑c : Perm α) = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ :=
  Nat.find (p := fun (n : ℕ) ↦
    (g ^ n : (a : α) → α)
        ((a : (a : ↥g.cycleFactorsFinset) → α)
            (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx'') :
          α) =
      x)
    ⋯
hn : (HPow.hPow (β := ℤ) g (↑n : ℤ) : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
suffices :
  a.ofPermHomFun τ x =
    (HPow.hPow (β := ℤ) g (↑n : ℤ) : (a : α) → α)
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
            ↥g.cycleFactorsFinset) :
        α)
⊢ a.ofPermHomFun τ x =
    (g ^ m : (a : α) → α)
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
            ↥g.cycleFactorsFinset) :
        α)

Tactic:
suffices ofPermHomFun a τ x = (g ^ (n : ℤ)) (a ((τ : Perm g.cycleFactorsFinset) c)) by
    rw [this, IsCycleOn.zpow_apply_eq_zpow_apply
      (isCycleOn_support_of_mem_cycleFactorsFinset ((τ : Perm g.cycleFactorsFinset) c).prop)
      (mem_support_self a ((τ : Perm g.cycleFactorsFinset) c))]
    simp only [τ.prop c]
    rw [← IsCycleOn.zpow_apply_eq_zpow_apply
      (isCycleOn_support_of_mem_cycleFactorsFinset c.prop) (mem_support_self a c)]
    rw [hn, hm]
-- 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 ∈ (↑c : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
hx' : (↑c : Perm α) = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ :=
  Nat.find (p := fun (n : ℕ) ↦
    (g ^ n : (a : α) → α)
        ((a : (a : ↥g.cycleFactorsFinset) → α)
            (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx'') :
          α) =
      x)
    ⋯
hn : (HPow.hPow (β := ℤ) g (↑n : ℤ) : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
simp :
  Eq (α := α)
    ((g ^
            Nat.find (p := fun (n : ℕ) ↦
              (g ^ n : (a : α) → α)
                  ((a : (a : ↥g.cycleFactorsFinset) → α)
                      (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx'') :
                    α) =
                x)
              ⋯ :
          (a : α) → α)
        ((a : (a : ↥g.cycleFactorsFinset) → α)
            (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
                (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx'') :
              ↥g.cycleFactorsFinset) :
          α) :
      α)
    ((HPow.hPow (β := ℤ) g (↑n : ℤ) : (a : α) → α)
        ((a : (a : ↥g.cycleFactorsFinset) → α)
            (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
              ↥g.cycleFactorsFinset) :
          α) :
      α)
⊢ a.ofPermHomFun τ x =
    (HPow.hPow (β := ℤ) g (↑n : ℤ) : (a : α) → α)
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
            ↥g.cycleFactorsFinset) :
        α)

Tactic:
simp only [ofPermHomFun, dif_pos hx'']

Premises used: dif_pos, Equiv.Perm.Basis.ofPermHomFun
-- 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 ∈ (↑c : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
hx' : (↑c : Perm α) = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ :=
  Nat.find (p := fun (n : ℕ) ↦
    (g ^ n : (a : α) → α)
        ((a : (a : ↥g.cycleFactorsFinset) → α)
            (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx'') :
          α) =
      x)
    ⋯
hn : (HPow.hPow (β := ℤ) g (↑n : ℤ) : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
h : g.cycleOf x = (↑c : Perm α)
⊢ Eq (α := α)
    ((g ^
            Nat.find (p := fun (n : ℕ) ↦
              (g ^ n : (a : α) → α)
                  ((a : (a : ↥g.cycleFactorsFinset) → α)
                      (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx'') :
                    α) =
                x)
              ⋯ :
          (a : α) → α)
        ((a : (a : ↥g.cycleFactorsFinset) → α)
            (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset)
                (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx'') :
              ↥g.cycleFactorsFinset) :
          α) :
      α)
    ((HPow.hPow (β := ℤ) g (↑n : ℤ) : (a : α) → α)
        ((a : (a : ↥g.cycleFactorsFinset) → α)
            (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
              ↥g.cycleFactorsFinset) :
          α) :
      α)

Tactic:
congr
-- 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 ∈ (↑c : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
hx' : (↑c : Perm α) = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ :=
  Nat.find (p := fun (n : ℕ) ↦
    (g ^ n : (a : α) → α)
        ((a : (a : ↥g.cycleFactorsFinset) → α)
            (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx'') :
          α) =
      x)
    ⋯
hn : (HPow.hPow (β := ℤ) g (↑n : ℤ) : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
⊢ g.cycleOf x = (↑c : Perm α)

Tactic:
hx'.symm

Premises used: Eq.symm
-- 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 ∈ (↑c : Perm α).support
m : ℤ
hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
hx' : (↑c : Perm α) = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ :=
  Nat.find (p := fun (n : ℕ) ↦
    (g ^ n : (a : α) → α)
        ((a : (a : ↥g.cycleFactorsFinset) → α)
            (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx'') :
          α) =
      x)
    ⋯
hn : (HPow.hPow (β := ℤ) g (↑n : ℤ) : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) = x
⊢ g.cycleOf x = (↑c : Perm α)

Tactic:
exact hx'.symm

Premises used: Eq.symm
-- 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
hnc : g.cycleOf x ∉ g.cycleFactorsFinset
⊢ a.ofPermHomFun τ x = x

Tactic:
rw [ofPermHomFun, dif_neg]

Premises used: dif_neg, Equiv.Perm.Basis.ofPermHomFun
-- 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
hnc : (g : (a : α) → α) x = x
⊢ g.cycleOf x ∉ g.cycleFactorsFinset

Tactic:
rw [cycleOf_mem_cycleFactorsFinset_iff, notMem_support]

Premises used: Equiv.Perm.notMem_support, Equiv.Perm.cycleOf_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 : α
hx : Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
⊢ (g : (a : α) → α) x = x

Tactic:
hx

Premises used: Set.Mem, setOf, Function.fixedPoints, Function.IsFixedPt
-- 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
⊢ (g : (a : α) → α) x = x

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)
x : α
c : ↥g.cycleFactorsFinset
inl :
  ∀ (hx : Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x),
    Membership.mem (γ := Finset α)
        (support
          (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α))
        (a.ofPermHomFun τ x) ↔
      x ∈ (↑c : Perm α).support
inr :
  ∀ (d : ↥g.cycleFactorsFinset) (hd : x ∈ (↑d : Perm α).support) (m : ℤ)
    (hm : (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) d : α) = x),
    Membership.mem (γ := Finset α)
        (support
          (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α))
        (a.ofPermHomFun τ x) ↔
      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:
rcases mem_fixedPoints_or_exists_zpow_eq a x with (hx | ⟨d, hd, 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 : α
c : ↥g.cycleFactorsFinset
hx : Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
inl :
  Membership.mem (γ := Finset α)
      (support
        (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α))
      x ↔
    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:
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
hx : Membership.mem (γ := Set α) (Function.fixedPoints (⇑g : (a : α) → α)) x
this : ∀ (d : ↥g.cycleFactorsFinset), x ∉ (↑d : Perm α).support
⊢ Membership.mem (γ := Finset α)
      (support
        (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α))
      x ↔
    x ∈ (↑c : Perm α).support

Tactic:
simp only [this]
-- 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
inl : ∀ (d : ↥g.cycleFactorsFinset), x ∉ (↑d : Perm α).support
⊢ Membership.mem (γ := Finset α)
      (support
        (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α))
      x ↔
    x ∈ (↑c : Perm α).support

Tactic:
suffices ∀ (d : g.cycleFactorsFinset), x ∉ (d : Perm α).support by
      simp only [this]