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

State before:
x n : ℕ
X_LT_N : x < n
⊢ x ≤ pred n
Tactic:
cases n
State after:
case zero
x : ℕ
X_LT_N : x < zero
⊢ x ≤ pred zero

case succ
x n✝ : ℕ
X_LT_N : x < succ n✝
⊢ x ≤ pred (succ n✝)

State before:
x : ℕ
X_LT_N : x < zero
⊢ x ≤ pred zero
Tactic:
case zero => { simp [Nat.not_lt_zero] at X_LT_N; }
State after:
no goals

State before:
x n' : ℕ
X_LT_N : x < succ n'
⊢ x ≤ pred (succ n')
Tactic:
case succ n' => {
 rewrite [Nat.pred_succ];
 apply Nat.le_of_lt_succ;
 exact X_LT_N;
}
State after:
no goals

State before:
x : ℕ
X_LT_N : x < zero
⊢ x ≤ pred zero
Tactic:
simp [Nat.not_lt_zero] at X_LT_N
State after:
no goals

State before:
x n' : ℕ
X_LT_N : x < succ n'
⊢ x ≤ pred (succ n')
Tactic:
rewrite [Nat.pred_succ]
State after:
x n' : ℕ
X_LT_N : x < succ n'
⊢ x ≤ n'

State before:
x n' : ℕ
X_LT_N : x < succ n'
⊢ x ≤ n'
Tactic:
apply Nat.le_of_lt_succ
State after:
case a
x n' : ℕ
X_LT_N : x < succ n'
⊢ x < succ n'

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