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

State before:
a b c : Nat
⊢ a - (b + c) = a - b - c
Tactic:
apply Nat.le_antisymm (Nat.sub_le_iff_left.mpr _)
                      (Nat.sub_le_iff_left.mpr $ Nat.sub_le_iff_left.mpr _)
State after:
a b c : Nat
⊢ a ≤ b + c + (a - b - c)

a b c : Nat
⊢ a ≤ b + (c + (a - (b + c)))

State before:
a b c : Nat
⊢ a ≤ b + c + (a - b - c)

a b c : Nat
⊢ a ≤ b + (c + (a - (b + c)))
Tactic:
. rw [Nat.add_assoc]
  apply Nat.le_trans Nat.le_add_sub (Nat.add_le_add_left Nat.le_add_sub _)
State after:
a b c : Nat
⊢ a ≤ b + (c + (a - (b + c)))

State before:
a b c : Nat
⊢ a ≤ b + (c + (a - (b + c)))
Tactic:
. rw [←Nat.add_assoc]
  apply Nat.le_add_sub
State after:
no goals

State before:
a b c : Nat
⊢ a ≤ b + c + (a - b - c)
Tactic:
rw [Nat.add_assoc]
State after:
a b c : Nat
⊢ a ≤ b + (c + (a - b - c))

State before:
a b c : Nat
⊢ a ≤ b + (c + (a - b - c))
Tactic:
apply Nat.le_trans Nat.le_add_sub (Nat.add_le_add_left Nat.le_add_sub _)
State after:
no goals

State before:
a b c : Nat
⊢ a ≤ b + (c + (a - (b + c)))
Tactic:
rw [←Nat.add_assoc]
State after:
a b c : Nat
⊢ a ≤ b + c + (a - (b + c))

State before:
a b c : Nat
⊢ a ≤ b + c + (a - (b + c))
Tactic:
apply Nat.le_add_sub
State after:
no goals