case inl
y z : ℝ
h : y + z ≠ 0
hx : 0 ≤ 0
⊢ 0 ^ (y + z) = 0 ^ y * 0 ^ z

case inr
x y z : ℝ
hx : 0 ≤ x
h : y + z ≠ 0
pos : 0 < x
⊢ x ^ (y + z) = x ^ y * x ^ z
x y z : ℝ
hx : 0 ≤ x
h : y + z ≠ 0
⊢ x ^ (y + z) = x ^ y * x ^ z
rcases hx.eq_or_lt with (rfl | pos)
case inl
y z : ℝ
h : y + z ≠ 0
hx : 0 ≤ 0
⊢ 0 ^ y = 0 ∨ 0 ^ z = 0
case inl
y z : ℝ
h : y + z ≠ 0
hx : 0 ≤ 0
⊢ 0 ^ (y + z) = 0 ^ y * 0 ^ z
rw [zero_rpow h, zero_eq_mul]
case inl
y z : ℝ
h : y + z ≠ 0
hx : 0 ≤ 0
this : y ≠ 0 ∨ z ≠ 0
⊢ 0 ^ y = 0 ∨ 0 ^ z = 0
case inl
y z : ℝ
h : y + z ≠ 0
hx : 0 ≤ 0
⊢ 0 ^ y = 0 ∨ 0 ^ z = 0
have : y ≠ 0 ∨ z ≠ 0 := not_and_or.1 fun ⟨hy, hz⟩ => h <| hy.symm ▸ hz.symm ▸ zero_add 0
no goals
case inl
y z : ℝ
h : y + z ≠ 0
hx : 0 ≤ 0
this : y ≠ 0 ∨ z ≠ 0
⊢ 0 ^ y = 0 ∨ 0 ^ z = 0
exact this.imp zero_rpow zero_rpow
no goals
case inr
x y z : ℝ
hx : 0 ≤ x
h : y + z ≠ 0
pos : 0 < x
⊢ x ^ (y + z) = x ^ y * x ^ z
exact rpow_add pos _ _