α : Type u_1
β : Type ?u.770921
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
h' : Nodup (rotate l 1)
⊢ formPerm (rotate l 1) = formPerm l
α : Type u_1
β : Type ?u.770921
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
⊢ formPerm (rotate l 1) = formPerm l
have h' : Nodup (l.rotate 1) := by simpa using h
case H
α : Type u_1
β : Type ?u.770921
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
h' : Nodup (rotate l 1)
x : α
⊢ ↑(formPerm (rotate l 1)) x = ↑(formPerm l) x
α : Type u_1
β : Type ?u.770921
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
h' : Nodup (rotate l 1)
⊢ formPerm (rotate l 1) = formPerm l
ext x
case pos
α : Type u_1
β : Type ?u.770921
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
h' : Nodup (rotate l 1)
x : α
hx : x ∈ rotate l 1
⊢ ↑(formPerm (rotate l 1)) x = ↑(formPerm l) x

case neg
α : Type u_1
β : Type ?u.770921
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
h' : Nodup (rotate l 1)
x : α
hx : ¬x ∈ rotate l 1
⊢ ↑(formPerm (rotate l 1)) x = ↑(formPerm l) x
case H
α : Type u_1
β : Type ?u.770921
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
h' : Nodup (rotate l 1)
x : α
⊢ ↑(formPerm (rotate l 1)) x = ↑(formPerm l) x
by_cases hx : x ∈ l.rotate 1
no goals
α : Type u_1
β : Type ?u.770921
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
⊢ Nodup (rotate l 1)
simpa using h
case pos.intro.intro
α : Type u_1
β : Type ?u.770921
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
h' : Nodup (rotate l 1)
k : ℕ
hk : k < length (rotate l 1)
hx : nthLe (rotate l 1) k hk ∈ rotate l 1
⊢ ↑(formPerm (rotate l 1)) (nthLe (rotate l 1) k hk) = ↑(formPerm l) (nthLe (rotate l 1) k hk)
case pos
α : Type u_1
β : Type ?u.770921
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
h' : Nodup (rotate l 1)
x : α
hx : x ∈ rotate l 1
⊢ ↑(formPerm (rotate l 1)) x = ↑(formPerm l) x
obtain ⟨k, hk, rfl⟩ := nthLe_of_mem hx
case pos.intro.intro
α : Type u_1
β : Type ?u.770921
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
h' : Nodup (rotate l 1)
k : ℕ
hk : k < length (rotate l 1)
hx : nthLe (rotate l 1) k hk ∈ rotate l 1
⊢ nthLe l (((k + 1) % length (rotate l 1) + 1) % length l)
      (_ : ((k + 1) % length (rotate l 1) + 1) % length l < length l) =
    nthLe l (((k + 1) % length l + 1) % length l) (_ : ((k + 1) % length l + 1) % length l < length l)
case pos.intro.intro
α : Type u_1
β : Type ?u.770921
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
h' : Nodup (rotate l 1)
k : ℕ
hk : k < length (rotate l 1)
hx : nthLe (rotate l 1) k hk ∈ rotate l 1
⊢ ↑(formPerm (rotate l 1)) (nthLe (rotate l 1) k hk) = ↑(formPerm l) (nthLe (rotate l 1) k hk)
rw [formPerm_apply_nthLe _ h', nthLe_rotate l, nthLe_rotate l, formPerm_apply_nthLe _ h]
no goals
case pos.intro.intro
α : Type u_1
β : Type ?u.770921
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
h' : Nodup (rotate l 1)
k : ℕ
hk : k < length (rotate l 1)
hx : nthLe (rotate l 1) k hk ∈ rotate l 1
⊢ nthLe l (((k + 1) % length (rotate l 1) + 1) % length l)
      (_ : ((k + 1) % length (rotate l 1) + 1) % length l < length l) =
    nthLe l (((k + 1) % length l + 1) % length l) (_ : ((k + 1) % length l + 1) % length l < length l)
simp
case neg.h
α : Type u_1
β : Type ?u.770921
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
h' : Nodup (rotate l 1)
x : α
hx : ¬x ∈ rotate l 1
⊢ ¬x ∈ l
case neg
α : Type u_1
β : Type ?u.770921
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
h' : Nodup (rotate l 1)
x : α
hx : ¬x ∈ rotate l 1
⊢ ↑(formPerm (rotate l 1)) x = ↑(formPerm l) x
rw [formPerm_apply_of_not_mem _ _ hx, formPerm_apply_of_not_mem]
no goals
case neg.h
α : Type u_1
β : Type ?u.770921
inst✝ : DecidableEq α
l✝ : List α
x✝ : α
l : List α
h : Nodup l
h' : Nodup (rotate l 1)
x : α
hx : ¬x ∈ rotate l 1
⊢ ¬x ∈ l
simpa using hx