case inl
z : ℝ
h_one_le : 1 ≤ z
hx : ⊥ ≤ 1
⊢ ⊥ ^ z ≤ ⊥

case inr
x : ℝ≥0
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
h : 0 < x
⊢ x ^ z ≤ x
x : ℝ≥0
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
⊢ x ^ z ≤ x
rcases eq_bot_or_bot_lt x with (rfl | (h : 0 < x))
case inr
x : ℝ≥0
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
h : 0 < x
⊢ x ^ z ≤ x ^ 1
case inr
x : ℝ≥0
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
h : 0 < x
⊢ x ^ z ≤ x
nth_rw 2 [← NNReal.rpow_one x]
no goals
case inr
x : ℝ≥0
z : ℝ
hx : x ≤ 1
h_one_le : 1 ≤ z
h : 0 < x
⊢ x ^ z ≤ x ^ 1
exact NNReal.rpow_le_rpow_of_exponent_ge h hx h_one_le
case inl
z : ℝ
h_one_le : 1 ≤ z
hx : ⊥ ≤ 1
this : z ≠ 0
⊢ ⊥ ^ z ≤ ⊥
case inl
z : ℝ
h_one_le : 1 ≤ z
hx : ⊥ ≤ 1
⊢ ⊥ ^ z ≤ ⊥
have : z ≠ 0 := by linarith
no goals
case inl
z : ℝ
h_one_le : 1 ≤ z
hx : ⊥ ≤ 1
this : z ≠ 0
⊢ ⊥ ^ z ≤ ⊥
simp [this]
no goals
z : ℝ
h_one_le : 1 ≤ z
hx : ⊥ ≤ 1
⊢ z ≠ 0
linarith