case nil
α : Type u_1
β : Type ?u.668958
inst✝ : DecidableEq α
l : List α
x : α
h : Nodup []
hl : 1 < length []
⊢ ↑(formPerm []) (nthLe [] 0 (_ : 0 < length [])) = nthLe [] 1 hl

case cons.nil
α : Type u_1
β : Type ?u.668958
inst✝ : DecidableEq α
l : List α
x✝ x : α
h : Nodup [x]
hl : 1 < length [x]
⊢ ↑(formPerm [x]) (nthLe [x] 0 (_ : 0 < length [x])) = nthLe [x] 1 hl

case cons.cons
α : Type u_1
β : Type ?u.668958
inst✝ : DecidableEq α
l : List α
x✝ x y : α
tl : List α
h : Nodup (x :: y :: tl)
hl : 1 < length (x :: y :: tl)
⊢ ↑(formPerm (x :: y :: tl)) (nthLe (x :: y :: tl) 0 (_ : 0 < length (x :: y :: tl))) = nthLe (x :: y :: tl) 1 hl
α : Type u_1
β : Type ?u.668958
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
h : Nodup l
hl : 1 < length l
⊢ ↑(formPerm l) (nthLe l 0 (_ : 0 < length l)) = nthLe l 1 hl
rcases l with (_ | ⟨x, _ | ⟨y, tl⟩⟩)
no goals
case nil
α : Type u_1
β : Type ?u.668958
inst✝ : DecidableEq α
l : List α
x : α
h : Nodup []
hl : 1 < length []
⊢ ↑(formPerm []) (nthLe [] 0 (_ : 0 < length [])) = nthLe [] 1 hl
simp at hl
no goals
case cons.nil
α : Type u_1
β : Type ?u.668958
inst✝ : DecidableEq α
l : List α
x✝ x : α
h : Nodup [x]
hl : 1 < length [x]
⊢ ↑(formPerm [x]) (nthLe [x] 0 (_ : 0 < length [x])) = nthLe [x] 1 hl
simp
no goals
case cons.cons
α : Type u_1
β : Type ?u.668958
inst✝ : DecidableEq α
l : List α
x✝ x y : α
tl : List α
h : Nodup (x :: y :: tl)
hl : 1 < length (x :: y :: tl)
⊢ ↑(formPerm (x :: y :: tl)) (nthLe (x :: y :: tl) 0 (_ : 0 < length (x :: y :: tl))) = nthLe (x :: y :: tl) 1 hl
simpa using formPerm_apply_head _ _ _ h