no goals
ι : Type ?u.208122
α : Type u_1
β : Type ?u.208128
f g : Perm α
p : α → Prop
x y z : α
inst✝ : Finite α
⊢ SameCycle f x y → ∃ i, i < orderOf f ∧ ↑(f ^ i) x = y
classical
  rintro ⟨k, rfl⟩
  use (k % orderOf f).natAbs
  have h₀ := Int.coe_nat_pos.mpr (orderOf_pos f)
  have h₁ := Int.emod_nonneg k h₀.ne'
  rw [← zpow_ofNat, Int.natAbs_of_nonneg h₁, ← zpow_eq_mod_orderOf]
  refine' ⟨_, by rfl⟩
  rw [← Int.ofNat_lt, Int.natAbs_of_nonneg h₁]
  exact Int.emod_lt_of_pos _ h₀
case intro
ι : Type ?u.208122
α : Type u_1
β : Type ?u.208128
f g : Perm α
p : α → Prop
x z : α
inst✝ : Finite α
k : ℤ
⊢ ∃ i, i < orderOf f ∧ ↑(f ^ i) x = ↑(f ^ k) x
ι : Type ?u.208122
α : Type u_1
β : Type ?u.208128
f g : Perm α
p : α → Prop
x y z : α
inst✝ : Finite α
⊢ SameCycle f x y → ∃ i, i < orderOf f ∧ ↑(f ^ i) x = y
rintro ⟨k, rfl⟩
case intro
ι : Type ?u.208122
α : Type u_1
β : Type ?u.208128
f g : Perm α
p : α → Prop
x z : α
inst✝ : Finite α
k : ℤ
⊢ Int.natAbs (k % ↑(orderOf f)) < orderOf f ∧ ↑(f ^ Int.natAbs (k % ↑(orderOf f))) x = ↑(f ^ k) x
case intro
ι : Type ?u.208122
α : Type u_1
β : Type ?u.208128
f g : Perm α
p : α → Prop
x z : α
inst✝ : Finite α
k : ℤ
⊢ ∃ i, i < orderOf f ∧ ↑(f ^ i) x = ↑(f ^ k) x
use (k % orderOf f).natAbs
case intro
ι : Type ?u.208122
α : Type u_1
β : Type ?u.208128
f g : Perm α
p : α → Prop
x z : α
inst✝ : Finite α
k : ℤ
h₀ : 0 < ↑(orderOf f)
⊢ Int.natAbs (k % ↑(orderOf f)) < orderOf f ∧ ↑(f ^ Int.natAbs (k % ↑(orderOf f))) x = ↑(f ^ k) x
case intro
ι : Type ?u.208122
α : Type u_1
β : Type ?u.208128
f g : Perm α
p : α → Prop
x z : α
inst✝ : Finite α
k : ℤ
⊢ Int.natAbs (k % ↑(orderOf f)) < orderOf f ∧ ↑(f ^ Int.natAbs (k % ↑(orderOf f))) x = ↑(f ^ k) x
have h₀ := Int.coe_nat_pos.mpr (orderOf_pos f)
case intro
ι : Type ?u.208122
α : Type u_1
β : Type ?u.208128
f g : Perm α
p : α → Prop
x z : α
inst✝ : Finite α
k : ℤ
h₀ : 0 < ↑(orderOf f)
h₁ : 0 ≤ k % ↑(orderOf f)
⊢ Int.natAbs (k % ↑(orderOf f)) < orderOf f ∧ ↑(f ^ Int.natAbs (k % ↑(orderOf f))) x = ↑(f ^ k) x
case intro
ι : Type ?u.208122
α : Type u_1
β : Type ?u.208128
f g : Perm α
p : α → Prop
x z : α
inst✝ : Finite α
k : ℤ
h₀ : 0 < ↑(orderOf f)
⊢ Int.natAbs (k % ↑(orderOf f)) < orderOf f ∧ ↑(f ^ Int.natAbs (k % ↑(orderOf f))) x = ↑(f ^ k) x
have h₁ := Int.emod_nonneg k h₀.ne'
case intro
ι : Type ?u.208122
α : Type u_1
β : Type ?u.208128
f g : Perm α
p : α → Prop
x z : α
inst✝ : Finite α
k : ℤ
h₀ : 0 < ↑(orderOf f)
h₁ : 0 ≤ k % ↑(orderOf f)
⊢ Int.natAbs (k % ↑(orderOf f)) < orderOf f ∧ ↑(f ^ k) x = ↑(f ^ k) x
case intro
ι : Type ?u.208122
α : Type u_1
β : Type ?u.208128
f g : Perm α
p : α → Prop
x z : α
inst✝ : Finite α
k : ℤ
h₀ : 0 < ↑(orderOf f)
h₁ : 0 ≤ k % ↑(orderOf f)
⊢ Int.natAbs (k % ↑(orderOf f)) < orderOf f ∧ ↑(f ^ Int.natAbs (k % ↑(orderOf f))) x = ↑(f ^ k) x
rw [← zpow_ofNat, Int.natAbs_of_nonneg h₁, ← zpow_eq_mod_orderOf]
case intro
ι : Type ?u.208122
α : Type u_1
β : Type ?u.208128
f g : Perm α
p : α → Prop
x z : α
inst✝ : Finite α
k : ℤ
h₀ : 0 < ↑(orderOf f)
h₁ : 0 ≤ k % ↑(orderOf f)
⊢ Int.natAbs (k % ↑(orderOf f)) < orderOf f
case intro
ι : Type ?u.208122
α : Type u_1
β : Type ?u.208128
f g : Perm α
p : α → Prop
x z : α
inst✝ : Finite α
k : ℤ
h₀ : 0 < ↑(orderOf f)
h₁ : 0 ≤ k % ↑(orderOf f)
⊢ Int.natAbs (k % ↑(orderOf f)) < orderOf f ∧ ↑(f ^ k) x = ↑(f ^ k) x
refine' ⟨_, by rfl⟩
case intro
ι : Type ?u.208122
α : Type u_1
β : Type ?u.208128
f g : Perm α
p : α → Prop
x z : α
inst✝ : Finite α
k : ℤ
h₀ : 0 < ↑(orderOf f)
h₁ : 0 ≤ k % ↑(orderOf f)
⊢ k % ↑(orderOf f) < ↑(orderOf f)
case intro
ι : Type ?u.208122
α : Type u_1
β : Type ?u.208128
f g : Perm α
p : α → Prop
x z : α
inst✝ : Finite α
k : ℤ
h₀ : 0 < ↑(orderOf f)
h₁ : 0 ≤ k % ↑(orderOf f)
⊢ Int.natAbs (k % ↑(orderOf f)) < orderOf f
rw [← Int.ofNat_lt, Int.natAbs_of_nonneg h₁]
no goals
case intro
ι : Type ?u.208122
α : Type u_1
β : Type ?u.208128
f g : Perm α
p : α → Prop
x z : α
inst✝ : Finite α
k : ℤ
h₀ : 0 < ↑(orderOf f)
h₁ : 0 ≤ k % ↑(orderOf f)
⊢ k % ↑(orderOf f) < ↑(orderOf f)
exact Int.emod_lt_of_pos _ h₀
no goals
ι : Type ?u.208122
α : Type u_1
β : Type ?u.208128
f g : Perm α
p : α → Prop
x z : α
inst✝ : Finite α
k : ℤ
h₀ : 0 < ↑(orderOf f)
h₁ : 0 ≤ k % ↑(orderOf f)
⊢ ↑(f ^ k) x = ↑(f ^ k) x
rfl