-- Mathlib/.lake/packages/batteries/Batteries/Data/Vector/Monadic.lean
theorem toArray_mapFinIdxM [Monad m] [LawfulMonad m]
    (a : Vector α n) (f : (i : Nat) → α → (h : i < n) → m β) :
    toArray <$> a.mapFinIdxM f = a.toArray.mapFinIdxM
      (fun i x h => f i x (size_toArray a ▸ h))

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : Vector α n
f : (i : Nat) → α → i < n → m β
i j k : Nat
inv : k + 1 + j = n
bs : Vector β (n - (k + 1))
⊢ (do
      let a_1 ← f j a[j] ⋯
      toArray <$> mapFinIdxM.map a f k (j + 1) ⋯ (Vector.cast ⋯ (bs.push a_1))) =
    do
    let __do_lift ← f j a[j] ⋯
    Array.mapFinIdxM.map a.toArray (fun i x h => f i x ⋯) k (j + 1) ⋯ (bs.push __do_lift)

Tactic:
conv => lhs; arg 2; intro; rw [go]

Result:
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : Vector α n
f : (i : Nat) → α → i < n → m β
i j k : Nat
inv : k + 1 + j = n
bs : Vector β (n - (k + 1))
⊢ (do
      let x ← f j a[j] ⋯
      Array.mapFinIdxM.map a.toArray (fun i x h => f i x ⋯) k (j + 1) ⋯ (Vector.cast ⋯ (bs.push x)).toArray) =
    do
    let __do_lift ← f j a[j] ⋯
    Array.mapFinIdxM.map a.toArray (fun i x h => f i x ⋯) k (j + 1) ⋯ (bs.push __do_lift)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : Vector α n
f : (i : Nat) → α → i < n → m β
i j : Nat
inv : i + j = n
bs : Vector β (n - i)
⊢ toArray <$> mapFinIdxM.map a f i j inv bs = Array.mapFinIdxM.map a.toArray (fun i x h => f i x ⋯) i j ⋯ bs.toArray

Tactic:
match i with
| 0 => simp only [mapFinIdxM.map, map_pure, Array.mapFinIdxM.map, Nat.sub_zero]
| k + 1 =>
  simp only [mapFinIdxM.map, map_bind, Array.mapFinIdxM.map, getElem_toArray]
  conv => lhs; arg 2; intro; rw [go]
  rfl

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : Vector α n
f : (i : Nat) → α → i < n → m β
⊢ toArray <$> mapFinIdxM.map a f n 0 ⋯ (Vector.cast ⋯ { toArray := #[], size_toArray := ⋯ }) =
    Array.mapFinIdxM.map a.toArray (fun i x h => f i x ⋯) n 0 ⋯ (Array.mkEmpty n)

Tactic:
exact go _ _ _ _

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : Vector α n
f : (i : Nat) → α → i < n → m β
⊢ toArray <$> a.mapFinIdxM f = a.mapFinIdxM fun i x h => f i x ⋯

Tactic:
simp only [mapFinIdxM, Array.mapFinIdxM, size_toArray]

Result:
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : Vector α n
f : (i : Nat) → α → i < n → m β
⊢ toArray <$> mapFinIdxM.map a f n 0 ⋯ (Vector.cast ⋯ { toArray := #[], size_toArray := ⋯ }) =
    Array.mapFinIdxM.map a.toArray (fun i x h => f i x ⋯) n 0 ⋯ (Array.mkEmpty n)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : Vector α n
f : (i : Nat) → α → i < n → m β
i j k : Nat
inv : k + 1 + j = n
bs : Vector β (n - (k + 1))
⊢ toArray <$> mapFinIdxM.map a f (k + 1) j inv bs =
    Array.mapFinIdxM.map a.toArray (fun i x h => f i x ⋯) (k + 1) j ⋯ bs.toArray

Tactic:
simp only [mapFinIdxM.map, map_bind, Array.mapFinIdxM.map, getElem_toArray]

Result:
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : Vector α n
f : (i : Nat) → α → i < n → m β
i j k : Nat
inv : k + 1 + j = n
bs : Vector β (n - (k + 1))
⊢ (do
      let a_1 ← f j a[j] ⋯
      toArray <$> mapFinIdxM.map a f k (j + 1) ⋯ (Vector.cast ⋯ (bs.push a_1))) =
    do
    let __do_lift ← f j a[j] ⋯
    Array.mapFinIdxM.map a.toArray (fun i x h => f i x ⋯) k (j + 1) ⋯ (bs.push __do_lift)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : Vector α n
f : (i : Nat) → α → i < n → m β
i j : Nat
inv : 0 + j = n
bs : Vector β (n - 0)
⊢ toArray <$> mapFinIdxM.map a f 0 j inv bs = Array.mapFinIdxM.map a.toArray (fun i x h => f i x ⋯) 0 j ⋯ bs.toArray

Tactic:
simp only [mapFinIdxM.map, map_pure, Array.mapFinIdxM.map, Nat.sub_zero]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : Vector α n
f : (i : Nat) → α → i < n → m β
i j k : Nat
inv : k + 1 + j = n
bs : Vector β (n - (k + 1))
⊢ (do
      let x ← f j a[j] ⋯
      Array.mapFinIdxM.map a.toArray (fun i x h => f i x ⋯) k (j + 1) ⋯ (Vector.cast ⋯ (bs.push x)).toArray) =
    do
    let __do_lift ← f j a[j] ⋯
    Array.mapFinIdxM.map a.toArray (fun i x h => f i x ⋯) k (j + 1) ⋯ (bs.push __do_lift)

Tactic:
rfl

Result:
no goals