case pos
ι : Type ?u.2520927
α : Type u_1
β : Type ?u.2520933
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y : α
f : Perm α
n : ℕ
x : α
hx : ↑f x = x
⊢ ↑(f ^ (n % card (support (cycleOf f x)))) x = ↑(f ^ n) x

case neg
ι : Type ?u.2520927
α : Type u_1
β : Type ?u.2520933
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y : α
f : Perm α
n : ℕ
x : α
hx : ¬↑f x = x
⊢ ↑(f ^ (n % card (support (cycleOf f x)))) x = ↑(f ^ n) x
ι : Type ?u.2520927
α : Type u_1
β : Type ?u.2520933
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y : α
f : Perm α
n : ℕ
x : α
⊢ ↑(f ^ (n % card (support (cycleOf f x)))) x = ↑(f ^ n) x
by_cases hx : f x = x
no goals
case pos
ι : Type ?u.2520927
α : Type u_1
β : Type ?u.2520933
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y : α
f : Perm α
n : ℕ
x : α
hx : ↑f x = x
⊢ ↑(f ^ (n % card (support (cycleOf f x)))) x = ↑(f ^ n) x
rw [pow_apply_eq_self_of_apply_eq_self hx, pow_apply_eq_self_of_apply_eq_self hx]
no goals
case neg
ι : Type ?u.2520927
α : Type u_1
β : Type ?u.2520933
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f✝ g : Perm α
x✝ y : α
f : Perm α
n : ℕ
x : α
hx : ¬↑f x = x
⊢ ↑(f ^ (n % card (support (cycleOf f x)))) x = ↑(f ^ n) x
rw [← cycleOf_pow_apply_self, ← cycleOf_pow_apply_self f, ← (isCycle_cycleOf f hx).orderOf,
  ← pow_eq_mod_orderOf]