-- Mathlib/GroupTheory/Perm/List.lean
theorem formPerm_apply_lt_getElem (xs : List α) (h : Nodup xs) (n : ℕ) (hn : n + 1 < xs.length) :
    formPerm xs xs[n] = xs[n + 1]

Proof state:
case succ.cons.cons.a
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH✝ : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
IH : (y :: l).formPerm (y :: l)[n] = l[n]
⊢ (y :: l).formPerm (y :: l)[n] ≠ y

Tactic:
intro hx

Result:
case succ.cons.cons.a
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH✝ : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
IH : (y :: l).formPerm (y :: l)[n] = l[n]
hx : (y :: l).formPerm (y :: l)[n] = y
⊢ False

Proof state:
case succ.cons.cons.a
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH✝ : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
IH : (y :: l).formPerm (y :: l)[n] = l[n]
hx : (y :: l).formPerm (y :: l)[n] = y
⊢ False

Tactic:
rw [← hx, IH] at h

Result:
case succ.cons.cons.a
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH✝ : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x y : α
l : List α
hn : n + 1 + 1 < (x :: y :: l).length
h : (x :: l[n] :: l).Nodup
IH : (y :: l).formPerm (y :: l)[n] = l[n]
hx : (y :: l).formPerm (y :: l)[n] = y
⊢ False

Proof state:
case succ.cons.cons
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH✝ : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
IH : (y :: l).formPerm (y :: l)[n] = (y :: l)[n + 1]
⊢ (y :: l).formPerm (x :: y :: l)[n + 1] = (swap x y) (x :: y :: l)[n + 1 + 1]

Tactic:
simp only [getElem_cons_succ] at *

Result:
case succ.cons.cons
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH✝ : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
IH : (y :: l).formPerm (y :: l)[n] = l[n]
⊢ (y :: l).formPerm (y :: l)[n] = (swap x y) l[n]

Proof state:
case succ.cons.cons.a
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH✝ : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x y : α
l : List α
hn : n + 1 + 1 < (x :: y :: l).length
h : (x :: l[n] :: l).Nodup
IH : (y :: l).formPerm (y :: l)[n] = l[n]
hx : (y :: l).formPerm (y :: l)[n] = y
⊢ False

Tactic:
simp [getElem_mem] at h

Result:
no goals

Proof state:
case succ.cons.cons
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
⊢ (x :: y :: l).formPerm (x :: y :: l)[n + 1] = (x :: y :: l)[n + 1 + 1]

Tactic:
specialize IH (y :: l) h.of_cons _

Result:
case succ.cons.cons
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
⊢ n + 1 < (y :: l).length

case succ.cons.cons
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH✝ : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
IH : (y :: l).formPerm (y :: l)[n] = (y :: l)[n + 1]
⊢ (x :: y :: l).formPerm (x :: y :: l)[n + 1] = (x :: y :: l)[n + 1 + 1]

Proof state:
case zero
α : Type u_1
inst✝ : DecidableEq α
xs : List α
h : xs.Nodup
hn : 0 + 1 < xs.length
⊢ xs.formPerm xs[0] = xs[0 + 1]

Tactic:
simpa using formPerm_apply_getElem_zero _ h _

Result:
no goals

Proof state:
case succ.cons.nil
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x : α
h : [x].Nodup
hn : n + 1 + 1 < [x].length
⊢ [x].formPerm [x][n + 1] = [x][n + 1 + 1]

Tactic:
rw [formPerm_singleton, getElem_singleton, getElem_singleton, one_apply]

Result:
no goals

Proof state:
case succ
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
xs : List α
h : xs.Nodup
hn : n + 1 + 1 < xs.length
⊢ xs.formPerm xs[n + 1] = xs[n + 1 + 1]

Tactic:
rcases xs with (_ | ⟨x, _ | ⟨y, l⟩⟩)

Result:
case succ.nil
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
h : [].Nodup
hn : n + 1 + 1 < [].length
⊢ [].formPerm [][n + 1] = [][n + 1 + 1]

case succ.cons.nil
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x : α
h : [x].Nodup
hn : n + 1 + 1 < [x].length
⊢ [x].formPerm [x][n + 1] = [x][n + 1 + 1]

case succ.cons.cons
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
⊢ (x :: y :: l).formPerm (x :: y :: l)[n + 1] = (x :: y :: l)[n + 1 + 1]

Proof state:
case succ.cons.cons
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
⊢ n + 1 < (y :: l).length

Tactic:
simpa [Nat.succ_lt_succ_iff] using hn

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
xs : List α
h : xs.Nodup
n : ℕ
hn : n + 1 < xs.length
⊢ xs.formPerm xs[n] = xs[n + 1]

Tactic:
induction' n with n IH generalizing xs

Result:
case zero
α : Type u_1
inst✝ : DecidableEq α
xs : List α
h : xs.Nodup
hn : 0 + 1 < xs.length
⊢ xs.formPerm xs[0] = xs[0 + 1]

case succ
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
xs : List α
h : xs.Nodup
hn : n + 1 + 1 < xs.length
⊢ xs.formPerm xs[n + 1] = xs[n + 1 + 1]

Proof state:
case succ.nil
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
h : [].Nodup
hn : n + 1 + 1 < [].length
⊢ [].formPerm [][n + 1] = [][n + 1 + 1]

Tactic:
simp at hn

Result:
no goals

Proof state:
case succ.cons.cons
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH✝ : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
IH : (y :: l).formPerm (y :: l)[n] = (y :: l)[n + 1]
⊢ (x :: y :: l).formPerm (x :: y :: l)[n + 1] = (x :: y :: l)[n + 1 + 1]

Tactic:
simp only [swap_apply_eq_iff, coe_mul, formPerm_cons_cons, Function.comp]

Result:
case succ.cons.cons
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH✝ : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
IH : (y :: l).formPerm (y :: l)[n] = (y :: l)[n + 1]
⊢ (y :: l).formPerm (x :: y :: l)[n + 1] = (swap x y) (x :: y :: l)[n + 1 + 1]