case intro
z : ℝ
hz : 0 ≤ z
x : ℝ≥0
hx : ↑x ≤ 1
⊢ ↑x ^ z ≤ 1
x : ℝ≥0∞
z : ℝ
hx : x ≤ 1
hz : 0 ≤ z
⊢ x ^ z ≤ 1
lift x to ℝ≥0 using ne_of_lt (lt_of_le_of_lt hx coe_lt_top)
case intro
z : ℝ
hz : 0 ≤ z
x : ℝ≥0
hx : x ≤ 1
⊢ ↑x ^ z ≤ 1
case intro
z : ℝ
hz : 0 ≤ z
x : ℝ≥0
hx : ↑x ≤ 1
⊢ ↑x ^ z ≤ 1
simp only [coe_le_one_iff] at hx
no goals
case intro
z : ℝ
hz : 0 ≤ z
x : ℝ≥0
hx : x ≤ 1
⊢ ↑x ^ z ≤ 1
simp [coe_rpow_of_nonneg _ hz, NNReal.rpow_le_one hx hz]