intros h_shape h_data
τ : DimList
D : MLIRTy
t₁ t₂ : RankedTensor τ D
⊢ t₁.toTensor.shape = t₂.toTensor.shape → t₁.toTensor.data = t₂.toTensor.data → t₁ = t₂
τ : DimList
D : MLIRTy
t₁ t₂ : RankedTensor τ D
h_shape : t₁.toTensor.shape = t₂.toTensor.shape
h_data : t₁.toTensor.data = t₂.toTensor.data
⊢ t₁ = t₂