Theorem: Cpdt.Chapter3.s_inj (Cpdt/Chapter3/ManualConstructors.lean)

State before:
n m : Nat
⊢ Nat.succ n = Nat.succ m → n = m
Tactic:
intro h
State after:
n m : Nat
h : Nat.succ n = Nat.succ m
⊢ n = m

State before:
n m : Nat
h : Nat.succ n = Nat.succ m
⊢ n = m
Tactic:
rw [←Nat.pred_succ n]
State after:
n m : Nat
h : Nat.succ n = Nat.succ m
⊢ Nat.pred (Nat.succ n) = m

State before:
n m : Nat
h : Nat.succ n = Nat.succ m
⊢ Nat.pred (Nat.succ n) = m
Tactic:
rw [←Nat.pred_succ m]
State after:
n m : Nat
h : Nat.succ n = Nat.succ m
⊢ Nat.pred (Nat.succ n) = Nat.pred (Nat.succ m)

State before:
n m : Nat
h : Nat.succ n = Nat.succ m
⊢ Nat.pred (Nat.succ n) = Nat.pred (Nat.succ m)
Tactic:
rw [h]
State after:
no goals