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

State before:
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
⊢ fish (mapM f) (mapM g) = mapM (fish f g)
Tactic:
funext x
State after:
case h
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
x : List a
⊢ fish (mapM f) (mapM g) x = mapM (fish f g) x

State before:
case h
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
x : List a
⊢ fish (mapM f) (mapM g) x = mapM (fish f g) x
Tactic:
induction x
State after:
case h.nil
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
⊢ fish (mapM f) (mapM g) [] = mapM (fish f g) []

case h.cons
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
head✝ : a
tail✝ : List a
tail_ih✝ : fish (mapM f) (mapM g) tail✝ = mapM (fish f g) tail✝
⊢ fish (mapM f) (mapM g) (head✝ :: tail✝) = mapM (fish f g) (head✝ :: tail✝)

State before:
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
⊢ fish (mapM f) (mapM g) [] = mapM (fish f g) []
Tactic:
case nil => {
     simp[fish, List.mapM, List.mapM.loop];
}
State after:
no goals

State before:
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
⊢ fish (mapM f) (mapM g) (head :: tail) = mapM (fish f g) (head :: tail)
Tactic:
case cons head tail IH => {
  rewrite [mapM_cons];
  simp[fish];
  simp [bind_assoc]
  simp[mapM_cons];
  congr; funext x';
  rewrite [commute_implies_mapM_commute];
  congr;
  funext x';
  simp [fish] at IH;
  rewrite [<- IH];
  simp[bind_assoc];
  apply COMMUTE;
}
State after:
no goals

State before:
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
⊢ fish (mapM f) (mapM g) [] = mapM (fish f g) []
Tactic:
simp[fish, List.mapM, List.mapM.loop]
State after:
no goals

State before:
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
⊢ fish (mapM f) (mapM g) (head :: tail) = mapM (fish f g) (head :: tail)
Tactic:
rewrite [mapM_cons]
State after:
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
⊢ fish (mapM f) (mapM g) (head :: tail) = do
    let b ← fish f g head
    let bs ← mapM (fish f g) tail
    pure (b :: bs)

State before:
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
⊢ fish (mapM f) (mapM g) (head :: tail) = do
    let b ← fish f g head
    let bs ← mapM (fish f g) tail
    pure (b :: bs)
Tactic:
simp[fish]
State after:
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
⊢ (do
      let x ← f head
      let x_1 ← mapM f tail
      let __do_lift ← g x
      let __do_lift_1 ← mapM g x_1
      pure (__do_lift :: __do_lift_1)) =
    do
    let x ← f head
    let b ← g x
    let bs ← mapM (fun a_1 => f a_1 >>= g) tail
    pure (b :: bs)

State before:
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
⊢ (do
      let x ← f head
      let x_1 ← mapM f tail
      let __do_lift ← g x
      let __do_lift_1 ← mapM g x_1
      pure (__do_lift :: __do_lift_1)) =
    do
    let x ← f head
    let b ← g x
    let bs ← mapM (fun a_1 => f a_1 >>= g) tail
    pure (b :: bs)
Tactic:
congr
State after:
case e_a
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
⊢ (fun x => do
      let x_1 ← mapM f tail
      let __do_lift ← g x
      let __do_lift_1 ← mapM g x_1
      pure (__do_lift :: __do_lift_1)) =
    fun x => do
    let b ← g x
    let bs ← mapM (fun a_1 => f a_1 >>= g) tail
    pure (b :: bs)

State before:
case e_a
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
⊢ (fun x => do
      let x_1 ← mapM f tail
      let __do_lift ← g x
      let __do_lift_1 ← mapM g x_1
      pure (__do_lift :: __do_lift_1)) =
    fun x => do
    let b ← g x
    let bs ← mapM (fun a_1 => f a_1 >>= g) tail
    pure (b :: bs)
Tactic:
funext x'
State after:
case e_a.h
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x' : a
⊢ (do
      let x ← mapM f tail
      let __do_lift ← g x'
      let __do_lift_1 ← mapM g x
      pure (__do_lift :: __do_lift_1)) =
    do
    let b ← g x'
    let bs ← mapM (fun a_1 => f a_1 >>= g) tail
    pure (b :: bs)

State before:
case e_a.h
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x' : a
⊢ (do
      let x ← mapM f tail
      let __do_lift ← g x'
      let __do_lift_1 ← mapM g x
      pure (__do_lift :: __do_lift_1)) =
    do
    let b ← g x'
    let bs ← mapM (fun a_1 => f a_1 >>= g) tail
    pure (b :: bs)
Tactic:
rewrite [commute_implies_mapM_commute]
State after:
case e_a.h
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x' : a
⊢ (do
      let r2 ← g x'
      let r1 ← mapM f tail
      let __do_lift ← mapM g r1
      pure (r2 :: __do_lift)) =
    do
    let b ← g x'
    let bs ← mapM (fun a_1 => f a_1 >>= g) tail
    pure (b :: bs)

