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

State before:
bound : ℕ
flat : TensorFlatIndex bound
⊢ bound ≠ 0
Tactic:
intros BOUND
State after:
bound : ℕ
flat : TensorFlatIndex bound
BOUND : bound = 0
⊢ False

State before:
bound : ℕ
flat : TensorFlatIndex bound
BOUND : bound = 0
⊢ False
Tactic:
have H_INBOUND := flat.h_ix_inbound
State after:
bound : ℕ
flat : TensorFlatIndex bound
BOUND : bound = 0
H_INBOUND : flat.ix < bound
⊢ False

State before:
bound : ℕ
flat : TensorFlatIndex bound
BOUND : bound = 0
H_INBOUND : flat.ix < bound
⊢ False
Tactic:
simp [BOUND] at H_INBOUND
State after:
no goals