no goals
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
l₁ l₂ : List α
⊢ mapM f (l₁ ++ l₂) = do
    let __do_lift ← mapM f l₁
    let __do_lift_1 ← mapM f l₂
    pure (__do_lift ++ __do_lift_1)
induction l₁ <;> simp [*]