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

State before:
x y n : ℕ
LE : x ≤ pred n
⊢ x * y ≤ n * y - y
Tactic:
cases H:n
State after:
case zero
x y n : ℕ
LE : x ≤ pred n
H : n = zero
⊢ x * y ≤ zero * y - y

case succ
x y n : ℕ
LE : x ≤ pred n
n✝ : ℕ
H : n = succ n✝
⊢ x * y ≤ succ n✝ * y - y

State before:
x y n : ℕ
LE : x ≤ pred n
H : n = zero
⊢ x * y ≤ zero * y - y
Tactic:
case zero => {
rewrite [H] at LE;
simp at LE;
rewrite [LE];
simp;
}
State after:
no goals

State before:
x y n : ℕ
LE : x ≤ pred n
n' : ℕ
H : n = succ n'
⊢ x * y ≤ succ n' * y - y
Tactic:
case succ n' => {
simp at LE;
rewrite [H] at LE;
simp at LE;
sorry; }
State after:
no goals

State before:
x y n : ℕ
LE : x ≤ pred n
H : n = zero
⊢ x * y ≤ zero * y - y
Tactic:
rewrite [H] at LE
State after:
x y n : ℕ
LE : x ≤ pred zero
H : n = zero
⊢ x * y ≤ zero * y - y

State before:
x y n : ℕ
LE : x ≤ pred zero
H : n = zero
⊢ x * y ≤ zero * y - y
Tactic:
simp at LE
State after:
x y n : ℕ
H : n = zero
LE : x = 0
⊢ x * y ≤ zero * y - y

State before:
x y n : ℕ
H : n = zero
LE : x = 0
⊢ x * y ≤ zero * y - y
Tactic:
rewrite [LE]
State after:
x y n : ℕ
H : n = zero
LE : x = 0
⊢ 0 * y ≤ zero * y - y

State before:
x y n : ℕ
H : n = zero
LE : x = 0
⊢ 0 * y ≤ zero * y - y
Tactic:
simp
State after:
no goals

State before:
x y n : ℕ
LE : x ≤ pred n
n' : ℕ
H : n = succ n'
⊢ x * y ≤ succ n' * y - y
Tactic:
rewrite [H] at LE
State after:
x y n n' : ℕ
LE : x ≤ pred (succ n')
H : n = succ n'
⊢ x * y ≤ succ n' * y - y

State before:
x y n n' : ℕ
LE : x ≤ pred (succ n')
H : n = succ n'
⊢ x * y ≤ succ n' * y - y
Tactic:
simp at LE
State after:
x y n n' : ℕ
LE : x ≤ n'
H : n = succ n'
⊢ x * y ≤ succ n' * y - y

State before:
x y n n' : ℕ
LE : x ≤ n'
H : n = succ n'
⊢ x * y ≤ succ n' * y - y
Tactic:
sorry
State after:
no goals