-- Mathlib/GroupTheory/Perm/List.lean
theorem formPerm_rotate_one (l : List α) (h : Nodup l) : formPerm (l.rotate 1) = formPerm l

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
x : α
hx : x ∈ l.rotate 1
⊢ (l.rotate 1).formPerm x = l.formPerm x

Tactic:
obtain ⟨k, hk, rfl⟩ := getElem_of_mem hx

Result:
case pos.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
k : ℕ
hk : k < (l.rotate 1).length
hx : (l.rotate 1)[k] ∈ l.rotate 1
⊢ (l.rotate 1).formPerm (l.rotate 1)[k] = l.formPerm (l.rotate 1)[k]

Proof state:
case pos.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
k : ℕ
hk : k < (l.rotate 1).length
hx : (l.rotate 1)[k] ∈ l.rotate 1
⊢ (l.rotate 1).formPerm (l.rotate 1)[k] = l.formPerm (l.rotate 1)[k]

Tactic:
rw [formPerm_apply_getElem _ h', getElem_rotate l, getElem_rotate l, formPerm_apply_getElem _ h]

Result:
case pos.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
k : ℕ
hk : k < (l.rotate 1).length
hx : (l.rotate 1)[k] ∈ l.rotate 1
⊢ l[((k + 1) % (l.rotate 1).length + 1) % l.length] = l[((k + 1) % l.length + 1) % l.length]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
⊢ (l.rotate 1).formPerm = l.formPerm

Tactic:
have h' : Nodup (l.rotate 1) := by simpa using h

Result:
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
⊢ (l.rotate 1).formPerm = l.formPerm

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
⊢ (l.rotate 1).Nodup

Tactic:
simpa using h

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
x : α
hx : x ∉ l.rotate 1
⊢ x ∉ l

Tactic:
simpa using hx

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
⊢ (l.rotate 1).formPerm = l.formPerm

Tactic:
ext x

Result:
case H
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
x : α
⊢ (l.rotate 1).formPerm x = l.formPerm x

Proof state:
case pos.intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
k : ℕ
hk : k < (l.rotate 1).length
hx : (l.rotate 1)[k] ∈ l.rotate 1
⊢ l[((k + 1) % (l.rotate 1).length + 1) % l.length] = l[((k + 1) % l.length + 1) % l.length]

Tactic:
simp

Result:
no goals

Proof state:
case H
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
x : α
⊢ (l.rotate 1).formPerm x = l.formPerm x

Tactic:
by_cases hx : x ∈ l.rotate 1

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
x : α
hx : x ∈ l.rotate 1
⊢ (l.rotate 1).formPerm x = l.formPerm x

case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
x : α
hx : x ∉ l.rotate 1
⊢ (l.rotate 1).formPerm x = l.formPerm x

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
x : α
hx : x ∉ l.rotate 1
⊢ (l.rotate 1).formPerm x = l.formPerm x

Tactic:
rw [formPerm_apply_of_not_mem hx, formPerm_apply_of_not_mem]

Result:
case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
x : α
hx : x ∉ l.rotate 1
⊢ x ∉ l