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

State before:
m : Type → Type u_1
a b : Type
xs : List a
y : a
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f g : a → m a
k : List a → a → m b
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
⊢ (do
      let r1 ← mapM f xs
      let r2 ← g y
      k r1 r2) =
    do
    let r2 ← g y
    let r1 ← mapM f xs
    k r1 r2
Tactic:
sorry
State after:
no goals