. intro hget
  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)
⊢ 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