cases τ <;> simp [hasType] at Htype
τ : MLIRTy
i : Float
s : List ℕ
Hshape : hasShape (float i) s = true
Htype : hasType (float i) τ = true
⊢ List.length (flatten (float i) Htype) = shapeProd s
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