unfold mapWithFlatIndex
M : Type → Type
inst✝¹ : Monad M
inst✝ : LawfulMonad M
v : Tensor1D
f : TensorFlatIndex v.size0 → FinInt 32 → FinInt 32
fM : TensorFlatIndex v.size0 → FinInt 32 → M (FinInt 32)
h : ∀ (flat_index : TensorFlatIndex v.size0) (val : FinInt 32), fM flat_index val = pure (f flat_index val)
⊢ mapMWithFlatIndex v fM = pure (mapWithFlatIndex v f)
M : Type → Type
inst✝¹ : Monad M
inst✝ : LawfulMonad M
v : Tensor1D
f : TensorFlatIndex v.size0 → FinInt 32 → FinInt 32
fM : TensorFlatIndex v.size0 → FinInt 32 → M (FinInt 32)
h : ∀ (flat_index : TensorFlatIndex v.size0) (val : FinInt 32), fM flat_index val = pure (f flat_index val)
⊢ mapMWithFlatIndex v fM =
    pure
      { size0 := v.size0,
        data :=
          List.map
            (fun x =>
              match x with
              | (val, ix) => f ((_ : List.length v.data = v.size0) ▸ ix) val)
            (List.zipFlatIndex v.data),
        h_data_size :=
          (_ :
            List.length
                (List.map
                  (fun x =>
                    match x with
                    | (val, ix) => f ((_ : List.length v.data = v.size0) ▸ ix) val)
                  (List.zipFlatIndex v.data)) =
              v.size0) }