trivial
case mk.mk
τ : DimList
D : MLIRTy
toTensor✝¹ : Tensor D
h_refines✝¹ : DimList.shapeRefines toTensor✝¹.shape τ = true
toTensor✝ : Tensor D
h_refines✝ : DimList.shapeRefines toTensor✝.shape τ = true
h_shape : toTensor✝¹.shape = toTensor✝.shape
h_data : toTensor✝¹.data = toTensor✝.data
this : toTensor✝¹ = toTensor✝
⊢ toTensor✝¹ = toTensor✝
no goals