cases s <;> simp [flatten, hasShape] at *
case float
i : Float
s : List ℕ
Hshape : hasShape (float i) s = true
a✝ : ℕ
Htype✝ : hasType (float i) (MLIRType.float a✝) = true
Htype : True
⊢ List.length (flatten (float i) Htype✝) = shapeProd s
no goals