Theorem: Nat.sub_lt_sub_of_lt_left (GMLInit/Data/Nat/Sub.lean)

State before:
x y z : Nat
⊢ x < y → z < y → x - z < y - z
Tactic:
intro hx hz
State after:
x y z : Nat
hx : x < y
hz : z < y
⊢ x - z < y - z

State before:
x y z : Nat
hx : x < y
hz : z < y
⊢ x - z < y - z
Tactic:
apply Nat.lt_sub_of_add_lt
State after:
case h
x y z : Nat
hx : x < y
hz : z < y
⊢ x - z + z < y

State before:
case h
x y z : Nat
hx : x < y
hz : z < y
⊢ x - z + z < y
Tactic:
cases Nat.le_total x z with
| inl h => rw [Nat.sub_eq_zero_of_le h, Nat.zero_add]; exact hz
| inr h => rw [Nat.add_comm, Nat.add_sub_comm, Nat.sub_eq_zero_of_le h, Nat.add_zero]; exact hx
State after:
no goals

State before:
case h.inl
x y z : Nat
hx : x < y
hz : z < y
h : x ≤ z
⊢ x - z + z < y
Tactic:
rw [Nat.sub_eq_zero_of_le h, Nat.zero_add]
State after:
case h.inl
x y z : Nat
hx : x < y
hz : z < y
h : x ≤ z
⊢ z < y

State before:
case h.inl
x y z : Nat
hx : x < y
hz : z < y
h : x ≤ z
⊢ z < y
Tactic:
exact hz
State after:
no goals

State before:
case h.inr
x y z : Nat
hx : x < y
hz : z < y
h : z ≤ x
⊢ x - z + z < y
Tactic:
rw [Nat.add_comm, Nat.add_sub_comm, Nat.sub_eq_zero_of_le h, Nat.add_zero]
State after:
case h.inr
x y z : Nat
hx : x < y
hz : z < y
h : z ≤ x
⊢ x < y

State before:
case h.inr
x y z : Nat
hx : x < y
hz : z < y
h : z ≤ x
⊢ x < y
Tactic:
exact hx
State after:
no goals