-- 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
⊢ a.ofPermHomFun τ x = (g ^ m) (a (↑τ c))

Tactic:
have hx'' : g.cycleOf x ∈ g.cycleFactorsFinset := hx' ▸ c.prop

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
⊢ a.ofPermHomFun τ x = (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
⊢ a.ofPermHomFun τ x = (g ^ m) (a (↑τ c))

Tactic:
set n := Nat.find (a.sameCycle hx'').exists_nat_pow_eq

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 ⋯
⊢ a.ofPermHomFun τ x = (g ^ m) (a (↑τ c))

Proof state:
case h.e_6.h.h.e_6.h
α : 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 ⋯
⊢ c = ⟨g.cycleOf x, hx''⟩

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

Result:
no goals

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
⊢ (g ^ Nat.find ⋯) (a (↑τ ⟨g.cycleOf x, hx''⟩)) = (g ^ ↑n) (a (↑τ c))

Tactic:
congr

Result:
case h.e_6.h.h.e_6.h.h.e_6.h.e_val
α : 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.cycleOf x = ↑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 ⋯
⊢ a.ofPermHomFun τ x = (g ^ m) (a (↑τ c))

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']

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 ^ m) (a (↑τ c))

Proof state:
case h.e_6.h.h.e_6.h.h.e_6.h.e_val
α : 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.cycleOf x = ↑c

Tactic:
exact hx'.symm

Result:
no goals

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))
⊢ (g ^ ↑n) (a c) = (g ^ m) (a c)

Tactic:
rw [hn, hm]

Result:
no goals

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 ⋯
⊢ (g ^ n) (a c) = (g ^ Nat.find ⋯) (a ⟨g.cycleOf x, hx''⟩)

Tactic:
congr

Result:
case h.e_6.h.h.e_6.h
α : 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 ⋯
⊢ c = ⟨g.cycleOf x, hx''⟩

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
⊢ a.ofPermHomFun τ x = (g ^ m) (a (↑τ c))

Tactic:
have hx' : c = g.cycleOf x := cycle_is_cycleOf hx (Subtype.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
⊢ a.ofPermHomFun τ x = (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
this : a.ofPermHomFun τ x = (g ^ ↑n) (a (↑τ c))
⊢ a.ofPermHomFun τ x = (g ^ m) (a (↑τ c))

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))]

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 ⋯
⊢ (g ^ ↑n) (a c) = x

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

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 ⋯
⊢ (g ^ n) (a c) = (g ^ Nat.find ⋯) (a ⟨g.cycleOf x, hx''⟩)