case inl
R : Type ?u.7555
S : Type ?u.7558
M : Type u_1
inst✝ : MonoidWithZero M
n : ℕ
h : n = 0
⊢ 0 ^ n = 1

case inr
R : Type ?u.7555
S : Type ?u.7558
M : Type u_1
inst✝ : MonoidWithZero M
n : ℕ
h : ¬n = 0
⊢ 0 ^ n = 0
R : Type ?u.7555
S : Type ?u.7558
M : Type u_1
inst✝ : MonoidWithZero M
n : ℕ
⊢ 0 ^ n = if n = 0 then 1 else 0
split_ifs with h
no goals
case inl
R : Type ?u.7555
S : Type ?u.7558
M : Type u_1
inst✝ : MonoidWithZero M
n : ℕ
h : n = 0
⊢ 0 ^ n = 1
rw [h, pow_zero]
no goals
case inr
R : Type ?u.7555
S : Type ?u.7558
M : Type u_1
inst✝ : MonoidWithZero M
n : ℕ
h : ¬n = 0
⊢ 0 ^ n = 0
rw [zero_pow (Nat.pos_of_ne_zero h)]