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

State before:
n : Nat
⊢ one ^ n = one
Tactic:
induction n with
| zero => rw [pow_zero]
| succ n' ih =>
  rw [pow_succ, ih, mul_one]
State after:
no goals

State before:
case zero

⊢ one ^ zero = one
Tactic:
rw [pow_zero]
State after:
no goals

State before:
case succ
n' : Nat
ih : one ^ n' = one
⊢ one ^ succ n' = one
Tactic:
rw [pow_succ, ih, mul_one]
State after:
no goals