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