Theorem: TensorFlatIndex.shapeProd_member_nonzero (MLIR/Util/KDTensor.lean)

State before:
shape : List ℕ
flat : TensorFlatIndex (shapeProd shape)
n : ℕ
MEMBER : List.Mem n shape
⊢ n > 0
Tactic:
have PROD_NONZERO: shapeProd shape > 0 := flat.bound_gt_zero
State after:
shape : List ℕ
flat : TensorFlatIndex (shapeProd shape)
n : ℕ
MEMBER : List.Mem n shape
PROD_NONZERO : shapeProd shape > 0
⊢ n > 0

State before:
shape : List ℕ
flat : TensorFlatIndex (shapeProd shape)
n : ℕ
MEMBER : List.Mem n shape
PROD_NONZERO : shapeProd shape > 0
⊢ n > 0
Tactic:
apply shapeProd_nonzero_implies_member_nonzero
State after:
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 ℕ

State before:
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 ℕ
Tactic:
exact MEMBER
State after:
case PROD
shape : List ℕ
flat : TensorFlatIndex (shapeProd shape)
n : ℕ
MEMBER : List.Mem n shape
PROD_NONZERO : shapeProd shape > 0
⊢ shapeProd shape > 0

State before:
case PROD
shape : List ℕ
flat : TensorFlatIndex (shapeProd shape)
n : ℕ
MEMBER : List.Mem n shape
PROD_NONZERO : shapeProd shape > 0
⊢ shapeProd shape > 0
Tactic:
exact PROD_NONZERO
State after:
no goals