Theorem: Nat.zero_pow_of_nonzero (GMLInit/Data/Nat/Pow.lean)

State before:
x : Nat
⊢ x ≠ 0 → 0 ^ x = 0
Tactic:
cases x with
| zero => intro; contradiction
| succ x => intro; rw [Nat.zero_pow_succ]
State after:
no goals

State before:
case zero

⊢ 0 ≠ 0 → 0 ^ 0 = 0
Tactic:
intro
State after:
case zero
a✝ : 0 ≠ 0
⊢ 0 ^ 0 = 0

State before:
case zero
a✝ : 0 ≠ 0
⊢ 0 ^ 0 = 0
Tactic:
contradiction
State after:
no goals

State before:
case succ
x : Nat
⊢ x + 1 ≠ 0 → 0 ^ (x + 1) = 0
Tactic:
intro
State after:
case succ
x : Nat
a✝ : x + 1 ≠ 0
⊢ 0 ^ (x + 1) = 0

State before:
case succ
x : Nat
a✝ : x + 1 ≠ 0
⊢ 0 ^ (x + 1) = 0
Tactic:
rw [Nat.zero_pow_succ]
State after:
no goals