-- Mathlib/GroupTheory/Perm/List.lean
theorem formPerm_apply_getElem (xs : List α) (w : Nodup xs) (i : ℕ) (h : i < xs.length) :
    formPerm xs xs[i] =
      xs[(i + 1) % xs.length]'(Nat.mod_lt _ (i.zero_le.trans_lt h))

Proof state:
α : Type u_1
inst✝ : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
⊢ i < xs.length.succ

Tactic:
simpa using h

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
this : i ≤ xs.length
⊢ (x :: xs).formPerm (x :: xs)[i] = (x :: xs)[(i + 1) % (x :: xs).length]

Tactic:
rcases this.eq_or_lt with (rfl | hn')

Result:
case cons.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
w : (x :: xs).Nodup
h : xs.length < (x :: xs).length
this : xs.length ≤ xs.length
⊢ (x :: xs).formPerm (x :: xs)[xs.length] = (x :: xs)[(xs.length + 1) % (x :: xs).length]

case cons.inr
α : Type u_1
inst✝ : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
this : i ≤ xs.length
hn' : i < xs.length
⊢ (x :: xs).formPerm (x :: xs)[i] = (x :: xs)[(i + 1) % (x :: xs).length]

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
⊢ (x :: xs).formPerm (x :: xs)[i] = (x :: xs)[(i + 1) % (x :: xs).length]

Tactic:
have : i ≤ xs.length := by
  refine Nat.le_of_lt_succ ?_
  simpa using h

Result:
case cons
α : Type u_1
inst✝ : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
this : i ≤ xs.length
⊢ (x :: xs).formPerm (x :: xs)[i] = (x :: xs)[(i + 1) % (x :: xs).length]

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
i : ℕ
w : [].Nodup
h : i < [].length
⊢ [].formPerm [][i] = [][(i + 1) % [].length]

Tactic:
simp at h

Result:
no goals

Proof state:
case cons.inr
α : Type u_1
inst✝ : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
this : i ≤ xs.length
hn' : i < xs.length
⊢ (x :: xs)[i + 1] = (x :: xs)[(i + 1) % (x :: xs).length]

Tactic:
congr

Result:
case cons.inr.e_i
α : Type u_1
inst✝ : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
this : i ≤ xs.length
hn' : i < xs.length
⊢ i + 1 = (i + 1) % (x :: xs).length

Proof state:
case cons.inr.e_i
α : Type u_1
inst✝ : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
this : i ≤ xs.length
hn' : i < xs.length
⊢ i + 1 = (i + 1) % (x :: xs).length

Tactic:
rw [Nat.mod_eq_of_lt]

Result:
case cons.inr.e_i
α : Type u_1
inst✝ : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
this : i ≤ xs.length
hn' : i < xs.length
⊢ i + 1 < (x :: xs).length

Proof state:
α : Type u_1
inst✝ : DecidableEq α
xs : List α
w : xs.Nodup
i : ℕ
h : i < xs.length
⊢ xs.formPerm xs[i] = xs[(i + 1) % xs.length]

Tactic:
rcases xs with - | ⟨x, xs⟩

Result:
case nil
α : Type u_1
inst✝ : DecidableEq α
i : ℕ
w : [].Nodup
h : i < [].length
⊢ [].formPerm [][i] = [][(i + 1) % [].length]

case cons
α : Type u_1
inst✝ : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
⊢ (x :: xs).formPerm (x :: xs)[i] = (x :: xs)[(i + 1) % (x :: xs).length]

Proof state:
case cons.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
w : (x :: xs).Nodup
h : xs.length < (x :: xs).length
this : xs.length ≤ xs.length
⊢ (x :: xs).formPerm (x :: xs)[xs.length] = (x :: xs)[(xs.length + 1) % (x :: xs).length]

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
⊢ i ≤ xs.length

Tactic:
refine Nat.le_of_lt_succ ?_

Result:
α : Type u_1
inst✝ : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
⊢ i < xs.length.succ

Proof state:
case cons.inr
α : Type u_1
inst✝ : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
this : i ≤ xs.length
hn' : i < xs.length
⊢ (x :: xs).formPerm (x :: xs)[i] = (x :: xs)[(i + 1) % (x :: xs).length]

Tactic:
rw [formPerm_apply_lt_getElem (x :: xs) w _ (Nat.succ_lt_succ hn')]

Result:
case cons.inr
α : Type u_1
inst✝ : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
this : i ≤ xs.length
hn' : i < xs.length
⊢ (x :: xs)[i + 1] = (x :: xs)[(i + 1) % (x :: xs).length]

Proof state:
case cons.inr.e_i
α : Type u_1
inst✝ : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
this : i ≤ xs.length
hn' : i < xs.length
⊢ i + 1 < (x :: xs).length

Tactic:
simpa [Nat.succ_eq_add_one]

Result:
no goals