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