Finite optional traversal

A successful finite traversal retains the value returned at every coordinate, including when the index type is empty. The temporary buffer is confined to the internal representation proof.

@[simp]

theorem TorchLean.Tensor.Internal.sequenceFinM_pure {m : Type → Type} [Monad m] [LawfulMonad m] {α : Type} {n : ℕ} (values : Fin n → α) : sequenceFinM (pure ∘ values) = pure values

Sequencing a pure finite family retains the original indexed values.

theorem TorchLean.Tensor.Internal.sequenceFinM_get_of_eq_some {α : Type} {n : ℕ} {f : Fin n → Option α} {values : Fin n → α} (h : sequenceFinM f = some values) (i : Fin n) : f i = some (values i)

Unpack a successful finite sequence without assumptions about positive cardinality.