match bs, xs with
| b :: bs, x :: xs =>
cases b with
| true => exact Mem.head _
| false => simp only [get, map] at hget
case mpr.zero
α : Type u_1
β : Type u_2
f : α → β
xs : List α
bs : List Bool
pf1 : Nat.zero < length xs
pf2 : Nat.zero < length bs
hu : Unique (map f xs)
hget : get bs { val := Nat.zero, isLt := pf2 } = true
⊢ get (map f xs) { val := Nat.zero, isLt := (_ : Nat.zero < length (map f xs)) } ∈ map f (sieve bs xs)
no goals