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