α : Type u_1
β : Type ?u.733602
inst✝ : DecidableEq α
l : List α
x : α
⊢ ↑(toFinset l ⊔ toFinset (tail l)) ≤ ↑(toFinset l)
α : Type u_1
β : Type ?u.733602
inst✝ : DecidableEq α
l : List α
x : α
⊢ {x | ↑(formPerm l) x ≠ x} ≤ ↑(toFinset l)
refine' (zipWith_swap_prod_support' l l.tail).trans _
no goals
α : Type u_1
β : Type ?u.733602
inst✝ : DecidableEq α
l : List α
x : α
⊢ ↑(toFinset l ⊔ toFinset (tail l)) ≤ ↑(toFinset l)
simpa [Finset.subset_iff] using tail_subset l