case intro.refl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
k : Fin (length l)
hx : List.get l k ∈ l
⊢ toList (formPerm l) (List.get l k) ~r l
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x✝ : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
x : α
hx : x ∈ l
⊢ toList (formPerm l) x ~r l
obtain ⟨k, hk, rfl⟩ := get_of_mem hx
case intro.refl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
k : Fin (length l)
hx : List.get l k ∈ l
hr : l ~r rotate l ↑k
⊢ toList (formPerm l) (List.get l k) ~r l
case intro.refl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
k : Fin (length l)
hx : List.get l k ∈ l
⊢ toList (formPerm l) (List.get l k) ~r l
have hr : l ~r l.rotate k := ⟨k, rfl⟩
case intro.refl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
k : Fin (length l)
hx : List.get l k ∈ l
hr : l ~r rotate l ↑k
⊢ toList (formPerm (rotate l ↑k)) (List.get l k) ~r l
case intro.refl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
k : Fin (length l)
hx : List.get l k ∈ l
hr : l ~r rotate l ↑k
⊢ toList (formPerm l) (List.get l k) ~r l
rw [formPerm_eq_of_isRotated hn hr]
case intro.refl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
k : Fin (length l)
hx : List.get l k ∈ l
hr : l ~r rotate l ↑k
⊢ toList (formPerm (rotate l ↑k))
      (List.get (rotate l ↑k)
        { val := (length l - ↑k % length l + ↑k) % length l,
          isLt := (_ : (length l - ↑k % length l + ↑k) % length l < length (rotate l ↑k)) }) ~r
    l
case intro.refl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
k : Fin (length l)
hx : List.get l k ∈ l
hr : l ~r rotate l ↑k
⊢ toList (formPerm (rotate l ↑k)) (List.get l k) ~r l
rw [get_eq_get_rotate l k k]
case intro.refl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
k : Fin (length l)
hx : List.get l k ∈ l
hr : l ~r rotate l ↑k
⊢ toList (formPerm (rotate l ↑k)) (List.get (rotate l ↑k) { val := 0, isLt := (_ : 0 < length (rotate l ↑k)) }) ~r l
case intro.refl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
k : Fin (length l)
hx : List.get l k ∈ l
hr : l ~r rotate l ↑k
⊢ toList (formPerm (rotate l ↑k))
      (List.get (rotate l ↑k)
        { val := (length l - ↑k % length l + ↑k) % length l,
          isLt := (_ : (length l - ↑k % length l + ↑k) % length l < length (rotate l ↑k)) }) ~r
    l
simp only [Nat.mod_eq_of_lt k.2, tsub_add_cancel_of_le (le_of_lt k.2), Nat.mod_self]
case intro.refl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
k : Fin (length l)
hx : List.get l k ∈ l
hr : l ~r rotate l ↑k
⊢ rotate l ↑k ~r l

case intro.refl.hl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
k : Fin (length l)
hx : List.get l k ∈ l
hr : l ~r rotate l ↑k
⊢ 2 ≤ length (rotate l ↑k)

case intro.refl.hn
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
k : Fin (length l)
hx : List.get l k ∈ l
hr : l ~r rotate l ↑k
⊢ Nodup (rotate l ↑k)
case intro.refl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
k : Fin (length l)
hx : List.get l k ∈ l
hr : l ~r rotate l ↑k
⊢ toList (formPerm (rotate l ↑k)) (List.get (rotate l ↑k) { val := 0, isLt := (_ : 0 < length (rotate l ↑k)) }) ~r l
erw [toList_formPerm_nontrivial]
no goals
case intro.refl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
k : Fin (length l)
hx : List.get l k ∈ l
hr : l ~r rotate l ↑k
⊢ rotate l ↑k ~r l
simp
no goals
case intro.refl.hl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
k : Fin (length l)
hx : List.get l k ∈ l
hr : l ~r rotate l ↑k
⊢ 2 ≤ length (rotate l ↑k)
simpa using hl
no goals
case intro.refl.hn
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
l : List α
hl : 2 ≤ length l
hn : Nodup l
k : Fin (length l)
hx : List.get l k ∈ l
hr : l ~r rotate l ↑k
⊢ Nodup (rotate l ↑k)
simpa using hn