trans (N ^ (1 : ℝ) * (N ^ ((1-r)/2 : ℝ))⁻¹)
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
N : ℝ
hN : 0 < N
⊢ N ^ r * N ^ ((1 - r) / 2) = N * (N ^ ((1 - r) / 2))⁻¹
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
N : ℝ
hN : 0 < N
⊢ N ^ r * N ^ ((1 - r) / 2) = N ^ 1 * (N ^ ((1 - r) / 2))⁻¹

x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
k r : ℝ
hr : r < 1
N : ℝ
hN : 0 < N
⊢ N ^ 1 * (N ^ ((1 - r) / 2))⁻¹ = N * (N ^ ((1 - r) / 2))⁻¹