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

State before:
a b : Nat
h : a ≤ b
⊢ succ a ≤ succ b
Tactic:
cases h with
| intro w pw =>
  exists w
  rw [succ_add]
  exact (succ_eq_succ_iff.mpr pw)
State after:
no goals

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

State before:
case intro
a b w : Nat
pw : b = a + w
⊢ succ b = succ a + w
Tactic:
rw [succ_add]
State after:
case intro
a b w : Nat
pw : b = a + w
⊢ succ b = succ (a + w)

State before:
case intro
a b w : Nat
pw : b = a + w
⊢ succ b = succ (a + w)
Tactic:
exact (succ_eq_succ_iff.mpr pw)
State after:
no goals