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

State before:
a b : Nat
⊢ succ a = succ b ↔ a = b
Tactic:
constructor
State after:
case mp
a b : Nat
⊢ succ a = succ b → a = b

case mpr
a b : Nat
⊢ a = b → succ a = succ b

State before:
a b : Nat
⊢ succ a = succ b → a = b
Tactic:
case mp =>
  apply succ_inj
State after:
no goals

State before:
a b : Nat
⊢ a = b → succ a = succ b
Tactic:
case mpr =>
  exact succ_eq_succ_of_eq
State after:
no goals

State before:
a b : Nat
⊢ succ a = succ b → a = b
Tactic:
apply succ_inj
State after:
no goals

State before:
a b : Nat
⊢ a = b → succ a = succ b
Tactic:
exact succ_eq_succ_of_eq
State after:
no goals