case pos
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : p = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

case neg
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
by_cases hp0 : p = 0
case pos
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
hx0 : x = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)

case neg
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
hx0 : ¬x = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
case neg
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
by_cases hx0 : x = 0
case neg
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
hx0 : x ≠ 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
case neg
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
hx0 : ¬x = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
rw [← Ne.def] at hx0
no goals
case neg
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
hx0 : x ≠ 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
exact ofReal_rpow_of_pos (hx_nonneg.lt_of_ne hx0.symm)
no goals
case pos
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : p = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
simp [hp0]
case pos
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : p ≠ 0
hx0 : x = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
case pos
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : ¬p = 0
hx0 : x = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
rw [← Ne.def] at hp0
case pos
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : p ≠ 0
hx0 : x = 0
hp_pos : 0 < p
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
case pos
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : p ≠ 0
hx0 : x = 0
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
have hp_pos : 0 < p := lt_of_le_of_ne hp_nonneg hp0.symm
no goals
case pos
x p : ℝ
hx_nonneg : 0 ≤ x
hp_nonneg : 0 ≤ p
hp0 : p ≠ 0
hx0 : x = 0
hp_pos : 0 < p
⊢ ENNReal.ofReal x ^ p = ENNReal.ofReal (x ^ p)
simp [hx0, hp_pos, hp_pos.ne.symm]