ι : Type ?u.2180524
α : Type u_1
β : Type ?u.2180530
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y : α
f : Perm α
x : α
z : ℤ
⊢ ↑(cycleOf f x ^ z) x = ↑(f ^ z) x
ι : Type ?u.2180524
α : Type u_1
β : Type ?u.2180530
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y : α
f : Perm α
x : α
⊢ ∀ (n : ℤ), ↑(cycleOf f x ^ n) x = ↑(f ^ n) x
intro z
case ofNat
ι : Type ?u.2180524
α : Type u_1
β : Type ?u.2180530
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y : α
f : Perm α
x : α
z : ℕ
⊢ ↑(cycleOf f x ^ Int.ofNat z) x = ↑(f ^ Int.ofNat z) x

case negSucc
ι : Type ?u.2180524
α : Type u_1
β : Type ?u.2180530
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y : α
f : Perm α
x : α
hz : ℕ
⊢ ↑(cycleOf f x ^ Int.negSucc hz) x = ↑(f ^ Int.negSucc hz) x
ι : Type ?u.2180524
α : Type u_1
β : Type ?u.2180530
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y : α
f : Perm α
x : α
z : ℤ
⊢ ↑(cycleOf f x ^ z) x = ↑(f ^ z) x
induction' z with z hz
no goals
case ofNat
ι : Type ?u.2180524
α : Type u_1
β : Type ?u.2180530
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y : α
f : Perm α
x : α
z : ℕ
⊢ ↑(cycleOf f x ^ Int.ofNat z) x = ↑(f ^ Int.ofNat z) x
exact cycleOf_pow_apply_self f x z
no goals
case negSucc
ι : Type ?u.2180524
α : Type u_1
β : Type ?u.2180530
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y : α
f : Perm α
x : α
hz : ℕ
⊢ ↑(cycleOf f x ^ Int.negSucc hz) x = ↑(f ^ Int.negSucc hz) x
rw [zpow_negSucc, ← inv_pow, cycleOf_inv, zpow_negSucc, ← inv_pow, cycleOf_pow_apply_self]