case nil =>
  cases inferredShape head <;> simp [bind, Option.bind]
head : TensorElem
⊢ (do
        let __do_lift ← inferredShape head
        some (1 :: __do_lift)) =
      some [] →
    False
no goals