Theorem: succ_times (Notes4/Induction.lean)

State before:
α : Type
n m : ℕ
⊢ times (n + 1) m = times n m + m
Tactic:
match m with 
| 0 =>
  simp [times]
| m'+1 => 
  simp [times]
  rw [@succ_times n m']
  ac_rfl
State after:
no goals

State before:
α : Type
n m : ℕ
⊢ times (n + 1) 0 = times n 0 + 0
Tactic:
simp [times]
State after:
no goals

State before:
α : Type
n m m' : ℕ
⊢ times (n + 1) (m' + 1) = times n (m' + 1) + (m' + 1)
Tactic:
simp [times]
State after:
α : Type
n m m' : ℕ
⊢ times (n + 1) m' + (n + 1) = times n m' + n + (m' + 1)

State before:
α : Type
n m m' : ℕ
⊢ times (n + 1) m' + (n + 1) = times n m' + n + (m' + 1)
Tactic:
rw [@succ_times n m']
State after:
α : Type
n m m' : ℕ
⊢ times n m' + m' + (n + 1) = times n m' + n + (m' + 1)

State before:
α : Type
n m m' : ℕ
⊢ times n m' + m' + (n + 1) = times n m' + n + (m' + 1)
Tactic:
ac_rfl
State after:
no goals