filter_upwards [Filter.eventually_gt_atTop 0]
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ (fun x => x ^ r * x ^ ((1 - r) / 2)) =ᶠ[atTop] fun N => N * (N ^ ((1 - r) / 2))⁻¹
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
⊢ ∀ (a : ℝ), 0 < a → a ^ r * a ^ ((1 - r) / 2) = a * (a ^ ((1 - r) / 2))⁻¹