case cons s_head' s_tail' =>
apply dite (head_shape = s_tail')
. intros Heq; rw [Heq]; simp
  intros H H'; rw [←H, Nat.add_sub_self_right, ←H']
  exact ⟨by simp_arith, rfl, rfl, rfl⟩
. intros Hne; simp [Hne]
head mid : TensorElem
tail : List TensorElem
s_head : ℕ
s_tail head_shape : List ℕ
s_head' : ℕ
s_tail' : List ℕ
⊢ (if head_shape = s_tail' then some ((s_head' + 1) :: s_tail') else none) = some (s_head :: s_tail) →
    0 < s_head ∧ head_shape = s_tail ∧ s_head' = s_head - 1 ∧ s_tail' = s_tail
no goals