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

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (g ^ m) x = (g ^ n) x ↔ m % ↑(support (cycleOf g x)).card = n % ↑(support (cycleOf g x)).card
Tactic:
rw [Int.emod_eq_emod_iff_emod_sub_eq_zero]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (g ^ m) x = (g ^ n) x ↔ (m - n) % ↑(support (cycleOf g x)).card = 0

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (g ^ m) x = (g ^ n) x ↔ (m - n) % ↑(support (cycleOf g x)).card = 0
Tactic:
conv_lhs => rw [← Int.sub_add_cancel m n, Int.add_comm, zpow_add]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (g ^ n * g ^ (m - n)) x = (g ^ n) x ↔ (m - n) % ↑(support (cycleOf g x)).card = 0

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (g ^ n * g ^ (m - n)) x = (g ^ n) x ↔ (m - n) % ↑(support (cycleOf g x)).card = 0
Tactic:
simp only [coe_mul, Function.comp_apply, EmbeddingLike.apply_eq_iff_eq,
  EuclideanDomain.mod_eq_zero]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (g ^ (m - n)) x = x ↔ ↑(support (cycleOf g x)).card ∣ m - n

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (g ^ (m - n)) x = x ↔ ↑(support (cycleOf g x)).card ∣ m - n
Tactic:
rw [← Equiv.Perm.cycleOf_zpow_apply_self g x]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (cycleOf g x ^ (m - n)) x = x ↔ ↑(support (cycleOf g x)).card ∣ m - n

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (cycleOf g x ^ (m - n)) x = x ↔ ↑(support (cycleOf g x)).card ∣ m - n
Tactic:
rw [Equiv.Perm.cycle_zpow_mem_support_iff]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (m - n) % ↑(support (cycleOf g x)).card = 0 ↔ ↑(support (cycleOf g x)).card ∣ m - n

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

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

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (m - n) % ↑(support (cycleOf g x)).card = 0 ↔ ↑(support (cycleOf g x)).card ∣ m - n
Tactic:
simp only [EuclideanDomain.mod_eq_zero]
State after:
no goals

State before:
case hg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ IsCycle (cycleOf g x)
Tactic:
exact Equiv.Perm.isCycle_cycleOf g hx
State after:
no goals

State before:
case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (cycleOf g x) x ≠ x
Tactic:
simp only [Equiv.Perm.mem_support, Equiv.Perm.cycleOf_apply_self]
State after:
case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ g x ≠ x

State before:
case hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ g x ≠ x
Tactic:
exact hx
State after:
no goals