cases t₂
case mk
τ : MLIRTy
t₂ : Tensor τ
shape✝ : List ℕ
data✝ : List (MLIRType.eval τ)
h_data_size✝ : List.length data✝ = shapeProd shape✝
h_shape : { shape := shape✝, data := data✝, h_data_size := h_data_size✝ }.shape = t₂.shape
h_data : { shape := shape✝, data := data✝, h_data_size := h_data_size✝ }.data = t₂.data
⊢ { shape := shape✝, data := data✝, h_data_size := h_data_size✝ } = t₂
case mk.mk
τ : MLIRTy
shape✝¹ : List ℕ
data✝¹ : List (MLIRType.eval τ)
h_data_size✝¹ : List.length data✝¹ = shapeProd shape✝¹
shape✝ : List ℕ
data✝ : List (MLIRType.eval τ)
h_data_size✝ : List.length data✝ = shapeProd shape✝
h_shape :
  { shape := shape✝¹, data := data✝¹, h_data_size := h_data_size✝¹ }.shape =
    { shape := shape✝, data := data✝, h_data_size := h_data_size✝ }.shape
h_data :
  { shape := shape✝¹, data := data✝¹, h_data_size := h_data_size✝¹ }.data =
    { shape := shape✝, data := data✝, h_data_size := h_data_size✝ }.data
⊢ { shape := shape✝¹, data := data✝¹, h_data_size := h_data_size✝¹ } =
    { shape := shape✝, data := data✝, h_data_size := h_data_size✝ }