. intros a; cases a; simp [h]
case a
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)
⊢ ∀ (a : FinInt 32 × TensorFlatIndex (List.length v.data)),
    (match a with
      | (val, ix) => fM ((_ : List.length v.data = v.size0) ▸ ix) val) =
      pure (f ((_ : List.length v.data = v.size0) ▸ a.snd) a.fst)
no goals