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

State before:
x₁ x₂ y₁ y₂ : Nat
⊢ x₁ ≤ x₂ → y₁ ≥ y₂ → x₁ - y₁ ≤ x₂ - y₂
Tactic:
intro hx hy
State after:
x₁ x₂ y₁ y₂ : Nat
hx : x₁ ≤ x₂
hy : y₁ ≥ y₂
⊢ x₁ - y₁ ≤ x₂ - y₂

State before:
x₁ x₂ y₁ y₂ : Nat
hx : x₁ ≤ x₂
hy : y₁ ≥ y₂
⊢ x₁ - y₁ ≤ x₂ - y₂
Tactic:
transitivity (x₂ - y₁)
State after:
case left
x₁ x₂ y₁ y₂ : Nat
hx : x₁ ≤ x₂
hy : y₁ ≥ y₂
⊢ x₁ - y₁ ≤ x₂ - y₁

case right
x₁ x₂ y₁ y₂ : Nat
hx : x₁ ≤ x₂
hy : y₁ ≥ y₂
⊢ x₂ - y₁ ≤ x₂ - y₂

State before:
case left
x₁ x₂ y₁ y₂ : Nat
hx : x₁ ≤ x₂
hy : y₁ ≥ y₂
⊢ x₁ - y₁ ≤ x₂ - y₁
Tactic:
exact Nat.sub_le_sub_right hx _
State after:
no goals

State before:
case right
x₁ x₂ y₁ y₂ : Nat
hx : x₁ ≤ x₂
hy : y₁ ≥ y₂
⊢ x₂ - y₁ ≤ x₂ - y₂
Tactic:
exact Nat.sub_le_sub_left hy _
State after:
no goals