case inl
y z : ℝ
hz : 0 ≤ z
hyz : z ≤ y
hx0 : 0 ≤ 0
hx1 : 0 ≤ 1
⊢ 0 ^ y ≤ 0 ^ z

case inr
x y z : ℝ
hx0 : 0 ≤ x
hx1 : x ≤ 1
hz : 0 ≤ z
hyz : z ≤ y
hx0' : 0 < x
⊢ x ^ y ≤ x ^ z
x y z : ℝ
hx0 : 0 ≤ x
hx1 : x ≤ 1
hz : 0 ≤ z
hyz : z ≤ y
⊢ x ^ y ≤ x ^ z
rcases eq_or_lt_of_le hx0 with (rfl | hx0')
case inl.inl
y : ℝ
hx0 : 0 ≤ 0
hx1 : 0 ≤ 1
hz : 0 ≤ 0
hyz : 0 ≤ y
⊢ 0 ^ y ≤ 0 ^ 0

case inl.inr
y z : ℝ
hz : 0 ≤ z
hyz : z ≤ y
hx0 : 0 ≤ 0
hx1 : 0 ≤ 1
hz' : 0 < z
⊢ 0 ^ y ≤ 0 ^ z
case inl
y z : ℝ
hz : 0 ≤ z
hyz : z ≤ y
hx0 : 0 ≤ 0
hx1 : 0 ≤ 1
⊢ 0 ^ y ≤ 0 ^ z
rcases eq_or_lt_of_le hz with (rfl | hz')
no goals
case inl.inr
y z : ℝ
hz : 0 ≤ z
hyz : z ≤ y
hx0 : 0 ≤ 0
hx1 : 0 ≤ 1
hz' : 0 < z
⊢ 0 ^ y ≤ 0 ^ z
rw [zero_rpow, zero_rpow] <;> linarith
no goals
case inl.inl
y : ℝ
hx0 : 0 ≤ 0
hx1 : 0 ≤ 1
hz : 0 ≤ 0
hyz : 0 ≤ y
⊢ 0 ^ y ≤ 0 ^ 0
exact (rpow_zero 0).symm ▸ rpow_le_one hx0 hx1 hyz
no goals
case inr
x y z : ℝ
hx0 : 0 ≤ x
hx1 : x ≤ 1
hz : 0 ≤ z
hyz : z ≤ y
hx0' : 0 < x
⊢ x ^ y ≤ x ^ z
exact rpow_le_rpow_of_exponent_ge hx0' hx1 hyz