cases t₁
τ : DimList
D : MLIRTy
t₁ t₂ : RankedTensor τ D
h_shape : t₁.toTensor.shape = t₂.toTensor.shape
h_data : t₁.toTensor.data = t₂.toTensor.data
this : t₁.toTensor = t₂.toTensor
⊢ t₁ = 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₂