-- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean
theorem toList_formPerm_nontrivial (l : List α) (hl : 2 ≤ l.length) (hn : Nodup l) :
    toList (formPerm l) (l.get ⟨0, (zero_lt_two.trans_le hl)⟩) = l

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
⊢ l.formPerm.toList (l.get ⟨0, ⋯⟩) = l

Tactic:
have hc : l.formPerm.IsCycle := List.isCycle_formPerm hn hl

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
hc : l.formPerm.IsCycle
⊢ l.formPerm.toList (l.get ⟨0, ⋯⟩) = l

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
hc : l.formPerm.IsCycle
hs : l.formPerm.support = l.toFinset
⊢ l.formPerm.toList (l.get ⟨0, ⋯⟩) = l

Tactic:
rw [toList, hc.cycleOf_eq (mem_support.mp _), hs, card_toFinset, dedup_eq_self.mpr hn]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
hc : l.formPerm.IsCycle
hs : l.formPerm.support = l.toFinset
⊢ iterate (⇑l.formPerm) (l.get ⟨0, ⋯⟩) l.length = l

α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
hc : l.formPerm.IsCycle
hs : l.formPerm.support = l.toFinset
⊢ l.get ⟨0, ⋯⟩ ∈ l.formPerm.support

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
hc : l.formPerm.IsCycle
hs : l.formPerm.support = l.toFinset
⊢ (iterate (⇑l.formPerm) (l.get ⟨0, ⋯⟩) l.length).length = l.length

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
hc : l.formPerm.IsCycle
hs : l.formPerm.support = l.toFinset
k : ℕ
hk : k < (iterate (⇑l.formPerm) (l.get ⟨0, ⋯⟩) l.length).length
hk' : k < l.length
⊢ (iterate (⇑l.formPerm) (l.get ⟨0, ⋯⟩) l.length)[k] = l[k]

Tactic:
simp only [get_eq_getElem, getElem_iterate, iterate_eq_pow, formPerm_pow_apply_getElem _ hn,
  zero_add, Nat.mod_eq_of_lt hk']

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
hc : l.formPerm.IsCycle
hs : l.formPerm.support = l.toFinset
⊢ iterate (⇑l.formPerm) (l.get ⟨0, ⋯⟩) l.length = l

Tactic:
refine ext_getElem (by simp) fun k hk hk' => ?_

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
hc : l.formPerm.IsCycle
hs : l.formPerm.support = l.toFinset
k : ℕ
hk : k < (iterate (⇑l.formPerm) (l.get ⟨0, ⋯⟩) l.length).length
hk' : k < l.length
⊢ (iterate (⇑l.formPerm) (l.get ⟨0, ⋯⟩) l.length)[k] = l[k]

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
hc : l.formPerm.IsCycle
⊢ l.formPerm.support = l.toFinset

Tactic:
refine support_formPerm_of_nodup _ hn ?_

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
hc : l.formPerm.IsCycle
⊢ ∀ (x : α), l ≠ [x]

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
hc : l.formPerm.IsCycle
⊢ ∀ (x : α), l ≠ [x]

Tactic:
rintro _ rfl

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x✝ : α
hl : 2 ≤ [x✝].length
hn : [x✝].Nodup
hc : [x✝].formPerm.IsCycle
⊢ False

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
hc : l.formPerm.IsCycle
⊢ l.formPerm.toList (l.get ⟨0, ⋯⟩) = l

Tactic:
have hs : l.formPerm.support = l.toFinset := by
  refine support_formPerm_of_nodup _ hn ?_
  rintro _ rfl
  simp [Nat.succ_le_succ_iff] at hl

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
hc : l.formPerm.IsCycle
hs : l.formPerm.support = l.toFinset
⊢ l.formPerm.toList (l.get ⟨0, ⋯⟩) = l

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x✝ : α
hl : 2 ≤ [x✝].length
hn : [x✝].Nodup
hc : [x✝].formPerm.IsCycle
⊢ False

Tactic:
simp [Nat.succ_le_succ_iff] at hl

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List α
hl : 2 ≤ l.length
hn : l.Nodup
hc : l.formPerm.IsCycle
hs : l.formPerm.support = l.toFinset
⊢ l.get ⟨0, ⋯⟩ ∈ l.formPerm.support

Tactic:
simp [hs]

Result:
no goals