Theorem: MyNat.mul_pow (TheoremProvingLean/inductive_types.lean)

State before:
a b n : Nat
⊢ (a * b) ^ n = a ^ n * b ^ n
Tactic:
induction n with
| zero =>
  repeat (rw [pow_zero])
  rw [mul_one]
| succ n' ih =>
  rw [pow_succ, ih]
  repeat (rw [pow_succ])
  simp
State after:
no goals

State before:
case zero
a b : Nat
⊢ (a * b) ^ zero = a ^ zero * b ^ zero
Tactic:
repeat (rw [pow_zero])
State after:
case zero
a b : Nat
⊢ one = one * one

State before:
case zero
a b : Nat
⊢ one = one * one
Tactic:
rw [mul_one]
State after:
no goals

State before:
case zero
a b : Nat
⊢ one = one * b ^ zero
Tactic:
(rw [pow_zero])
State after:
case zero
a b : Nat
⊢ one = one * one

State before:
case zero
a b : Nat
⊢ one = one * b ^ zero
Tactic:
rw [pow_zero]
State after:
case zero
a b : Nat
⊢ one = one * one

State before:
case succ
a b n' : Nat
ih : (a * b) ^ n' = a ^ n' * b ^ n'
⊢ (a * b) ^ succ n' = a ^ succ n' * b ^ succ n'
Tactic:
rw [pow_succ, ih]
State after:
case succ
a b n' : Nat
ih : (a * b) ^ n' = a ^ n' * b ^ n'
⊢ a ^ n' * b ^ n' * (a * b) = a ^ succ n' * b ^ succ n'

State before:
case succ
a b n' : Nat
ih : (a * b) ^ n' = a ^ n' * b ^ n'
⊢ a ^ n' * b ^ n' * (a * b) = a ^ succ n' * b ^ succ n'
Tactic:
repeat (rw [pow_succ])
State after:
case succ
a b n' : Nat
ih : (a * b) ^ n' = a ^ n' * b ^ n'
⊢ a ^ n' * b ^ n' * (a * b) = a ^ n' * a * (b ^ n' * b)

State before:
case succ
a b n' : Nat
ih : (a * b) ^ n' = a ^ n' * b ^ n'
⊢ a ^ n' * b ^ n' * (a * b) = a ^ n' * a * (b ^ n' * b)
Tactic:
simp
State after:
no goals

State before:
case succ
a b n' : Nat
ih : (a * b) ^ n' = a ^ n' * b ^ n'
⊢ a ^ n' * b ^ n' * (a * b) = a ^ n' * a * b ^ succ n'
Tactic:
(rw [pow_succ])
State after:
case succ
a b n' : Nat
ih : (a * b) ^ n' = a ^ n' * b ^ n'
⊢ a ^ n' * b ^ n' * (a * b) = a ^ n' * a * (b ^ n' * b)

State before:
case succ
a b n' : Nat
ih : (a * b) ^ n' = a ^ n' * b ^ n'
⊢ a ^ n' * b ^ n' * (a * b) = a ^ n' * a * b ^ succ n'
Tactic:
rw [pow_succ]
State after:
case succ
a b n' : Nat
ih : (a * b) ^ n' = a ^ n' * b ^ n'
⊢ a ^ n' * b ^ n' * (a * b) = a ^ n' * a * (b ^ n' * b)