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

State before:
m : Nat
⊢ m ^ one = m
Tactic:
rw [one_eq_succ_zero, pow_succ, pow_zero, one_mul]
State after:
no goals