case pos
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : p = 0
⊢ 0 < x ^ p

case neg
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : ¬p = 0
⊢ 0 < x ^ p
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
⊢ 0 < x ^ p
by_cases hp_zero : p = 0
no goals
case pos
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : p = 0
⊢ 0 < x ^ p
simp [hp_zero, zero_lt_one]
case neg
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : p ≠ 0
⊢ 0 < x ^ p
case neg
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : ¬p = 0
⊢ 0 < x ^ p
rw [← Ne.def] at hp_zero
case neg
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : p ≠ 0
hp_pos : 0 < p
⊢ 0 < x ^ p
case neg
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : p ≠ 0
⊢ 0 < x ^ p
have hp_pos := lt_of_le_of_ne hp_nonneg hp_zero.symm
case neg
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : p ≠ 0
hp_pos : 0 < p
⊢ 0 ^ p < x ^ p
case neg
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : p ≠ 0
hp_pos : 0 < p
⊢ 0 < x ^ p
rw [← zero_rpow_of_pos hp_pos]
no goals
case neg
p : ℝ
x : ℝ≥0∞
hx_pos : 0 < x
hp_nonneg : 0 ≤ p
hp_zero : p ≠ 0
hp_pos : 0 < p
⊢ 0 ^ p < x ^ p
exact rpow_lt_rpow hx_pos hp_pos