Theorem: zero_times (Notes4/Induction.lean)

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

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

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

State before:
α : Type
n n' : ℕ
⊢ times 0 n' = 0
Tactic:
exact zero_times
State after:
no goals