Theorem: LoVe.mmap_append (LoVe/Lectures/LoVe07_EffectfulProgramming_Demo.lean)

State before:
m : Type → Type
inst✝ : LawfulMonad m
α β : Type
f : α → m β
x✝ : List α
⊢ mmap f ([] ++ x✝) = do
    let bs ← mmap f []
    let bs' ← mmap f x✝
    pure (bs ++ bs')
Tactic:
simp [mmap, LawfulMonad.bind_pure, LawfulMonad.pure_bind]
State after:
no goals

State before:
m : Type → Type
inst✝ : LawfulMonad m
α β : Type
f : α → m β
a : α
as as' : List α
⊢ mmap f (a :: as ++ as') = do
    let bs ← mmap f (a :: as)
    let bs' ← mmap f as'
    pure (bs ++ bs')
Tactic:
simp [mmap, mmap_append _ as as', LawfulMonad.pure_bind,
LawfulMonad.bind_assoc]
State after:
no goals