Theorem: exp_eq_exp' (Notes4/Theorems.lean)

State before:
b e : ℕ
⊢ exp b e = exp' b e
Tactic:
match e with 
| 0 => simp [exp,exp'] 
| n+1 => 
  simp only [exp,exp']
  simp only [Nat.add]
  rw [exp_eq_exp' b n]
State after:
no goals

State before:
b e : ℕ
⊢ exp b 0 = exp' b 0
Tactic:
simp [exp,exp']
State after:
no goals

State before:
b e n : ℕ
⊢ exp b (n + 1) = exp' b (n + 1)
Tactic:
simp only [exp,exp']
State after:
b e n : ℕ
⊢ exp b (Nat.add n 0) * b = exp' b (Nat.add n 0) * b

State before:
b e n : ℕ
⊢ exp b (Nat.add n 0) * b = exp' b (Nat.add n 0) * b
Tactic:
simp only [Nat.add]
State after:
b e n : ℕ
⊢ exp b n * b = exp' b n * b

State before:
b e n : ℕ
⊢ exp b n * b = exp' b n * b
Tactic:
rw [exp_eq_exp' b n]
State after:
no goals