case zero
R : Type ?u.509735
n : ℕ
⊢ ↑(pow Nat.zero) n = if Nat.zero = 0 ∧ n = 0 then 0 else n ^ Nat.zero

case succ
R : Type ?u.509735
n n✝ : ℕ
⊢ ↑(pow (succ n✝)) n = if succ n✝ = 0 ∧ n = 0 then 0 else n ^ succ n✝
R : Type ?u.509735
k n : ℕ
⊢ ↑(pow k) n = if k = 0 ∧ n = 0 then 0 else n ^ k
cases k
case succ
R : Type ?u.509735
n k : ℕ
⊢ ↑(pow (succ k)) n = if succ k = 0 ∧ n = 0 then 0 else n ^ succ k
case succ
R : Type ?u.509735
n n✝ : ℕ
⊢ ↑(pow (succ n✝)) n = if succ n✝ = 0 ∧ n = 0 then 0 else n ^ succ n✝
rename_i k
no goals
case succ
R : Type ?u.509735
n k : ℕ
⊢ ↑(pow (succ k)) n = if succ k = 0 ∧ n = 0 then 0 else n ^ succ k
simp [pow, (ne_of_lt (Nat.succ_pos k)).symm]
no goals
case zero
R : Type ?u.509735
n : ℕ
⊢ ↑(pow Nat.zero) n = if Nat.zero = 0 ∧ n = 0 then 0 else n ^ Nat.zero
simp [pow]