α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
hc : IsCycle (formPerm l)
⊢ toList (formPerm l) (nthLe l 0 (_ : 0 < length l)) = l
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
⊢ toList (formPerm l) (nthLe l 0 (_ : 0 < length l)) = l
have hc : l.formPerm.IsCycle := List.isCycle_formPerm hn hl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
hc : IsCycle (formPerm l)
hs : support (formPerm l) = toFinset l
⊢ toList (formPerm l) (nthLe l 0 (_ : 0 < length l)) = l
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
hc : IsCycle (formPerm l)
⊢ toList (formPerm l) (nthLe l 0 (_ : 0 < length l)) = l
have hs : l.formPerm.support = l.toFinset := by
  refine' support_formPerm_of_nodup _ hn _
  rintro _ rfl
  simp [Nat.succ_le_succ_iff] at hl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
hc : IsCycle (formPerm l)
hs : support (formPerm l) = toFinset l
⊢ map (fun k => ↑(formPerm l ^ k) (nthLe l 0 (_ : 0 < length l))) (range (length l)) = l

α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
hc : IsCycle (formPerm l)
hs : support (formPerm l) = toFinset l
⊢ nthLe l 0 (_ : 0 < length l) ∈ support (formPerm l)
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
hc : IsCycle (formPerm l)
hs : support (formPerm l) = toFinset l
⊢ toList (formPerm l) (nthLe l 0 (_ : 0 < length l)) = l
rw [toList, hc.cycleOf_eq (mem_support.mp _), hs, card_toFinset, dedup_eq_self.mpr hn]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
hc : IsCycle (formPerm l)
⊢ ∀ (x : α), l ≠ [x]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
hc : IsCycle (formPerm l)
⊢ support (formPerm l) = toFinset l
refine' support_formPerm_of_nodup _ hn _
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x x✝ : α
hl : 2 ≤ length [x✝]
hn : Nodup [x✝]
hc : IsCycle (formPerm [x✝])
⊢ False
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
hc : IsCycle (formPerm l)
⊢ ∀ (x : α), l ≠ [x]
rintro _ rfl
no goals
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x x✝ : α
hl : 2 ≤ length [x✝]
hn : Nodup [x✝]
hc : IsCycle (formPerm [x✝])
⊢ False
simp [Nat.succ_le_succ_iff] at hl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
hc : IsCycle (formPerm l)
hs : support (formPerm l) = toFinset l
k : ℕ
hk : k < length (map (fun k => ↑(formPerm l ^ k) (nthLe l 0 (_ : 0 < length l))) (range (length l)))
hk' : k < length l
⊢ List.get (map (fun k => ↑(formPerm l ^ k) (nthLe l 0 (_ : 0 < length l))) (range (length l)))
      { val := k, isLt := hk } =
    List.get l { val := k, isLt := hk' }
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
hc : IsCycle (formPerm l)
hs : support (formPerm l) = toFinset l
⊢ map (fun k => ↑(formPerm l ^ k) (nthLe l 0 (_ : 0 < length l))) (range (length l)) = l
refine' ext_get (by simp) fun k hk hk' => _
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
hc : IsCycle (formPerm l)
hs : support (formPerm l) = toFinset l
k : ℕ
hk : k < length (map (fun k => ↑(formPerm l ^ k) (nthLe l 0 (_ : 0 < length l))) (range (length l)))
hk' : k < length l
⊢ nthLe l k (_ : k < length l) = List.get l { val := k, isLt := hk' }
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
hc : IsCycle (formPerm l)
hs : support (formPerm l) = toFinset l
k : ℕ
hk : k < length (map (fun k => ↑(formPerm l ^ k) (nthLe l 0 (_ : 0 < length l))) (range (length l)))
hk' : k < length l
⊢ List.get (map (fun k => ↑(formPerm l ^ k) (nthLe l 0 (_ : 0 < length l))) (range (length l)))
      { val := k, isLt := hk } =
    List.get l { val := k, isLt := hk' }
simp [formPerm_pow_apply_nthLe _ hn, Nat.mod_eq_of_lt hk']
no goals
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
hc : IsCycle (formPerm l)
hs : support (formPerm l) = toFinset l
k : ℕ
hk : k < length (map (fun k => ↑(formPerm l ^ k) (nthLe l 0 (_ : 0 < length l))) (range (length l)))
hk' : k < length l
⊢ nthLe l k (_ : k < length l) = List.get l { val := k, isLt := hk' }
rw [nthLe_eq]
no goals
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
hc : IsCycle (formPerm l)
hs : support (formPerm l) = toFinset l
⊢ length (map (fun k => ↑(formPerm l ^ k) (nthLe l 0 (_ : 0 < length l))) (range (length l))) = length l
simp
no goals
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
hc : IsCycle (formPerm l)
hs : support (formPerm l) = toFinset l
⊢ nthLe l 0 (_ : 0 < length l) ∈ support (formPerm l)
simpa [hs] using get_mem _ _ _