simp at *
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 := toTensor✝¹, h_refines := h_refines✝¹ }.toTensor.shape =
    { toTensor := toTensor✝, h_refines := h_refines✝ }.toTensor.shape
h_data :
  { toTensor := toTensor✝¹, h_refines := h_refines✝¹ }.toTensor.data =
    { toTensor := toTensor✝, h_refines := h_refines✝ }.toTensor.data
this :
  { toTensor := toTensor✝¹, h_refines := h_refines✝¹ }.toTensor =
    { toTensor := toTensor✝, h_refines := h_refines✝ }.toTensor
⊢ { toTensor := toTensor✝¹, h_refines := h_refines✝¹ } = { toTensor := toTensor✝, h_refines := h_refines✝ }
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✝