rw[this, List.bind_pure_eq_map]
α : Type u
inst✝¹ : DecidableEq α
β : Type v
inst✝ : DecidableEq β
f : β → Option α
g : β → α
bs : List β
h : ∀ x ∈ bs, f x = some (g x)
this : (bs.bind fun i => (f i).toList) = bs.bind (pure ∘ g)
⊢ (bs.bind fun i => (f i).toList) = map g bs
no goals