-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem toArray_mapM_go [Monad m] [LawfulMonad m] (f : α → m β) (v : Vector α n) (i h r) :
    toArray <$> mapM.go f v i h r = Array.mapM.map f v.toArray i r.toArray

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
n : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
v : Vector α n
i : Nat
h : i ≤ n
r : Vector β i
⊢ (toArray <$>
      if h' : i < n then do
        let __do_lift ← f v[i]
        mapM.go f v (i + 1) ⋯ (r.push __do_lift)
      else pure (Vector.cast ⋯ r)) =
    Array.mapM.map f v.toArray i r.toArray

Tactic:
unfold Array.mapM.map

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
n : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
v : Vector α n
i : Nat
h : i ≤ n
r : Vector β i
⊢ (toArray <$>
      if h' : i < n then do
        let __do_lift ← f v[i]
        mapM.go f v (i + 1) ⋯ (r.push __do_lift)
      else pure (Vector.cast ⋯ r)) =
    if hlt : i < v.size then do
      let __do_lift ← f v.toArray[i]
      Array.mapM.map f v.toArray (i + 1) (r.push __do_lift)
    else pure r.toArray

Proof state:
case isFalse
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
n : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
v : Vector α n
i : Nat
h : i ≤ n
r : Vector β i
h✝ : ¬i < n
⊢ toArray <$> pure (Vector.cast ⋯ r) = pure r.toArray

Tactic:
simp

Result:
no goals

Proof state:
case isTrue.e_a.h
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
n : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
v : Vector α n
i : Nat
h : i ≤ n
r : Vector β i
h✝ : i < n
b : β
⊢ toArray <$> mapM.go f v (i + 1) ⋯ (r.push b) = Array.mapM.map f v.toArray (i + 1) (r.push b)

Tactic:
rw [toArray_mapM_go]

Result:
case isTrue.e_a.h
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
n : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
v : Vector α n
i : Nat
h : i ≤ n
r : Vector β i
h✝ : i < n
b : β
⊢ Array.mapM.map f v.toArray (i + 1) (r.push b).toArray = Array.mapM.map f v.toArray (i + 1) (r.push b)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
n : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
v : Vector α n
i : Nat
h : i ≤ n
r : Vector β i
⊢ (toArray <$>
      if h' : i < n then do
        let __do_lift ← f v[i]
        mapM.go f v (i + 1) ⋯ (r.push __do_lift)
      else pure (Vector.cast ⋯ r)) =
    if h : i < n then do
      let __do_lift ← f v[i]
      Array.mapM.map f v.toArray (i + 1) (r.push __do_lift)
    else pure r.toArray

Tactic:
split

Result:
case isTrue
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
n : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
v : Vector α n
i : Nat
h : i ≤ n
r : Vector β i
h✝ : i < n
⊢ (toArray <$> do
      let __do_lift ← f v[i]
      mapM.go f v (i + 1) ⋯ (r.push __do_lift)) =
    do
    let __do_lift ← f v[i]
    Array.mapM.map f v.toArray (i + 1) (r.push __do_lift)

case isFalse
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
n : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
v : Vector α n
i : Nat
h : i ≤ n
r : Vector β i
h✝ : ¬i < n
⊢ toArray <$> pure (Vector.cast ⋯ r) = pure r.toArray

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
n : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
v : Vector α n
i : Nat
h : i ≤ n
r : Vector β i
⊢ (toArray <$>
      if h' : i < n then do
        let __do_lift ← f v[i]
        mapM.go f v (i + 1) ⋯ (r.push __do_lift)
      else pure (Vector.cast ⋯ r)) =
    if hlt : i < v.size then do
      let __do_lift ← f v.toArray[i]
      Array.mapM.map f v.toArray (i + 1) (r.push __do_lift)
    else pure r.toArray

Tactic:
simp only [v.size_toArray, getElem_toArray]

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
n : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
v : Vector α n
i : Nat
h : i ≤ n
r : Vector β i
⊢ (toArray <$>
      if h' : i < n then do
        let __do_lift ← f v[i]
        mapM.go f v (i + 1) ⋯ (r.push __do_lift)
      else pure (Vector.cast ⋯ r)) =
    if h : i < n then do
      let __do_lift ← f v[i]
      Array.mapM.map f v.toArray (i + 1) (r.push __do_lift)
    else pure r.toArray

Proof state:
case isTrue
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
n : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
v : Vector α n
i : Nat
h : i ≤ n
r : Vector β i
h✝ : i < n
⊢ (toArray <$> do
      let __do_lift ← f v[i]
      mapM.go f v (i + 1) ⋯ (r.push __do_lift)) =
    do
    let __do_lift ← f v[i]
    Array.mapM.map f v.toArray (i + 1) (r.push __do_lift)

Tactic:
simp only [map_bind]

Result:
case isTrue
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
n : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
v : Vector α n
i : Nat
h : i ≤ n
r : Vector β i
h✝ : i < n
⊢ (do
      let a ← f v[i]
      toArray <$> mapM.go f v (i + 1) ⋯ (r.push a)) =
    do
    let __do_lift ← f v[i]
    Array.mapM.map f v.toArray (i + 1) (r.push __do_lift)

Proof state:
case isTrue.e_a
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
n : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
v : Vector α n
i : Nat
h : i ≤ n
r : Vector β i
h✝ : i < n
⊢ (fun a => toArray <$> mapM.go f v (i + 1) ⋯ (r.push a)) = fun __do_lift =>
    Array.mapM.map f v.toArray (i + 1) (r.push __do_lift)

Tactic:
funext b

Result:
case isTrue.e_a.h
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
n : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
v : Vector α n
i : Nat
h : i ≤ n
r : Vector β i
h✝ : i < n
b : β
⊢ toArray <$> mapM.go f v (i + 1) ⋯ (r.push b) = Array.mapM.map f v.toArray (i + 1) (r.push b)

Proof state:
case isTrue
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
n : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
v : Vector α n
i : Nat
h : i ≤ n
r : Vector β i
h✝ : i < n
⊢ (do
      let a ← f v[i]
      toArray <$> mapM.go f v (i + 1) ⋯ (r.push a)) =
    do
    let __do_lift ← f v[i]
    Array.mapM.map f v.toArray (i + 1) (r.push __do_lift)

Tactic:
congr

Result:
case isTrue.e_a
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
n : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
v : Vector α n
i : Nat
h : i ≤ n
r : Vector β i
h✝ : i < n
⊢ (fun a => toArray <$> mapM.go f v (i + 1) ⋯ (r.push a)) = fun __do_lift =>
    Array.mapM.map f v.toArray (i + 1) (r.push __do_lift)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
n : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
v : Vector α n
i : Nat
h : i ≤ n
r : Vector β i
⊢ toArray <$> mapM.go f v i h r = Array.mapM.map f v.toArray i r.toArray

Tactic:
unfold mapM.go

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
n : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
v : Vector α n
i : Nat
h : i ≤ n
r : Vector β i
⊢ (toArray <$>
      if h' : i < n then do
        let __do_lift ← f v[i]
        mapM.go f v (i + 1) ⋯ (r.push __do_lift)
      else pure (Vector.cast ⋯ r)) =
    Array.mapM.map f v.toArray i r.toArray

Proof state:
case isTrue.e_a.h
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
n : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
v : Vector α n
i : Nat
h : i ≤ n
r : Vector β i
h✝ : i < n
b : β
⊢ Array.mapM.map f v.toArray (i + 1) (r.push b).toArray = Array.mapM.map f v.toArray (i + 1) (r.push b)

Tactic:
rfl

Result:
no goals