Theorem: Equiv.Perm.zpow_mod_card_support_cycleOf_self_apply (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ inst✝ : Fintype α
f : Perm α
n : ℤ
x : α
⊢ (f ^ (n % ↑(support (cycleOf f x)).card)) x = (f ^ n) x
Tactic:
by_cases hx : f x = x
State after:
case pos
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ inst✝ : Fintype α
f : Perm α
n : ℤ
x : α
hx : f x = x
⊢ (f ^ (n % ↑(support (cycleOf f x)).card)) x = (f ^ n) x

case neg
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ inst✝ : Fintype α
f : Perm α
n : ℤ
x : α
hx : ¬f x = x
⊢ (f ^ (n % ↑(support (cycleOf f x)).card)) x = (f ^ n) x

State before:
case pos
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ inst✝ : Fintype α
f : Perm α
n : ℤ
x : α
hx : f x = x
⊢ (f ^ (n % ↑(support (cycleOf f x)).card)) x = (f ^ n) x
Tactic:
rw [Equiv.Perm.zpow_apply_eq_self_of_apply_eq_self hx,
  Equiv.Perm.zpow_apply_eq_self_of_apply_eq_self hx]
State after:
no goals

State before:
case neg
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ inst✝ : Fintype α
f : Perm α
n : ℤ
x : α
hx : ¬f x = x
⊢ (f ^ (n % ↑(support (cycleOf f x)).card)) x = (f ^ n) x
Tactic:
rw [← f.cycleOf_zpow_apply_self, ← f.cycleOf_zpow_apply_self,
  ← (f.isCycle_cycleOf hx).orderOf, zpow_mod_orderOf]
State after:
no goals