case intro
z : ℝ
hz : z < 0
x : ℝ≥0
hx1 : 0 < ↑x
hx2 : ↑x ≤ 1
⊢ 1 ≤ ↑x ^ z
x : ℝ≥0∞
z : ℝ
hx1 : 0 < x
hx2 : x ≤ 1
hz : z < 0
⊢ 1 ≤ x ^ z
lift x to ℝ≥0 using ne_of_lt (lt_of_le_of_lt hx2 coe_lt_top)
case intro
z : ℝ
hz : z < 0
x : ℝ≥0
hx1 : 0 < x
hx2 : x ≤ 1
⊢ 1 ≤ ↑x ^ z
case intro
z : ℝ
hz : z < 0
x : ℝ≥0
hx1 : 0 < ↑x
hx2 : ↑x ≤ 1
⊢ 1 ≤ ↑x ^ z
simp only [coe_le_one_iff, coe_pos] at hx1 hx2⊢
no goals
case intro
z : ℝ
hz : z < 0
x : ℝ≥0
hx1 : 0 < x
hx2 : x ≤ 1
⊢ 1 ≤ ↑x ^ z
simp [coe_rpow_of_ne_zero (ne_of_gt hx1),
  NNReal.one_le_rpow_of_pos_of_le_one_of_nonpos hx1 hx2 (le_of_lt hz)]