-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Monadic.lean
theorem mapM_append [Monad m] [LawfulMonad m] [Nonempty β]
    (f : α → m β) {l₁ : Vector α n} {l₂ : Vector α n'} :
    (l₁ ++ l₂).mapM f = (return (← l₁.mapM f) ++ (← l₂.mapM f))

Proof state:
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
n n' : Nat
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : Nonempty β
f : α → m β
l₁ : Vector α n
l₂ : Vector α n'
this :
  toArray <$> mapM f (l₁ ++ l₂) = do
    let __do_lift ← toArray <$> mapM f l₁
    let __do_lift_1 ← toArray <$> mapM f l₂
    pure (__do_lift ++ __do_lift_1)
⊢ toArray <$> mapM f (l₁ ++ l₂) =
    toArray <$> do
      let __do_lift ← mapM f l₁
      let __do_lift_1 ← mapM f l₂
      pure (__do_lift ++ __do_lift_1)

Tactic:
rw [this]

Result:
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
n n' : Nat
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : Nonempty β
f : α → m β
l₁ : Vector α n
l₂ : Vector α n'
this :
  toArray <$> mapM f (l₁ ++ l₂) = do
    let __do_lift ← toArray <$> mapM f l₁
    let __do_lift_1 ← toArray <$> mapM f l₂
    pure (__do_lift ++ __do_lift_1)
⊢ (do
      let __do_lift ← toArray <$> mapM f l₁
      let __do_lift_1 ← toArray <$> mapM f l₂
      pure (__do_lift ++ __do_lift_1)) =
    toArray <$> do
      let __do_lift ← mapM f l₁
      let __do_lift_1 ← mapM f l₂
      pure (__do_lift ++ __do_lift_1)

Proof state:
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
n n' : Nat
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : Nonempty β
f : α → m β
l₁ : Vector α n
l₂ : Vector α n'
⊢ mapM f (l₁ ++ l₂) = do
    let __do_lift ← mapM f l₁
    let __do_lift_1 ← mapM f l₂
    pure (__do_lift ++ __do_lift_1)

Tactic:
apply map_toArray_inj

Result:
case w
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
n n' : Nat
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : Nonempty β
f : α → m β
l₁ : Vector α n
l₂ : Vector α n'
⊢ toArray <$> mapM f (l₁ ++ l₂) =
    toArray <$> do
      let __do_lift ← mapM f l₁
      let __do_lift_1 ← mapM f l₂
      pure (__do_lift ++ __do_lift_1)

Proof state:
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
n n' : Nat
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : Nonempty β
f : α → m β
l₁ : Vector α n
l₂ : Vector α n'
this :
  toArray <$> mapM f (l₁ ++ l₂) = do
    let __do_lift ← toArray <$> mapM f l₁
    let __do_lift_1 ← toArray <$> mapM f l₂
    pure (__do_lift ++ __do_lift_1)
⊢ (do
      let __do_lift ← toArray <$> mapM f l₁
      let __do_lift_1 ← toArray <$> mapM f l₂
      pure (__do_lift ++ __do_lift_1)) =
    toArray <$> do
      let __do_lift ← mapM f l₁
      let __do_lift_1 ← mapM f l₂
      pure (__do_lift ++ __do_lift_1)

Tactic:
simp only [bind_pure_comp, Functor.map_map, bind_map_left, map_bind, toArray_append]

Result:
no goals

Proof state:
case w
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
n n' : Nat
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : Nonempty β
f : α → m β
l₁ : Vector α n
l₂ : Vector α n'
⊢ toArray <$> mapM f (l₁ ++ l₂) = do
    let __do_lift ← toArray <$> mapM f l₁
    let __do_lift_1 ← toArray <$> mapM f l₂
    pure (__do_lift ++ __do_lift_1)

Tactic:
simp

Result:
no goals

Proof state:
case w
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
n n' : Nat
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : Nonempty β
f : α → m β
l₁ : Vector α n
l₂ : Vector α n'
⊢ toArray <$> mapM f (l₁ ++ l₂) =
    toArray <$> do
      let __do_lift ← mapM f l₁
      let __do_lift_1 ← mapM f l₂
      pure (__do_lift ++ __do_lift_1)

Tactic:
suffices toArray <$> (l₁ ++ l₂).mapM f = (return (← toArray <$> l₁.mapM f) ++ (← toArray <$> l₂.mapM f)) by
  rw [this]
  simp only [bind_pure_comp, Functor.map_map, bind_map_left, map_bind, toArray_append]

Result:
case w
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
n n' : Nat
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : Nonempty β
f : α → m β
l₁ : Vector α n
l₂ : Vector α n'
⊢ toArray <$> mapM f (l₁ ++ l₂) = do
    let __do_lift ← toArray <$> mapM f l₁
    let __do_lift_1 ← toArray <$> mapM f l₂
    pure (__do_lift ++ __do_lift_1)