x y z : ℝ
hx : 1 < x
x_pos : 0 < x
⊢ x ^ y ≤ x ^ z ↔ y ≤ z
x y z : ℝ
hx : 1 < x
⊢ x ^ y ≤ x ^ z ↔ y ≤ z
have x_pos : 0 < x := lt_trans zero_lt_one hx
no goals
x y z : ℝ
hx : 1 < x
x_pos : 0 < x
⊢ x ^ y ≤ x ^ z ↔ y ≤ z
rw [← log_le_log (rpow_pos_of_pos x_pos y) (rpow_pos_of_pos x_pos z), log_rpow x_pos,
  log_rpow x_pos, mul_le_mul_right (log_pos hx)]