Theorem: List.mapM_eq_map (Logic/Vorspiel/Vorspiel.lean)

State before:
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.168328 → Type ?u.168330
α : Type u_1
β : Type u_2
inst✝ : Monad m
l : List α
f : α → β
⊢ mapM' (fun x => some (f x)) l = some (map f l)
Tactic:
induction l <;> simp[Option.pure_eq_some, Option.bind_eq_bind, Function.comp, *]
State after:
no goals