ι : Type ?u.2245333
α : Type u_1
β : Type ?u.2245339
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y : α
f : Perm α
x : α
k : ℤ
⊢ ↑f (↑(f ^ k) x) = ↑(f ^ (k + 1)) x

ι : Type ?u.2245333
α : Type u_1
β : Type ?u.2245339
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y : α
f : Perm α
x : α
k : ℤ
⊢ SameCycle f x (↑(f ^ k) x)
ι : Type ?u.2245333
α : Type u_1
β : Type ?u.2245339
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y : α
f : Perm α
x : α
k : ℤ
⊢ ↑(cycleOf f x) (↑(f ^ k) x) = ↑(f ^ (k + 1)) x
rw [SameCycle.cycleOf_apply]
no goals
ι : Type ?u.2245333
α : Type u_1
β : Type ?u.2245339
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y : α
f : Perm α
x : α
k : ℤ
⊢ ↑f (↑(f ^ k) x) = ↑(f ^ (k + 1)) x
rw [add_comm, zpow_add, zpow_one, mul_apply]
no goals
ι : Type ?u.2245333
α : Type u_1
β : Type ?u.2245339
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y : α
f : Perm α
x : α
k : ℤ
⊢ SameCycle f x (↑(f ^ k) x)
exact ⟨k, rfl⟩