case cons head tail ih =>
  intros s_head s_tail H
  cases tail
  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]
  case cons mid tail =>
    let H' := inferredShape_cons_inv H
    specialize (ih H'.2.2)
    constructor
    . have helper: forall {n m}, n > 0 → n - 1 = m → n = m + 1 := by
        sorry
      simp [helper H'.1 ih.1]
    . sorry
head : TensorElem
tail : List TensorElem
ih :
  ∀ {head : ℕ} {tail_1 : List ℕ},
    inferredShape (nested tail) = some (head :: tail_1) →
      head = List.length tail ∧ (List.all tail fun x => decide (inferredShape x = some tail_1)) = true
⊢ ∀ {head_1 : ℕ} {tail_1 : List ℕ},
    inferredShape (nested (head :: tail)) = some (head_1 :: tail_1) →
      head_1 = Nat.succ (List.length tail) ∧
        inferredShape head = some tail_1 ∧ ∀ (x : TensorElem), x ∈ tail → inferredShape x = some tail_1
no goals