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

State before:
a b c : Nat
⊢ a - b ≤ c ↔ a ≤ b + c
Tactic:
apply Iff.intro
State after:
case mp
a b c : Nat
⊢ a - b ≤ c → a ≤ b + c

case mpr
a b c : Nat
⊢ a ≤ b + c → a - b ≤ c

State before:
case mp
a b c : Nat
⊢ a - b ≤ c → a ≤ b + c

case mpr
a b c : Nat
⊢ a ≤ b + c → a - b ≤ c
Tactic:
. intros h
  rw [Nat.add_comm]
  apply Nat.le_add_of_sub_le
  exact h
State after:
case mpr
a b c : Nat
⊢ a ≤ b + c → a - b ≤ c

State before:
case mpr
a b c : Nat
⊢ a ≤ b + c → a - b ≤ c
Tactic:
. intros h
  apply Nat.sub_le_of_le_add
  rw [Nat.add_comm]
  exact h
State after:
no goals

State before:
case mp
a b c : Nat
⊢ a - b ≤ c → a ≤ b + c
Tactic:
intros h
State after:
case mp
a b c : Nat
h : a - b ≤ c
⊢ a ≤ b + c

State before:
case mp
a b c : Nat
h : a - b ≤ c
⊢ a ≤ b + c
Tactic:
rw [Nat.add_comm]
State after:
case mp
a b c : Nat
h : a - b ≤ c
⊢ a ≤ c + b

State before:
case mp
a b c : Nat
h : a - b ≤ c
⊢ a ≤ c + b
Tactic:
apply Nat.le_add_of_sub_le
State after:
case mp.h
a b c : Nat
h : a - b ≤ c
⊢ a - b ≤ c

State before:
case mp.h
a b c : Nat
h : a - b ≤ c
⊢ a - b ≤ c
Tactic:
exact h
State after:
no goals

State before:
case mpr
a b c : Nat
⊢ a ≤ b + c → a - b ≤ c
Tactic:
intros h
State after:
case mpr
a b c : Nat
h : a ≤ b + c
⊢ a - b ≤ c

State before:
case mpr
a b c : Nat
h : a ≤ b + c
⊢ a - b ≤ c
Tactic:
apply Nat.sub_le_of_le_add
State after:
case mpr.h
a b c : Nat
h : a ≤ b + c
⊢ a ≤ c + b

State before:
case mpr.h
a b c : Nat
h : a ≤ b + c
⊢ a ≤ c + b
Tactic:
rw [Nat.add_comm]
State after:
case mpr.h
a b c : Nat
h : a ≤ b + c
⊢ a ≤ b + c

State before:
case mpr.h
a b c : Nat
h : a ≤ b + c
⊢ a ≤ b + c
Tactic:
exact h
State after:
no goals