case nil
α : Type u_1
β : Type ?u.761706
inst✝ : DecidableEq α
l : List α
x : α
n : ℕ
h : Nodup []
hn : n < length []
⊢ ↑(formPerm []) (nthLe [] n hn) = nthLe [] ((n + 1) % length []) (_ : (n + 1) % length [] < length [])

case cons
α : Type u_1
β : Type ?u.761706
inst✝ : DecidableEq α
l : List α
x✝ : α
n : ℕ
x : α
xs : List α
h : Nodup (x :: xs)
hn : n < length (x :: xs)
⊢ ↑(formPerm (x :: xs)) (nthLe (x :: xs) n hn) =
    nthLe (x :: xs) ((n + 1) % length (x :: xs)) (_ : (n + 1) % length (x :: xs) < length (x :: xs))
α : Type u_1
β : Type ?u.761706
inst✝ : DecidableEq α
l : List α
x : α
xs : List α
h : Nodup xs
n : ℕ
hn : n < length xs
⊢ ↑(formPerm xs) (nthLe xs n hn) = nthLe xs ((n + 1) % length xs) (_ : (n + 1) % length xs < length xs)
cases' xs with x xs
no goals
case nil
α : Type u_1
β : Type ?u.761706
inst✝ : DecidableEq α
l : List α
x : α
n : ℕ
h : Nodup []
hn : n < length []
⊢ ↑(formPerm []) (nthLe [] n hn) = nthLe [] ((n + 1) % length []) (_ : (n + 1) % length [] < length [])
simp at hn
case cons
α : Type u_1
β : Type ?u.761706
inst✝ : DecidableEq α
l : List α
x✝ : α
n : ℕ
x : α
xs : List α
h : Nodup (x :: xs)
hn : n < length (x :: xs)
this : n ≤ length xs
⊢ ↑(formPerm (x :: xs)) (nthLe (x :: xs) n hn) =
    nthLe (x :: xs) ((n + 1) % length (x :: xs)) (_ : (n + 1) % length (x :: xs) < length (x :: xs))
case cons
α : Type u_1
β : Type ?u.761706
inst✝ : DecidableEq α
l : List α
x✝ : α
n : ℕ
x : α
xs : List α
h : Nodup (x :: xs)
hn : n < length (x :: xs)
⊢ ↑(formPerm (x :: xs)) (nthLe (x :: xs) n hn) =
    nthLe (x :: xs) ((n + 1) % length (x :: xs)) (_ : (n + 1) % length (x :: xs) < length (x :: xs))
have : n ≤ xs.length := by
  refine' Nat.le_of_lt_succ _
  simpa using hn
case cons.inl
α : Type u_1
β : Type ?u.761706
inst✝ : DecidableEq α
l : List α
x✝ x : α
xs : List α
h : Nodup (x :: xs)
hn : length xs < length (x :: xs)
this : length xs ≤ length xs
⊢ ↑(formPerm (x :: xs)) (nthLe (x :: xs) (length xs) hn) =
    nthLe (x :: xs) ((length xs + 1) % length (x :: xs)) (_ : (length xs + 1) % length (x :: xs) < length (x :: xs))

case cons.inr
α : Type u_1
β : Type ?u.761706
inst✝ : DecidableEq α
l : List α
x✝ : α
n : ℕ
x : α
xs : List α
h : Nodup (x :: xs)
hn : n < length (x :: xs)
this : n ≤ length xs
hn' : n < length xs
⊢ ↑(formPerm (x :: xs)) (nthLe (x :: xs) n hn) =
    nthLe (x :: xs) ((n + 1) % length (x :: xs)) (_ : (n + 1) % length (x :: xs) < length (x :: xs))
case cons
α : Type u_1
β : Type ?u.761706
inst✝ : DecidableEq α
l : List α
x✝ : α
n : ℕ
x : α
xs : List α
h : Nodup (x :: xs)
hn : n < length (x :: xs)
this : n ≤ length xs
⊢ ↑(formPerm (x :: xs)) (nthLe (x :: xs) n hn) =
    nthLe (x :: xs) ((n + 1) % length (x :: xs)) (_ : (n + 1) % length (x :: xs) < length (x :: xs))
