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

State before:
a b : Nat
⊢ a ≤ b → ∀ (t : Nat), a + t ≤ b + t
Tactic:
intro h t
State after:
a b : Nat
h : a ≤ b
t : Nat
⊢ a + t ≤ b + t

State before:
a b : Nat
h : a ≤ b
t : Nat
⊢ a + t ≤ b + t
Tactic:
cases h with
| intro w pw =>
  exists w
  rw [pw]
  simp
State after:
no goals

State before:
case intro
a b t w : Nat
pw : b = a + w
⊢ a + t ≤ b + t
Tactic:
exists w
State after:
case intro
a b t w : Nat
pw : b = a + w
⊢ b + t = a + t + w

State before:
case intro
a b t w : Nat
pw : b = a + w
⊢ b + t = a + t + w
Tactic:
rw [pw]
State after:
case intro
a b t w : Nat
pw : b = a + w
⊢ a + w + t = a + t + w

State before:
case intro
a b t w : Nat
pw : b = a + w
⊢ a + w + t = a + t + w
Tactic:
simp
State after:
no goals