case some tail_shape =>
cases tail_shape <;> simp
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 tail_shape : List ℕ
⊢ (match tail_shape with
      | [] => none
      | head :: tail => if head_shape = tail then some ((head + 1) :: tail) else none) =
      some (s_head :: s_tail) →
    0 < s_head ∧ head_shape = s_tail ∧ tail_shape = (s_head - 1) :: s_tail
no goals