case nil =>
  simp [inferredShape, List.all_one]
  simp [inferredShape, bind, Option.bind, List.all_one] at H
  split at H; trivial; simp at H
  case h_2 _ s_mid H' =>
    simp [←H.1, H', H.2]
head : TensorElem
s_head : ℕ
s_tail : List ℕ
ih :
  ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested []) = some (head :: tail) →
      head = List.length [] ∧ (List.all [] fun x => decide (inferredShape x = some tail)) = true
H : inferredShape (nested [head]) = some (s_head :: s_tail)
⊢ s_head = Nat.succ (List.length []) ∧
    inferredShape head = some s_tail ∧ ∀ (x : TensorElem), x ∈ [] → inferredShape x = some s_tail
no goals