case hl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
k : ℕ
⊢ length (toList p (↑(p ^ k) x)) = length (rotate (toList p x) k)

case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
k : ℕ
⊢ ∀ (n : ℕ) (h₁ : n < length (toList p (↑(p ^ k) x))) (h₂ : n < length (rotate (toList p x) k)),
    nthLe (toList p (↑(p ^ k) x)) n h₁ = nthLe (rotate (toList p x) k) n h₂
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
k : ℕ
⊢ toList p (↑(p ^ k) x) = rotate (toList p x) k
apply ext_nthLe
no goals
case hl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
k : ℕ
⊢ length (toList p (↑(p ^ k) x)) = length (rotate (toList p x) k)
simp only [length_toList, cycleOf_self_apply_pow, length_rotate]
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
k n : ℕ
hn : n < length (toList p (↑(p ^ k) x))
hn' : n < length (rotate (toList p x) k)
⊢ nthLe (toList p (↑(p ^ k) x)) n hn = nthLe (rotate (toList p x) k) n hn'
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
k : ℕ
⊢ ∀ (n : ℕ) (h₁ : n < length (toList p (↑(p ^ k) x))) (h₂ : n < length (rotate (toList p x) k)),
    nthLe (toList p (↑(p ^ k) x)) n h₁ = nthLe (rotate (toList p x) k) n h₂
intro n hn hn'
no goals
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x : α
k n : ℕ
hn : n < length (toList p (↑(p ^ k) x))
hn' : n < length (rotate (toList p x) k)
⊢ nthLe (toList p (↑(p ^ k) x)) n hn = nthLe (rotate (toList p x) k) n hn'
rw [nthLe_toList, nthLe_rotate, nthLe_toList, length_toList,
  pow_mod_card_support_cycleOf_self_apply, pow_add, mul_apply]