-- Mathlib/GroupTheory/Perm/Centralizer.lean
theorem ofPermHomFun_apply_of_cycleOf_mem {x : α} {c : g.cycleFactorsFinset}
    (hx : x ∈ c.val.support) {m : ℤ} (hm : (g ^ m) (a c) = x) :
    ofPermHomFun a τ x = (g ^ m) (a ((τ : Perm g.cycleFactorsFinset) c))

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : { x // x ∈ g.cycleFactorsFinset }
hx : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
hx' : ↑c = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ := Nat.find ⋯
hn : (g ^ ↑n) (a c) = x
⊢ a.ofPermHomFun τ x = (g ^ ↑n) (a (↑τ c))

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

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : { x // x ∈ g.cycleFactorsFinset }
hx : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
hx' : ↑c = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ := Nat.find ⋯
hn : (g ^ ↑n) (a c) = x
⊢ (g ^ Nat.find ⋯) (a (↑τ ⟨g.cycleOf x, hx''⟩)) = (g ^ ↑n) (a (↑τ c))

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : { x // x ∈ g.cycleFactorsFinset }
hx : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
hx' : ↑c = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ := Nat.find ⋯
hn : (g ^ ↑n) (a c) = x
this : a.ofPermHomFun τ x = (g ^ ↑n) (a (↑τ c))
⊢ ↑n ≡ m [ZMOD ↑(↑(↑τ c)).support.card]

Tactic:
simp only [τ.prop c]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : { x // x ∈ g.cycleFactorsFinset }
hx : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
hx' : ↑c = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ := Nat.find ⋯
hn : (g ^ ↑n) (a c) = x
this : a.ofPermHomFun τ x = (g ^ ↑n) (a (↑τ c))
⊢ ↑n ≡ m [ZMOD ↑(↑c).support.card]

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : { x // x ∈ g.cycleFactorsFinset }
hx : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
hx' : ↑c = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ := Nat.find ⋯
hn : (g ^ ↑n) (a c) = x
this : a.ofPermHomFun τ x = (g ^ ↑n) (a (↑τ c))
⊢ ↑n ≡ m [ZMOD ↑(↑c).support.card]

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

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : { x // x ∈ g.cycleFactorsFinset }
hx : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
hx' : ↑c = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ := Nat.find ⋯
hn : (g ^ ↑n) (a c) = x
this : a.ofPermHomFun τ x = (g ^ ↑n) (a (↑τ c))
⊢ (g ^ ↑n) (a c) = (g ^ m) (a c)

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : { x // x ∈ g.cycleFactorsFinset }
hx : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
hx' : ↑c = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ := Nat.find ⋯
hn : (g ^ ↑n) (a c) = x
⊢ a.ofPermHomFun τ x = (g ^ m) (a (↑τ c))

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]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : { x // x ∈ g.cycleFactorsFinset }
hx : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
hx' : ↑c = g.cycleOf x
hx'' : g.cycleOf x ∈ g.cycleFactorsFinset
n : ℕ := Nat.find ⋯
hn : (g ^ ↑n) (a c) = x
⊢ a.ofPermHomFun τ x = (g ^ ↑n) (a (↑τ c))