-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem zpow_eq_zpow_on_iff [DecidableEq α] [Fintype α]
    (g : Perm α) {m n : ℤ} {x : α} (hx : g x ≠ x) :
    (g ^ m) x = (g ^ n) x ↔ m % #(g.cycleOf x).support = n % #(g.cycleOf x).support

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (m - n) % ↑(#(g.cycleOf x).support) = 0 ↔ ↑(#(g.cycleOf x).support) ∣ m - n

Tactic:
rw [← Int.dvd_iff_emod_eq_zero]

Result:
no goals

Proof state:
case hg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (g.cycleOf x).IsCycle

Tactic:
exact isCycle_cycleOf g hx

Result:
no goals

Proof state:
case hx
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ g x ≠ x

Tactic:
exact hx

Result:
no goals

Proof state:
case hx
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (g.cycleOf x) x ≠ x

Tactic:
simp only [mem_support, cycleOf_apply_self]

Result:
case hx
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ g x ≠ x

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (g ^ (m - n)) x = x ↔ ↑(#(g.cycleOf x).support) ∣ m - n

Tactic:
rw [← cycleOf_zpow_apply_self g x, cycle_zpow_mem_support_iff]

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (m - n) % ↑(#(g.cycleOf x).support) = 0 ↔ ↑(#(g.cycleOf x).support) ∣ m - n

case hg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (g.cycleOf x).IsCycle

case hx
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (g.cycleOf x) x ≠ x

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (g ^ n * g ^ (m - n)) x = (g ^ n) x ↔ (m - n) % ↑(#(g.cycleOf x).support) = 0

Tactic:
simp only [coe_mul, Function.comp_apply, EmbeddingLike.apply_eq_iff_eq]

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (g ^ (m - n)) x = x ↔ (m - n) % ↑(#(g.cycleOf x).support) = 0

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (g ^ m) x = (g ^ n) x ↔ (m - n) % ↑(#(g.cycleOf x).support) = 0

Tactic:
conv_lhs => rw [← Int.sub_add_cancel m n, Int.add_comm, zpow_add]

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (g ^ n * g ^ (m - n)) x = (g ^ n) x ↔ (m - n) % ↑(#(g.cycleOf x).support) = 0

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (g ^ m) x = (g ^ n) x ↔ m % ↑(#(g.cycleOf x).support) = n % ↑(#(g.cycleOf x).support)

Tactic:
rw [Int.emod_eq_emod_iff_emod_sub_eq_zero]

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (g ^ m) x = (g ^ n) x ↔ (m - n) % ↑(#(g.cycleOf x).support) = 0

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (g ^ (m - n)) x = x ↔ (m - n) % ↑(#(g.cycleOf x).support) = 0

Tactic:
rw [← Int.dvd_iff_emod_eq_zero]

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (g ^ (m - n)) x = x ↔ ↑(#(g.cycleOf x).support) ∣ m - n