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

State before:
⊢ ∀ (m k n : Nat), k < m → n > 0 → m - (k + n) < m - k
Tactic:
intros m k n hkm hn
State after:
m k n : Nat
hkm : k < m
hn : n > 0
⊢ m - (k + n) < m - k

State before:
m k n : Nat
hkm : k < m
hn : n > 0
⊢ m - (k + n) < m - k
Tactic:
apply Nat.lt_of_le_of_lt (m := m - k - n)
State after:
case h₁
m k n : Nat
hkm : k < m
hn : n > 0
⊢ m - (k + n) ≤ m - k - n

case h₂
m k n : Nat
hkm : k < m
hn : n > 0
⊢ m - k - n < m - k

State before:
case h₁
m k n : Nat
hkm : k < m
hn : n > 0
⊢ m - (k + n) ≤ m - k - n

case h₂
m k n : Nat
hkm : k < m
hn : n > 0
⊢ m - k - n < m - k
Tactic:
. apply Nat.le_of_eq (@Nat.sub_add_eq_sub_sub m k n)
State after:
case h₂
m k n : Nat
hkm : k < m
hn : n > 0
⊢ m - k - n < m - k

State before:
case h₂
m k n : Nat
hkm : k < m
hn : n > 0
⊢ m - k - n < m - k
Tactic:
. apply Nat.sub_lt
  . exact Nat.zero_lt_sub_of_lt hkm
  . exact hn
State after:
no goals

State before:
case h₁
m k n : Nat
hkm : k < m
hn : n > 0
⊢ m - (k + n) ≤ m - k - n
Tactic:
apply Nat.le_of_eq (@Nat.sub_add_eq_sub_sub m k n)
State after:
no goals

State before:
case h₂
m k n : Nat
hkm : k < m
hn : n > 0
⊢ m - k - n < m - k
Tactic:
apply Nat.sub_lt
State after:
case h₂.a
m k n : Nat
hkm : k < m
hn : n > 0
⊢ 0 < m - k

case h₂.a
m k n : Nat
hkm : k < m
hn : n > 0
⊢ 0 < n

State before:
case h₂.a
m k n : Nat
hkm : k < m
hn : n > 0
⊢ 0 < m - k

case h₂.a
m k n : Nat
hkm : k < m
hn : n > 0
⊢ 0 < n
Tactic:
. exact Nat.zero_lt_sub_of_lt hkm
State after:
case h₂.a
m k n : Nat
hkm : k < m
hn : n > 0
⊢ 0 < n

State before:
case h₂.a
m k n : Nat
hkm : k < m
hn : n > 0
⊢ 0 < n
Tactic:
. exact hn
State after:
no goals

State before:
case h₂.a
m k n : Nat
hkm : k < m
hn : n > 0
⊢ 0 < m - k
Tactic:
exact Nat.zero_lt_sub_of_lt hkm
State after:
no goals

State before:
case h₂.a
m k n : Nat
hkm : k < m
hn : n > 0
⊢ 0 < n
Tactic:
exact hn
State after:
no goals