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

State before:
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.169273 → Type ?u.169275
α : Type u_2
β : Type u_3
inst✝ : Monad m
γ : Type u_1
as : List α
f : α → Option β
g : Option β → Option γ
⊢ mapM' g (map f as) = mapM' (g ∘ f) as
Tactic:
induction' as with a as ih <;> simp[Option.bind_eq_bind, Function.comp, *]
State after:
no goals