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

State before:
a b t : Nat
⊢ a + t = b + t → a = b
Tactic:
induction t with
| zero =>
  rw [add_zero, add_zero]
  intro h
  exact h
| succ t' ih =>
  rw [add_succ, add_succ]
  intro h
  have ihl : a + t' = b + t' := by exact (succ_inj h)
  exact (ih ihl)
State after:
no goals

State before:
case zero
a b : Nat
⊢ a + zero = b + zero → a = b
Tactic:
rw [add_zero, add_zero]
State after:
case zero
a b : Nat
⊢ a = b → a = b

State before:
case zero
a b : Nat
⊢ a = b → a = b
Tactic:
intro h
State after:
case zero
a b : Nat
h : a = b
⊢ a = b

State before:
case zero
a b : Nat
h : a = b
⊢ a = b
Tactic:
exact h
State after:
no goals

State before:
case succ
a b t' : Nat
ih : a + t' = b + t' → a = b
⊢ a + succ t' = b + succ t' → a = b
Tactic:
rw [add_succ, add_succ]
State after:
case succ
a b t' : Nat
ih : a + t' = b + t' → a = b
⊢ succ (a + t') = succ (b + t') → a = b

State before:
case succ
a b t' : Nat
ih : a + t' = b + t' → a = b
⊢ succ (a + t') = succ (b + t') → a = b
Tactic:
intro h
State after:
case succ
a b t' : Nat
ih : a + t' = b + t' → a = b
h : succ (a + t') = succ (b + t')
⊢ a = b

State before:
case succ
a b t' : Nat
ih : a + t' = b + t' → a = b
h : succ (a + t') = succ (b + t')
⊢ a = b
Tactic:
have ihl : a + t' = b + t' := by exact (succ_inj h)
State after:
case succ
a b t' : Nat
ih : a + t' = b + t' → a = b
h : succ (a + t') = succ (b + t')
ihl : a + t' = b + t'
⊢ a = b

State before:
case succ
a b t' : Nat
ih : a + t' = b + t' → a = b
h : succ (a + t') = succ (b + t')
ihl : a + t' = b + t'
⊢ a = b
Tactic:
exact (ih ihl)
State after:
no goals

State before:
a b t' : Nat
ih : a + t' = b + t' → a = b
h : succ (a + t') = succ (b + t')
⊢ a + t' = b + t'
Tactic:
exact (succ_inj h)
State after:
no goals