awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (hypothesis)
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
⊢ a.ofPermHomFun τ x =
    (g ^ m : (a : α) → α)
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
            ↥g.cycleFactorsFinset) :
        α)
have hx' : (↑c : Perm α) = g.cycleOf x
Tactic: have hx' : c = g.cycleOf x := cycle_is_cycleOf hx (Subtype.prop c)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (hypothesis)
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
⊢ a.ofPermHomFun τ x =
    (g ^ m : (a : α) → α)
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
            ↥g.cycleFactorsFinset) :
        α)
have hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
Tactic: have hx'' : g.cycleOf x ∈ g.cycleFactorsFinset := hx' ▸ c.prop
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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
have 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)
            sorry :
        (a : α) → α)
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx'') :
        α) :
    α)
Tactic: rw [← Nat.find_spec (a.sameCycle hx'').exists_nat_pow_eq, zpow_natCast]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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)
    ⋯
⊢ 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'') :
          α) :
      α)
have h : c = Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx''
Tactic: congr
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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)
    ⋯
⊢ c = Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx''
have h : (↑c : Perm α) = (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx'') : Perm α)
Tactic: rw [← Subtype.coe_inj, hx']
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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 α)
⊢ c = Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx''
have h₁ : g.cycleOf x = (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) (g.cycleOf x) hx'') : Perm α)
Tactic: rw [← Subtype.coe_inj, hx']
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (hypothesis)
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)
    ⋯
⊢ a.ofPermHomFun τ x =
    (g ^ m : (a : α) → α)
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
            ↥g.cycleFactorsFinset) :
        α)
have hn : (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']
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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) :
        α)
⊢ a.ofPermHomFun τ x =
    (g ^ m : (a : α) → α)
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
            ↥g.cycleFactorsFinset) :
        α)
have rw : (↑n : ℤ) ≡ m [ZMOD
  (↑(Finset.card.{u_1} (α := α)
        (support
          (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α))) :
    ℤ)]
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))]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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) :
        α)
⊢ (↑n : ℤ) ≡ m [ZMOD
    (↑(Finset.card.{u_1} (α := α)
          (support
            (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) :
              Perm α))) :
      ℤ)]
have simp : (↑n : ℤ) ≡ m [ZMOD (↑(#(↑c : Perm α).support) : ℤ)]
Tactic: simp only [τ.prop c]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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) :
        α)
⊢ (↑n : ℤ) ≡ m [ZMOD (↑(#(↑c : Perm α).support) : ℤ)]
have rw : Eq (α := α) ((HPow.hPow (β := ℤ) g (↑n : ℤ) : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) : α)
  ((g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) : α)
Tactic: rw [← IsCycleOn.zpow_apply_eq_zpow_apply
      (isCycleOn_support_of_mem_cycleFactorsFinset c.prop) (mem_support_self a c)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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) :
        α)
⊢ Eq (α := α) ((HPow.hPow (β := ℤ) g (↑n : ℤ) : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) : α)
    ((g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) : α)
have rw : x = (g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α)
Tactic: rw [hn, hm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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 : α)
⊢ Eq (α := α) ((HPow.hPow (β := ℤ) g (↑n : ℤ) : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) : α)
    ((g ^ m : (a : α) → α) ((a : (a : ↥g.cycleFactorsFinset) → α) c : α) : α)
have rw₁ : x = x
Tactic: rw [hn, hm]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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
⊢ a.ofPermHomFun τ x =
    (g ^ m : (a : α) → α)
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
            ↥g.cycleFactorsFinset) :
        α)
have suffices : a.ofPermHomFun τ x =
  (HPow.hPow (β := ℤ) g (↑n : ℤ) : (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]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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
⊢ a.ofPermHomFun τ x =
    (HPow.hPow (β := ℤ) g (↑n : ℤ) : (a : α) → α)
      ((a : (a : ↥g.cycleFactorsFinset) → α)
          (((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c :
            ↥g.cycleFactorsFinset) :
        α)
have 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)
            sorry :
        (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: simp only [ofPermHomFun, dif_pos hx'']
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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
⊢ 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) :
          α) :
      α)
have h : g.cycleOf x = (↑c : Perm α)
Tactic: congr
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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 = x
have hnc : g.cycleOf x ∉ g.cycleFactorsFinset
Tactic: rw [ofPermHomFun, dif_neg]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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.cycleOf x ∉ g.cycleFactorsFinset
have hnc : (g : (a : α) → α) x = x
Tactic: rw [cycleOf_mem_cycleFactorsFinset_iff, notMem_support]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
⊢ Membership.mem (γ := Finset α)
      (support
        (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α))
      (a.ofPermHomFun τ x) ↔
    x ∈ (↑c : Perm α).support
have 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
Tactic: rcases mem_fixedPoints_or_exists_zpow_eq a x with (hx | ⟨d, hd, m, hm⟩)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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
⊢ Membership.mem (γ := Finset α)
      (support
        (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α))
      (a.ofPermHomFun τ x) ↔
    x ∈ (↑c : Perm α).support
have 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
Tactic: rcases mem_fixedPoints_or_exists_zpow_eq a x with (hx | ⟨d, hd, m, hm⟩)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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
⊢ Membership.mem (γ := Finset α)
      (support
        (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α))
      (a.ofPermHomFun τ x) ↔
    x ∈ (↑c : Perm α).support
have inl : Membership.mem (γ := Finset α)
    (support (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α))
    x ↔
  x ∈ (↑c : Perm α).support
Tactic: simp only [ofPermHomFun_apply_of_mem_fixedPoints a τ hx]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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
⊢ Membership.mem (γ := Finset α)
      (support
        (↑(((↑τ : Perm ↥g.cycleFactorsFinset) : (a : ↥g.cycleFactorsFinset) → ↥g.cycleFactorsFinset) c) : Perm α))
      x ↔
    x ∈ (↑c : Perm α).support
have inl : ∀ (d : ↥g.cycleFactorsFinset), x ∉ (↑d : Perm α).support
Tactic: suffices ∀ (d : g.cycleFactorsFinset), x ∉ (d : Perm α).support by
      simp only [this]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Centralizer (goal)
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
⊢ False
have inl : ∀ (hx : x ∉ g.support) (d : ↥g.cycleFactorsFinset) (hx' : x ∈ (↑d : Perm α).support), False
Tactic: rw [Function.mem_fixedPoints_iff, ← notMem_support] at hx
Cleared hypotheses: hx, d, hx'