case none
y z : ℝ
⊢ none ^ (y * z) = (none ^ y) ^ z

case some
y z : ℝ
x : ℝ≥0
⊢ Option.some x ^ (y * z) = (Option.some x ^ y) ^ z
x : ℝ≥0∞
y z : ℝ
⊢ x ^ (y * z) = (x ^ y) ^ z
cases' x with x
no goals
case none
y z : ℝ
⊢ none ^ (y * z) = (none ^ y) ^ z
rcases lt_trichotomy y 0 with (Hy | Hy | Hy) <;>
    rcases lt_trichotomy z 0 with (Hz | Hz | Hz) <;>
  simp [Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos,
    mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]
case pos
y z : ℝ
x : ℝ≥0
h : x = 0
⊢ Option.some x ^ (y * z) = (Option.some x ^ y) ^ z

case neg
y z : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ Option.some x ^ (y * z) = (Option.some x ^ y) ^ z
case some
y z : ℝ
x : ℝ≥0
⊢ Option.some x ^ (y * z) = (Option.some x ^ y) ^ z
by_cases h : x = 0
no goals
case pos
y z : ℝ
x : ℝ≥0
h : x = 0
⊢ Option.some x ^ (y * z) = (Option.some x ^ y) ^ z
rcases lt_trichotomy y 0 with (Hy | Hy | Hy) <;>
    rcases lt_trichotomy z 0 with (Hz | Hz | Hz) <;>
  simp [h, Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos,
    mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]
case neg
y z : ℝ
x : ℝ≥0
h : ¬x = 0
this : x ^ y ≠ 0
⊢ Option.some x ^ (y * z) = (Option.some x ^ y) ^ z
case neg
y z : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ Option.some x ^ (y * z) = (Option.some x ^ y) ^ z
have : x ^ y ≠ 0 := by simp [h]
no goals
case neg
y z : ℝ
x : ℝ≥0
h : ¬x = 0
this : x ^ y ≠ 0
⊢ Option.some x ^ (y * z) = (Option.some x ^ y) ^ z
simp [coe_rpow_of_ne_zero h, coe_rpow_of_ne_zero this, NNReal.rpow_mul]
no goals
y z : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ x ^ y ≠ 0
simp [h]