case e_a.h.COMMUTE
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x' : a
⊢ ∀ {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

State before:
case e_a.h
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x' : a
⊢ (do
      let r2 ← g x'
      let r1 ← mapM f tail
      let __do_lift ← mapM g r1
      pure (r2 :: __do_lift)) =
    do
    let b ← g x'
    let bs ← mapM (fun a_1 => f a_1 >>= g) tail
    pure (b :: bs)

case e_a.h.COMMUTE
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x' : a
⊢ ∀ {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
Tactic:
congr
State after:
case e_a.h.e_a
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x' : a
⊢ (fun r2 => do
      let r1 ← mapM f tail
      let __do_lift ← mapM g r1
      pure (r2 :: __do_lift)) =
    fun b => do
    let bs ← mapM (fun a_1 => f a_1 >>= g) tail
    pure (b :: bs)

case e_a.h.COMMUTE
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x' : a
⊢ ∀ {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

State before:
case e_a.h.e_a
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x' : a
⊢ (fun r2 => do
      let r1 ← mapM f tail
      let __do_lift ← mapM g r1
      pure (r2 :: __do_lift)) =
    fun b => do
    let bs ← mapM (fun a_1 => f a_1 >>= g) tail
    pure (b :: bs)

case e_a.h.COMMUTE
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x' : a
⊢ ∀ {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
Tactic:
funext x'
State after:
case e_a.h.e_a.h
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x'✝ x' : a
⊢ (do
      let r1 ← mapM f tail
      let __do_lift ← mapM g r1
      pure (x' :: __do_lift)) =
    do
    let bs ← mapM (fun a_1 => f a_1 >>= g) tail
    pure (x' :: bs)

case e_a.h.COMMUTE
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x' : a
⊢ ∀ {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

State before:
case e_a.h.e_a.h
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x'✝ x' : a
⊢ (do
      let r1 ← mapM f tail
      let __do_lift ← mapM g r1
      pure (x' :: __do_lift)) =
    do
    let bs ← mapM (fun a_1 => f a_1 >>= g) tail
    pure (x' :: bs)

case e_a.h.COMMUTE
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x' : a
⊢ ∀ {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
Tactic:
simp [fish] at IH
State after:
case e_a.h.e_a.h
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
head : a
tail : List a
IH : mapM f tail >>= mapM g = mapM (fun a_1 => f a_1 >>= g) tail
x'✝ x' : a
⊢ (do
      let r1 ← mapM f tail
      let __do_lift ← mapM g r1
      pure (x' :: __do_lift)) =
    do
    let bs ← mapM (fun a_1 => f a_1 >>= g) tail
    pure (x' :: bs)

case e_a.h.COMMUTE
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x' : a
⊢ ∀ {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

State before:
case e_a.h.e_a.h
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
head : a
tail : List a
IH : mapM f tail >>= mapM g = mapM (fun a_1 => f a_1 >>= g) tail
x'✝ x' : a
⊢ (do
      let r1 ← mapM f tail
      let __do_lift ← mapM g r1
      pure (x' :: __do_lift)) =
    do
    let bs ← mapM (fun a_1 => f a_1 >>= g) tail
    pure (x' :: bs)

case e_a.h.COMMUTE
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x' : a
⊢ ∀ {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
Tactic:
rewrite [<- IH]
State after:
case e_a.h.e_a.h
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
head : a
tail : List a
IH : mapM f tail >>= mapM g = mapM (fun a_1 => f a_1 >>= g) tail
x'✝ x' : a
⊢ (do
      let r1 ← mapM f tail
      let __do_lift ← mapM g r1
      pure (x' :: __do_lift)) =
    do
    let bs ← mapM f tail >>= mapM g
    pure (x' :: bs)

case e_a.h.COMMUTE
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x' : a
⊢ ∀ {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

State before:
case e_a.h.e_a.h
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
head : a
tail : List a
IH : mapM f tail >>= mapM g = mapM (fun a_1 => f a_1 >>= g) tail
x'✝ x' : a
⊢ (do
      let r1 ← mapM f tail
      let __do_lift ← mapM g r1
      pure (x' :: __do_lift)) =
    do
    let bs ← mapM f tail >>= mapM g
    pure (x' :: bs)

case e_a.h.COMMUTE
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x' : a
⊢ ∀ {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
Tactic:
simp[bind_assoc]
State after:
case e_a.h.COMMUTE
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x' : a
⊢ ∀ {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

State before:
case e_a.h.COMMUTE
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
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
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
x' : a
⊢ ∀ {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
Tactic:
apply COMMUTE
State after:
no goals