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

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

case mpr
t a b : Nat
⊢ a = b → a + t = b + t

State before:
t a b : Nat
⊢ a + t = b + t → a = b
Tactic:
case mp =>
  exact add_right_cancel
State after:
no goals

State before:
t a b : Nat
⊢ a = b → a + t = b + t
Tactic:
case mpr =>
  intro h
  rw [h]
State after:
no goals

State before:
t a b : Nat
⊢ a + t = b + t → a = b
Tactic:
exact add_right_cancel
State after:
no goals

State before:
t a b : Nat
⊢ a = b → a + t = b + t
Tactic:
intro h
State after:
t a b : Nat
h : a = b
⊢ a + t = b + t

State before:
t a b : Nat
h : a = b
⊢ a + t = b + t
Tactic:
rw [h]
State after:
no goals