trivial
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✝
h_data : data✝¹ = data✝
⊢ scale✝¹ = scale✝ ∧ data✝¹ = data✝
no goals