simp at *
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✝ }
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✝
h_data : data✝¹ = data✝
⊢ shape✝¹ = shape✝ ∧ data✝¹ = data✝