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

State before:
bound : ℕ
flat : TensorFlatIndex bound
⊢ bound > 0
Tactic:
have BOUND_NONZERO: bound ≠ 0 := TensorFlatIndex.bound_non_zero flat
State after:
bound : ℕ
flat : TensorFlatIndex bound
BOUND_NONZERO : bound ≠ 0
⊢ bound > 0

State before:
bound : ℕ
flat : TensorFlatIndex bound
BOUND_NONZERO : bound ≠ 0
⊢ bound > 0
Tactic:
cases bound
State after:
case zero
flat : TensorFlatIndex Nat.zero
BOUND_NONZERO : Nat.zero ≠ 0
⊢ Nat.zero > 0

case succ
n✝ : ℕ
flat : TensorFlatIndex (Nat.succ n✝)
BOUND_NONZERO : Nat.succ n✝ ≠ 0
⊢ Nat.succ n✝ > 0

State before:
flat : TensorFlatIndex Nat.zero
BOUND_NONZERO : Nat.zero ≠ 0
⊢ Nat.zero > 0
Tactic:
case zero => {
  simp [Nat.zero, BOUND_NONZERO];
  contradiction;
}
State after:
no goals

State before:
bound' : ℕ
flat : TensorFlatIndex (Nat.succ bound')
BOUND_NONZERO : Nat.succ bound' ≠ 0
⊢ Nat.succ bound' > 0
Tactic:
case succ bound' => {
  apply Nat.succ_gt_zero;
}
State after:
no goals

State before:
flat : TensorFlatIndex Nat.zero
BOUND_NONZERO : Nat.zero ≠ 0
⊢ Nat.zero > 0
Tactic:
simp [Nat.zero, BOUND_NONZERO]
State after:
flat : TensorFlatIndex Nat.zero
BOUND_NONZERO : Nat.zero ≠ 0
⊢ False

State before:
flat : TensorFlatIndex Nat.zero
BOUND_NONZERO : Nat.zero ≠ 0
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
bound' : ℕ
flat : TensorFlatIndex (Nat.succ bound')
BOUND_NONZERO : Nat.succ bound' ≠ 0
⊢ Nat.succ bound' > 0
Tactic:
apply Nat.succ_gt_zero
State after:
no goals