cases t₂
case mk
τ : DimList
D : MLIRTy
t₂ : RankedTensor τ D
toTensor✝ : Tensor D
h_refines✝ : DimList.shapeRefines toTensor✝.shape τ = true
h_shape : { toTensor := toTensor✝, h_refines := h_refines✝ }.toTensor.shape = t₂.toTensor.shape
h_data : { toTensor := toTensor✝, h_refines := h_refines✝ }.toTensor.data = t₂.toTensor.data
this : { toTensor := toTensor✝, h_refines := h_refines✝ }.toTensor = t₂.toTensor
⊢ { toTensor := toTensor✝, h_refines := h_refines✝ } = t₂
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✝ }