apply shapeProd_nonzero_implies_member_nonzero
shape : List ℕ
flat : TensorFlatIndex (shapeProd shape)
n : ℕ
MEMBER : List.Mem n shape
PROD_NONZERO : shapeProd shape > 0
⊢ n > 0
case MEM
shape : List ℕ
flat : TensorFlatIndex (shapeProd shape)
n : ℕ
MEMBER : List.Mem n shape
PROD_NONZERO : shapeProd shape > 0
⊢ List.Mem n ?xs

case PROD
shape : List ℕ
flat : TensorFlatIndex (shapeProd shape)
n : ℕ
MEMBER : List.Mem n shape
PROD_NONZERO : shapeProd shape > 0
⊢ shapeProd ?xs > 0

case xs
shape : List ℕ
flat : TensorFlatIndex (shapeProd shape)
n : ℕ
MEMBER : List.Mem n shape
PROD_NONZERO : shapeProd shape > 0
⊢ List ℕ