x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ 1 ≤ y ^ (1 / z) ↔ x ^ z ≤ y
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ≤ y ^ (1 / z) ↔ x ^ z ≤ y
nth_rw 1 [← rpow_one x]
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ (z * z⁻¹) ≤ y ^ (1 / z) ↔ x ^ z ≤ y
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ 1 ≤ y ^ (1 / z) ↔ x ^ z ≤ y
nth_rw 1 [← @_root_.mul_inv_cancel _ _ z hz.ne']
no goals
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ x ^ (z * z⁻¹) ≤ y ^ (1 / z) ↔ x ^ z ≤ y
rw [rpow_mul, ← one_div, @rpow_le_rpow_iff _ _ (1 / z) (by simp [hz])]
no goals
x y : ℝ≥0∞
z : ℝ
hz : 0 < z
⊢ 0 < 1 / z
simp [hz]