-- Mathlib/GroupTheory/Perm/Centralizer.lean
theorem ofPermHomFun_commute_zpow_apply (x : α) (j : ℤ) :
    ofPermHomFun a τ ((g ^ j) x) = (g ^ j) (ofPermHomFun a τ x)

Proof state:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
hx : x ∈ Function.fixedPoints ⇑g
⊢ a.ofPermHomFun τ ((g ^ j) x) = (g ^ j) (a.ofPermHomFun τ x)

Tactic:
rw [ofPermHomFun_apply_of_mem_fixedPoints a τ hx, ofPermHomFun_apply_of_mem_fixedPoints]

Result:
case inl.hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
hx : x ∈ Function.fixedPoints ⇑g
⊢ (g ^ j) x ∈ Function.fixedPoints ⇑g

Proof state:
case inl.hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
hx : x ∈ Function.fixedPoints ⇑g
⊢ (g ^ (j + 1)) x = (g ^ j) x

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

Result:
no goals

Proof state:
case inl.hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
hx : x ∈ Function.fixedPoints ⇑g
⊢ (g ^ j) x ∈ Function.fixedPoints ⇑g

Tactic:
rw [Function.mem_fixedPoints_iff]

Result:
case inl.hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
hx : x ∈ Function.fixedPoints ⇑g
⊢ g ((g ^ j) x) = (g ^ j) x

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
c : { x // x ∈ g.cycleFactorsFinset }
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
⊢ (g ^ (j + m)) (a c) = (g ^ j) x

Tactic:
rw [zpow_add, mul_apply, hm]

Result:
no goals

Proof state:
case inr.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
c : { x // x ∈ g.cycleFactorsFinset }
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
hm' : (g ^ (j + m)) (a c) = (g ^ j) x
⊢ a.ofPermHomFun τ ((g ^ j) x) = (g ^ j) (a.ofPermHomFun τ x)

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

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
c : { x // x ∈ g.cycleFactorsFinset }
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
hm' : (g ^ (j + m)) (a c) = (g ^ j) x
⊢ (g ^ j) x ∈ (↑c).support

Proof state:
case inl.hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
hx : x ∈ Function.fixedPoints ⇑g
⊢ g ((g ^ j) x) = (g ^ j) x

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

Result:
case inl.hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
hx : x ∈ Function.fixedPoints ⇑g
⊢ (g ^ (j + 1)) x = (g ^ j) x

Proof state:
case inr.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
c : { x // x ∈ g.cycleFactorsFinset }
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
⊢ a.ofPermHomFun τ ((g ^ j) x) = (g ^ j) (a.ofPermHomFun τ x)

Tactic:
have hm' : (g ^ (j + m)) (a c) = (g ^ j) x := by rw [zpow_add, mul_apply, hm]

Result:
case inr.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
c : { x // x ∈ g.cycleFactorsFinset }
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
hm' : (g ^ (j + m)) (a c) = (g ^ j) x
⊢ a.ofPermHomFun τ ((g ^ j) x) = (g ^ j) (a.ofPermHomFun τ x)

Proof state:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
hx : ∃ c, ∃ (_ : x ∈ (↑c).support), ∃ m, (g ^ m) (a c) = x
⊢ a.ofPermHomFun τ ((g ^ j) x) = (g ^ j) (a.ofPermHomFun τ x)

Tactic:
obtain ⟨c, hc, m, hm⟩ := hx

Result:
case inr.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
c : { x // x ∈ g.cycleFactorsFinset }
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
⊢ a.ofPermHomFun τ ((g ^ j) x) = (g ^ j) (a.ofPermHomFun τ x)

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
⊢ a.ofPermHomFun τ ((g ^ j) x) = (g ^ j) (a.ofPermHomFun τ x)

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

Result:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
hx : x ∈ Function.fixedPoints ⇑g
⊢ a.ofPermHomFun τ ((g ^ j) x) = (g ^ j) (a.ofPermHomFun τ x)

case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
hx : ∃ c, ∃ (_ : x ∈ (↑c).support), ∃ m, (g ^ m) (a c) = x
⊢ a.ofPermHomFun τ ((g ^ j) x) = (g ^ j) (a.ofPermHomFun τ x)

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
c : { x // x ∈ g.cycleFactorsFinset }
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
hm' : (g ^ (j + m)) (a c) = (g ^ j) x
⊢ (g ^ j) x ∈ (↑c).support

Tactic:
exact zpow_apply_mem_support_of_mem_cycleFactorsFinset_iff.mpr hc

Result:
no goals