case none
y z : ℝ
hx : none ≠ 0
h'x : none ≠ ⊤
⊢ none ^ (y + z) = none ^ y * none ^ z

case some
y z : ℝ
x : ℝ≥0
hx : Option.some x ≠ 0
h'x : Option.some x ≠ ⊤
⊢ Option.some x ^ (y + z) = Option.some x ^ y * Option.some x ^ z
x : ℝ≥0∞
y z : ℝ
hx : x ≠ 0
h'x : x ≠ ⊤
⊢ x ^ (y + z) = x ^ y * x ^ z
cases' x with x
case some
y z : ℝ
x : ℝ≥0
hx : Option.some x ≠ 0
h'x : Option.some x ≠ ⊤
this : x ≠ 0
⊢ Option.some x ^ (y + z) = Option.some x ^ y * Option.some x ^ z
case some
y z : ℝ
x : ℝ≥0
hx : Option.some x ≠ 0
h'x : Option.some x ≠ ⊤
⊢ Option.some x ^ (y + z) = Option.some x ^ y * Option.some x ^ z
have : x ≠ 0 := fun h => by simp [h] at hx
no goals
case some
y z : ℝ
x : ℝ≥0
hx : Option.some x ≠ 0
h'x : Option.some x ≠ ⊤
this : x ≠ 0
⊢ Option.some x ^ (y + z) = Option.some x ^ y * Option.some x ^ z
simp [coe_rpow_of_ne_zero this, NNReal.rpow_add this]
no goals
case none
y z : ℝ
hx : none ≠ 0
h'x : none ≠ ⊤
⊢ none ^ (y + z) = none ^ y * none ^ z
exact (h'x rfl).elim
no goals
y z : ℝ
x : ℝ≥0
hx : Option.some x ≠ 0
h'x : Option.some x ≠ ⊤
h : x = 0
⊢ False
simp [h] at hx