α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x y : α
hy✝ : y ∈ toList p x
hy : SameCycle p x y ∧ x ∈ support p
⊢ next (toList p x) y hy✝ = ↑p y
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x y : α
hy : y ∈ toList p x
⊢ next (toList p x) y hy = ↑p y
rw [mem_toList_iff] at hy
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x y : α
hy✝ : y ∈ toList p x
hy : SameCycle p x y ∧ x ∈ support p
k : ℕ
hk : k < Finset.card (support (cycleOf p x))
hk' : ↑(p ^ k) x = y
⊢ next (toList p x) y hy✝ = ↑p y
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x y : α
hy✝ : y ∈ toList p x
hy : SameCycle p x y ∧ x ∈ support p
⊢ next (toList p x) y hy✝ = ↑p y
obtain ⟨k, hk, hk'⟩ := hy.left.exists_pow_eq_of_mem_support hy.right
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x y : α
hy✝ : y ∈ toList p x
hy : SameCycle p x y ∧ x ∈ support p
k : ℕ
hk : k < Finset.card (support (cycleOf p x))
hk'✝ : ↑(p ^ k) x = y
hk' : nthLe (toList p x) k (_ : k < length (toList p x)) = y
⊢ next (toList p x) y hy✝ = ↑p y
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x y : α
hy✝ : y ∈ toList p x
hy : SameCycle p x y ∧ x ∈ support p
k : ℕ
hk : k < Finset.card (support (cycleOf p x))
hk' : ↑(p ^ k) x = y
⊢ next (toList p x) y hy✝ = ↑p y
rw [← nthLe_toList p x k (by simpa using hk)] at hk'
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x y : α
hy✝ : y ∈ toList p x
hy : SameCycle p x y ∧ x ∈ support p
k : ℕ
hk : k < Finset.card (support (cycleOf p x))
hk'✝ : ↑(p ^ k) x = y
hk' : nthLe (toList p x) k (_ : k < length (toList p x)) = y
⊢ next (toList p x) (nthLe (toList p x) k (_ : k < length (toList p x)))
      (_ : nthLe (toList p x) k (_ : k < length (toList p x)) ∈ toList p x) =
    ↑p (nthLe (toList p x) k (_ : k < length (toList p x)))
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x y : α
hy✝ : y ∈ toList p x
hy : SameCycle p x y ∧ x ∈ support p
k : ℕ
hk : k < Finset.card (support (cycleOf p x))
hk'✝ : ↑(p ^ k) x = y
hk' : nthLe (toList p x) k (_ : k < length (toList p x)) = y
⊢ next (toList p x) y hy✝ = ↑p y
simp_rw [← hk']
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x y : α
hy✝ : y ∈ toList p x
hy : SameCycle p x y ∧ x ∈ support p
k : ℕ
hk : k < Finset.card (support (cycleOf p x))
hk'✝ : ↑(p ^ k) x = y
hk' : nthLe (toList p x) k (_ : k < length (toList p x)) = y
⊢ IsCycle (cycleOf p x)
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x y : α
hy✝ : y ∈ toList p x
hy : SameCycle p x y ∧ x ∈ support p
k : ℕ
hk : k < Finset.card (support (cycleOf p x))
hk'✝ : ↑(p ^ k) x = y
hk' : nthLe (toList p x) k (_ : k < length (toList p x)) = y
⊢ next (toList p x) (nthLe (toList p x) k (_ : k < length (toList p x)))
      (_ : nthLe (toList p x) k (_ : k < length (toList p x)) ∈ toList p x) =
    ↑p (nthLe (toList p x) k (_ : k < length (toList p x)))
rw [next_nthLe _ (nodup_toList _ _), nthLe_toList, nthLe_toList, ← mul_apply, ← pow_succ,
  length_toList, pow_apply_eq_pow_mod_orderOf_cycleOf_apply p (k + 1), IsCycle.orderOf]
no goals
case intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x y : α
hy✝ : y ∈ toList p x
hy : SameCycle p x y ∧ x ∈ support p
k : ℕ
hk : k < Finset.card (support (cycleOf p x))
hk'✝ : ↑(p ^ k) x = y
hk' : nthLe (toList p x) k (_ : k < length (toList p x)) = y
⊢ IsCycle (cycleOf p x)
exact isCycle_cycleOf _ (mem_support.mp hy.right)
no goals
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p✝ : Perm α
x✝ : α
p : Perm α
x y : α
hy✝ : y ∈ toList p x
hy : SameCycle p x y ∧ x ∈ support p
k : ℕ
hk : k < Finset.card (support (cycleOf p x))
hk' : ↑(p ^ k) x = y
⊢ k < length (toList p x)
simpa using hk