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
x✝¹ : Option (List ℕ)
x✝ : List ℕ → Option (List ℕ)
s_mid : List ℕ
H' : inferredShape head = some s_mid
H : 1 = s_head ∧ s_mid = s_tail
⊢ s_head = Nat.succ 0 ∧ inferredShape head = some s_tail
no goals