Theorem: MyNat.succ_inj (IIScExperiments/NatAddMul.lean)

State before:
a b : MyNat
h : succ a = succ b
⊢ a = b
Tactic:
suffices h : pred (succ a) = pred (succ b) by
{ rw [pred_succ, pred_succ] at h
  exact h }
State after:
a b : MyNat
h : succ a = succ b
⊢ pred (succ a) = pred (succ b)

State before:
a b : MyNat
h : succ a = succ b
⊢ pred (succ a) = pred (succ b)
Tactic:
rw [h]
State after:
no goals

State before:
a b : MyNat
h✝ : succ a = succ b
h : pred (succ a) = pred (succ b)
⊢ a = b
Tactic:
rw [pred_succ, pred_succ] at h
State after:
a b : MyNat
h✝ : succ a = succ b
h : a = b
⊢ a = b

State before:
a b : MyNat
h✝ : succ a = succ b
h : a = b
⊢ a = b
Tactic:
exact h
State after:
no goals