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 (mk a h) = (fun (x : { a_1 : Array β // a_1.size = a.size }) => match x with | ⟨a_1, h'⟩ => mk a_1 ⋯) <$> 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 (mk a h) = (fun (x : { a_1 : Array β // a_1.size = a.size }) => match x with | ⟨a_1, h'⟩ => mk a_1 ⋯) <$> 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 β) : (mk a h).mapFinIdxM f = (fun (x : { a_1 : Array β // a_1.size = a.size }) => match x with | ⟨a_1, h'⟩ => mk a_1 ⋯) <$> satisfying ⋯