Theorem: mul_of_mul_base_exp (Notes4/Induction.lean)

State before:
a b c : ℕ
⊢ exp (a * b) c = exp a c * exp b c
Tactic:
match c with 
| 0 => simp only [exp] 
| z+1 => 
  simp only [exp,Nat.add]
  rw [mul_of_mul_base_exp a b z]
  ac_rfl
State after:
no goals

State before:
a b c : ℕ
⊢ exp (a * b) 0 = exp a 0 * exp b 0
Tactic:
simp only [exp]
State after:
no goals

State before:
a b c z : ℕ
⊢ exp (a * b) (z + 1) = exp a (z + 1) * exp b (z + 1)
Tactic:
simp only [exp,Nat.add]
State after:
a b c z : ℕ
⊢ exp (a * b) z * (a * b) = exp a z * a * (exp b z * b)

State before:
a b c z : ℕ
⊢ exp (a * b) z * (a * b) = exp a z * a * (exp b z * b)
Tactic:
rw [mul_of_mul_base_exp a b z]
State after:
a b c z : ℕ
⊢ exp a z * exp b z * (a * b) = exp a z * a * (exp b z * b)

State before:
a b c z : ℕ
⊢ exp a z * exp b z * (a * b) = exp a z * a * (exp b z * b)
Tactic:
ac_rfl
State after:
no goals