Theorem: mapMCommute.mapM_cons (MLIR/Dialects/LinalgSemantics.lean)

State before:
m : Type u_1 → Type u_2
a : Type u_3
b : Type u_1
M : Monad m
LM : LawfulMonad m
x : a
xs : List a
f : a → m b
⊢ mapM f (x :: xs) = do
    let b_1 ← f x
    let bs ← mapM f xs
    pure (b_1 :: bs)
Tactic:
simp[List.mapM, List.mapM.loop]
State after:
m : Type u_1 → Type u_2
a : Type u_3
b : Type u_1
M : Monad m
LM : LawfulMonad m
x : a
xs : List a
f : a → m b
⊢ (do
      let __do_lift ← f x
      List.mapM.loop f xs [__do_lift]) =
    do
    let b_1 ← f x
    let bs ← List.mapM.loop f xs []
    pure (b_1 :: bs)

State before:
m : Type u_1 → Type u_2
a : Type u_3
b : Type u_1
M : Monad m
LM : LawfulMonad m
x : a
xs : List a
f : a → m b
⊢ (do
      let __do_lift ← f x
      List.mapM.loop f xs [__do_lift]) =
    do
    let b_1 ← f x
    let bs ← List.mapM.loop f xs []
    pure (b_1 :: bs)
Tactic:
sorry
State after:
no goals