case inl
x : ℝ≥0∞
z : ℝ
H : z < 0
⊢ ENNReal.toNNReal x ^ z = ENNReal.toNNReal (x ^ z)

case inr.inl
x : ℝ≥0∞
z : ℝ
H : z = 0
⊢ ENNReal.toNNReal x ^ z = ENNReal.toNNReal (x ^ z)

case inr.inr
x : ℝ≥0∞
z : ℝ
H : 0 < z
⊢ ENNReal.toNNReal x ^ z = ENNReal.toNNReal (x ^ z)
x : ℝ≥0∞
z : ℝ
⊢ ENNReal.toNNReal x ^ z = ENNReal.toNNReal (x ^ z)
rcases lt_trichotomy z 0 with (H | H | H)
case inl.none
z : ℝ
H : z < 0
⊢ ENNReal.toNNReal none ^ z = ENNReal.toNNReal (none ^ z)

case inl.some
z : ℝ
H : z < 0
x : ℝ≥0
⊢ ENNReal.toNNReal (Option.some x) ^ z = ENNReal.toNNReal (Option.some x ^ z)
case inl
x : ℝ≥0∞
z : ℝ
H : z < 0
⊢ ENNReal.toNNReal x ^ z = ENNReal.toNNReal (x ^ z)
cases' x with x
case pos
z : ℝ
H : z < 0
x : ℝ≥0
hx : x = 0
⊢ ENNReal.toNNReal (Option.some x) ^ z = ENNReal.toNNReal (Option.some x ^ z)

case neg
z : ℝ
H : z < 0
x : ℝ≥0
hx : ¬x = 0
⊢ ENNReal.toNNReal (Option.some x) ^ z = ENNReal.toNNReal (Option.some x ^ z)
case inl.some
z : ℝ
H : z < 0
x : ℝ≥0
⊢ ENNReal.toNNReal (Option.some x) ^ z = ENNReal.toNNReal (Option.some x ^ z)
by_cases hx : x = 0
no goals
case inl.none
z : ℝ
H : z < 0
⊢ ENNReal.toNNReal none ^ z = ENNReal.toNNReal (none ^ z)
simp [H, ne_of_lt]
no goals
case pos
z : ℝ
H : z < 0
x : ℝ≥0
hx : x = 0
⊢ ENNReal.toNNReal (Option.some x) ^ z = ENNReal.toNNReal (Option.some x ^ z)
simp [hx, H, ne_of_lt]
no goals
case neg
z : ℝ
H : z < 0
x : ℝ≥0
hx : ¬x = 0
⊢ ENNReal.toNNReal (Option.some x) ^ z = ENNReal.toNNReal (Option.some x ^ z)
simp [coe_rpow_of_ne_zero hx]
no goals
case inr.inl
x : ℝ≥0∞
z : ℝ
H : z = 0
⊢ ENNReal.toNNReal x ^ z = ENNReal.toNNReal (x ^ z)
simp [H]
case inr.inr.none
z : ℝ
H : 0 < z
⊢ ENNReal.toNNReal none ^ z = ENNReal.toNNReal (none ^ z)

case inr.inr.some
z : ℝ
H : 0 < z
val✝ : ℝ≥0
⊢ ENNReal.toNNReal (Option.some val✝) ^ z = ENNReal.toNNReal (Option.some val✝ ^ z)
case inr.inr
x : ℝ≥0∞
z : ℝ
H : 0 < z
⊢ ENNReal.toNNReal x ^ z = ENNReal.toNNReal (x ^ z)
cases x
no goals
case inr.inr.some
z : ℝ
H : 0 < z
val✝ : ℝ≥0
⊢ ENNReal.toNNReal (Option.some val✝) ^ z = ENNReal.toNNReal (Option.some val✝ ^ z)
simp [coe_rpow_of_nonneg _ (le_of_lt H)]
no goals
case inr.inr.none
z : ℝ
H : 0 < z
⊢ ENNReal.toNNReal none ^ z = ENNReal.toNNReal (none ^ z)
simp [H, ne_of_gt]