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

State before:
a b : Nat
⊢ succ a ≤ succ b → a ≤ b
Tactic:
intro h
State after:
a b : Nat
h : succ a ≤ succ b
⊢ a ≤ b

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

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

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

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