no goals
α : Type u
β : Type v
p : α → Prop
inst✝ : DecidablePred p
as : List α
⊢ findIdxs (fun b => decide (p b)) as = map Prod.fst (indexesValues (fun b => decide (p b)) as)
simp only [indexesValues_eq_filter_enum, map_filter_eq_foldr, findIdxs, uncurry,
  foldrIdx_eq_foldr_enum, decide_eq_true_eq, comp_apply, Bool.cond_decide]