match bs, xs, hu with
| b :: bs, x :: xs, .cons hnmem hu =>
cases b with
| true => simp only [get, sieve] at *
| false =>
  simp only [get, sieve] at *
  exact mt mem_map_sieve_of_mem_map hnmem hf
case mp.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)
hf : get (map f xs) { val := Nat.zero, isLt := (_ : Nat.zero < length (map f xs)) } ∈ map f (sieve bs xs)
⊢ get bs { val := Nat.zero, isLt := pf2 } = true
no goals