case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
⊢ ↑(formPerm l) (nthLe l k hk) = next l (nthLe l k hk) hx
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
x : α
hx : x ∈ l
⊢ ↑(formPerm l) x = next l x hx
obtain ⟨k, hk, rfl⟩ := nthLe_of_mem hx
no goals
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hl : Nodup l
k : ℕ
hk : k < length l
hx : nthLe l k hk ∈ l
⊢ ↑(formPerm l) (nthLe l k hk) = next l (nthLe l k hk) hx
rw [next_nthLe _ hl, formPerm_apply_nthLe _ hl]