cases v₂
case mk
τ fixed : List ℕ
scalable : MLIRTy
v₂ : Vector τ fixed scalable
scale✝ : List ℕ
data✝ : List (MLIRType.eval scalable)
h_scale_size✝ : List.length scale✝ = List.length fixed
h_data_size✝ : List.length data✝ = size τ fixed scale✝ h_scale_size✝
h_scale :
  { scale := scale✝, data := data✝, h_scale_size := h_scale_size✝, h_data_size := h_data_size✝ }.scale = v₂.scale
h_data : { scale := scale✝, data := data✝, h_scale_size := h_scale_size✝, h_data_size := h_data_size✝ }.data = v₂.data
⊢ { scale := scale✝, data := data✝, h_scale_size := h_scale_size✝, h_data_size := h_data_size✝ } = v₂
case mk.mk
τ fixed : List ℕ
scalable : MLIRTy
scale✝¹ : List ℕ
data✝¹ : List (MLIRType.eval scalable)
h_scale_size✝¹ : List.length scale✝¹ = List.length fixed
h_data_size✝¹ : List.length data✝¹ = size τ fixed scale✝¹ h_scale_size✝¹
scale✝ : List ℕ
data✝ : List (MLIRType.eval scalable)
h_scale_size✝ : List.length scale✝ = List.length fixed
h_data_size✝ : List.length data✝ = size τ fixed scale✝ h_scale_size✝
h_scale :
  { scale := scale✝¹, data := data✝¹, h_scale_size := h_scale_size✝¹, h_data_size := h_data_size✝¹ }.scale =
    { scale := scale✝, data := data✝, h_scale_size := h_scale_size✝, h_data_size := h_data_size✝ }.scale
h_data :
  { scale := scale✝¹, data := data✝¹, h_scale_size := h_scale_size✝¹, h_data_size := h_data_size✝¹ }.data =
    { scale := scale✝, data := data✝, h_scale_size := h_scale_size✝, h_data_size := h_data_size✝ }.data
⊢ { scale := scale✝¹, data := data✝¹, h_scale_size := h_scale_size✝¹, h_data_size := h_data_size✝¹ } =
    { scale := scale✝, data := data✝, h_scale_size := h_scale_size✝, h_data_size := h_data_size✝ }