intros _ s H
e : TensorElem
⊢ ∀ (a : Float) (s : List ℕ), inferredShape (float a) = some s → hasShape (float a) s = true
e : TensorElem
a✝ : Float
s : List ℕ
H : inferredShape (float a✝) = some s
⊢ hasShape (float a✝) s = true