Theorem: MyNat.add_le_add_left (TheoremProvingLean/inductive_types.lean)

State before:
a b : Nat
h : a ≤ b
t : Nat
⊢ t + a ≤ t + b
Tactic:
have _ : a + t ≤ b + t := add_le_add_right h t
State after:
a b : Nat
h : a ≤ b
t : Nat
x✝ : a + t ≤ b + t
⊢ t + a ≤ t + b

State before:
a b : Nat
h : a ≤ b
t : Nat
x✝ : a + t ≤ b + t
⊢ t + a ≤ t + b
Tactic:
rw [add_comm t a, add_comm t b]
State after:
a b : Nat
h : a ≤ b
t : Nat
x✝ : a + t ≤ b + t
⊢ a + t ≤ b + t

State before:
a b : Nat
h : a ≤ b
t : Nat
x✝ : a + t ≤ b + t
⊢ a + t ≤ b + t
Tactic:
assumption
State after:
no goals