Theorem: times_comm (Notes4/Induction.lean)

State before:
α : Type
n m : ℕ
⊢ times n m = times m n
Tactic:
match n,m with 
| n, 0 => 
  simp [times]
  | n, m'+1 => 
  simp [times]
  rw [times_comm n m']
State after:
no goals

State before:
α : Type
n✝ m n : ℕ
⊢ times n 0 = times 0 n
Tactic:
simp [times]
State after:
no goals

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

State before:
α : Type
n✝ m n m' : ℕ
⊢ times n m' + n = times m' n + n
Tactic:
rw [times_comm n m']
State after:
no goals