Theorem: Nat.lt_of_not_ge (Table/BuiltinExtensions.lean)

State before:
x y : Nat
h : ¬x ≥ y
⊢ x < y
Tactic:
unfold LT.lt
State after:
x y : Nat
h : ¬x ≥ y
⊢ instLTNat.1 x y

State before:
x y : Nat
h : ¬x ≥ y
⊢ instLTNat.1 x y
Tactic:
unfold instLTNat
State after:
x y : Nat
h : ¬x ≥ y
⊢ { lt := Nat.lt }.1 x y

State before:
x y : Nat
h : ¬x ≥ y
⊢ { lt := Nat.lt }.1 x y
Tactic:
unfold Nat.lt
State after:
x y : Nat
h : ¬x ≥ y
⊢ { lt := fun n m => Nat.le (succ n) m }.1 x y

State before:
x y : Nat
h : ¬x ≥ y
⊢ { lt := fun n m => Nat.le (succ n) m }.1 x y
Tactic:
simp only
State after:
x y : Nat
h : ¬x ≥ y
⊢ Nat.le (succ x) y

State before:
x y : Nat
h : ¬x ≥ y
⊢ Nat.le (succ x) y
Tactic:
have h' : Nat.le (Nat.succ x) y = ((x + 1) ≤ y) := rfl
State after:
x y : Nat
h : ¬x ≥ y
h' : Nat.le (succ x) y = (x + 1 ≤ y)
⊢ Nat.le (succ x) y

State before:
x y : Nat
h : ¬x ≥ y
h' : Nat.le (succ x) y = (x + 1 ≤ y)
⊢ Nat.le (succ x) y
Tactic:
rw [h']
State after:
x y : Nat
h : ¬x ≥ y
h' : Nat.le (succ x) y = (x + 1 ≤ y)
⊢ x + 1 ≤ y

State before:
x y : Nat
h : ¬x ≥ y
h' : Nat.le (succ x) y = (x + 1 ≤ y)
⊢ x + 1 ≤ y
Tactic:
rw [←Nat.not_le_eq]
State after:
x y : Nat
h : ¬x ≥ y
h' : Nat.le (succ x) y = (x + 1 ≤ y)
⊢ ¬y ≤ x

State before:
x y : Nat
h : ¬x ≥ y
h' : Nat.le (succ x) y = (x + 1 ≤ y)
⊢ ¬y ≤ x
Tactic:
apply h
State after:
no goals