theorem Vector.mapM_mk {m : Type u_1 → Type u_2} {α : Type u_3} {n : Nat} {β : Type u_1} [Monad m] [LawfulMonad m] [MonadSatisfying m] (a : Array α) (h : a.size = n) (f : α → m β) : mapM f { toArray := a, size_toArray := h } = (fun (x : { a_1 : Array β // a_1.size = a.size }) => match x with | ⟨a_1, h'⟩ => { toArray := a_1, size_toArray := ⋯ }) <$> satisfying ⋯

theorem Vector.mapIdxM_mk {m : Type u_1 → Type u_2} {α : Type u_3} {n : Nat} {β : Type u_1} [Monad m] [LawfulMonad m] [MonadSatisfying m] (a : Array α) (h : a.size = n) (f : Nat → α → m β) : mapIdxM f { toArray := a, size_toArray := h } = (fun (x : { a_1 : Array β // a_1.size = a.size }) => match x with | ⟨a_1, h'⟩ => { toArray := a_1, size_toArray := ⋯ }) <$> satisfying ⋯

theorem Vector.mapFinIdxM_mk {m : Type u_1 → Type u_2} {α : Type u_3} {n : Nat} {β : Type u_1} [Monad m] [LawfulMonad m] [MonadSatisfying m] (a : Array α) (h : a.size = n) (f : (i : Nat) → α → i < n → m β) : { toArray := a, size_toArray := h }.mapFinIdxM f = (fun (x : { a_1 : Array β // a_1.size = a.size }) => match x with | ⟨a_1, h'⟩ => { toArray := a_1, size_toArray := ⋯ }) <$> satisfying ⋯