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