Theorem: Nat.le_one_minus_if_lt (MLIR/Util/KDTensor.lean)

State before:
x n : ℕ
X_LT_N : x < n
⊢ x ≤ pred n
Tactic:
rewrite [<- Nat.sub_one]
State after:
x n : ℕ
X_LT_N : x < n
⊢ x ≤ n - 1

State before:
x n : ℕ
X_LT_N : x < n
⊢ x ≤ n - 1
Tactic:
apply Nat.le_pred_if_lt
State after:
case X_LT_N
x n : ℕ
X_LT_N : x < n
⊢ x < Nat.sub n 0

State before:
case X_LT_N
x n : ℕ
X_LT_N : x < n
⊢ x < Nat.sub n 0
Tactic:
simp
State after:
case X_LT_N
x n : ℕ
X_LT_N : x < n
⊢ x < n

State before:
case X_LT_N
x n : ℕ
X_LT_N : x < n
⊢ x < n
Tactic:
exact X_LT_N
State after:
no goals