cases s <;> simp [flatten, hasShape] at *
case int
i : ℤ
s : List ℕ
Hshape : hasShape (int i) s = true
a✝¹ : Signedness
a✝ : ℕ
Htype✝ : hasType (int i) (MLIRType.int a✝¹ a✝) = true
Htype : FinInt.isInBounds a✝¹ a✝ i = true
⊢ List.length (flatten (int i) Htype✝) = shapeProd s
no goals