rcases this.eq_or_lt with (rfl | hn')
α : Type u_1
β : Type ?u.761706
inst✝ : DecidableEq α
l : List α
x✝ : α
n : ℕ
x : α
xs : List α
h : Nodup (x :: xs)
hn : n < length (x :: xs)
⊢ n < Nat.succ (length xs)
α : Type u_1
β : Type ?u.761706
inst✝ : DecidableEq α
l : List α
x✝ : α
n : ℕ
x : α
xs : List α
h : Nodup (x :: xs)
hn : n < length (x :: xs)
⊢ n ≤ length xs
refine' Nat.le_of_lt_succ _
no goals
α : Type u_1
β : Type ?u.761706
inst✝ : DecidableEq α
l : List α
x✝ : α
n : ℕ
x : α
xs : List α
h : Nodup (x :: xs)
hn : n < length (x :: xs)
⊢ n < Nat.succ (length xs)
simpa using hn
case cons.inl
α : Type u_1
β : Type ?u.761706
inst✝ : DecidableEq α
l : List α
x✝ x : α
xs : List α
h : Nodup (x :: xs)
hn : length xs < length (x :: xs)
this : length xs ≤ length xs
⊢ x = nthLe (x :: xs) 0 (_ : 0 < length (x :: xs))
case cons.inl
α : Type u_1
β : Type ?u.761706
inst✝ : DecidableEq α
l : List α
x✝ x : α
xs : List α
h : Nodup (x :: xs)
hn : length xs < length (x :: xs)
this : length xs ≤ length xs
⊢ ↑(formPerm (x :: xs)) (nthLe (x :: xs) (length xs) hn) =
    nthLe (x :: xs) ((length xs + 1) % length (x :: xs)) (_ : (length xs + 1) % length (x :: xs) < length (x :: xs))
simp
no goals
case cons.inl
α : Type u_1
β : Type ?u.761706
inst✝ : DecidableEq α
l : List α
x✝ x : α
xs : List α
h : Nodup (x :: xs)
hn : length xs < length (x :: xs)
this : length xs ≤ length xs
⊢ x = nthLe (x :: xs) 0 (_ : 0 < length (x :: xs))
simp [nthLe]
case cons.inr
α : Type u_1
β : Type ?u.761706
inst✝ : DecidableEq α
l : List α
x✝ : α
n : ℕ
x : α
xs : List α
h : Nodup (x :: xs)
hn : n < length (x :: xs)
this : n ≤ length xs
hn' : n < length xs
⊢ nthLe (x :: xs) (n + 1) (_ : Nat.succ n < Nat.succ (length xs)) =
    nthLe (x :: xs) ((n + 1) % length (x :: xs)) (_ : (n + 1) % length (x :: xs) < length (x :: xs))
case cons.inr
α : Type u_1
β : Type ?u.761706
inst✝ : DecidableEq α
l : List α
x✝ : α
n : ℕ
x : α
xs : List α
h : Nodup (x :: xs)
hn : n < length (x :: xs)
this : n ≤ length xs
hn' : n < length xs
⊢ ↑(formPerm (x :: xs)) (nthLe (x :: xs) n hn) =
    nthLe (x :: xs) ((n + 1) % length (x :: xs)) (_ : (n + 1) % length (x :: xs) < length (x :: xs))
rw [formPerm_apply_lt _ h _ (Nat.succ_lt_succ hn')]
case cons.inr.e_n
α : Type u_1
β : Type ?u.761706
inst✝ : DecidableEq α
l : List α
x✝ : α
n : ℕ
x : α
xs : List α
h : Nodup (x :: xs)
hn : n < length (x :: xs)
this : n ≤ length xs
hn' : n < length xs
⊢ n + 1 = (n + 1) % length (x :: xs)
case cons.inr
α : Type u_1
β : Type ?u.761706
inst✝ : DecidableEq α
l : List α
x✝ : α
n : ℕ
x : α
xs : List α
h : Nodup (x :: xs)
hn : n < length (x :: xs)
this : n ≤ length xs
hn' : n < length xs
⊢ nthLe (x :: xs) (n + 1) (_ : Nat.succ n < Nat.succ (length xs)) =
    nthLe (x :: xs) ((n + 1) % length (x :: xs)) (_ : (n + 1) % length (x :: xs) < length (x :: xs))
congr
case cons.inr.e_n
α : Type u_1
β : Type ?u.761706
inst✝ : DecidableEq α
l : List α
x✝ : α
n : ℕ
x : α
xs : List α
h : Nodup (x :: xs)
hn : n < length (x :: xs)
this : n ≤ length xs
hn' : n < length xs
⊢ n + 1 < length (x :: xs)
case cons.inr.e_n
α : Type u_1
β : Type ?u.761706
inst✝ : DecidableEq α
l : List α
x✝ : α
n : ℕ
x : α
xs : List α
h : Nodup (x :: xs)
hn : n < length (x :: xs)
this : n ≤ length xs
hn' : n < length xs
⊢ n + 1 = (n + 1) % length (x :: xs)
rw [Nat.mod_eq_of_lt]
no goals
case cons.inr.e_n
α : Type u_1
β : Type ?u.761706
inst✝ : DecidableEq α
l : List α
x✝ : α
n : ℕ
x : α
xs : List α
h : Nodup (x :: xs)
hn : n < length (x :: xs)
this : n ≤ length xs
hn' : n < length xs
⊢ n + 1 < length (x :: xs)
simpa [Nat.succ_eq_add_one]