y : ℝ
hy : 0 < y
⊢ OrderIso.symm
      (StrictMono.orderIsoOfRightInverse (fun x => x ^ y) (_ : StrictMono fun x => x ^ y) (fun x => x ^ (1 / y))
        (_ : ∀ (x : ℝ≥0∞), (fun x => x ^ y) ((fun x => x ^ (1 / y)) x) = x)) =
    StrictMono.orderIsoOfRightInverse (fun x => x ^ (1 / y)) (_ : StrictMono fun x => x ^ (1 / y)) (fun x => x ^ y)
      (_ : Function.RightInverse (fun x => x ^ y) fun x => x ^ (1 / y))
y : ℝ
hy : 0 < y
⊢ OrderIso.symm (orderIsoRpow y hy) = orderIsoRpow (1 / y) (_ : 0 < 1 / y)
simp only [orderIsoRpow, one_div_one_div]
no goals
y : ℝ
hy : 0 < y
⊢ OrderIso.symm
      (StrictMono.orderIsoOfRightInverse (fun x => x ^ y) (_ : StrictMono fun x => x ^ y) (fun x => x ^ (1 / y))
        (_ : ∀ (x : ℝ≥0∞), (fun x => x ^ y) ((fun x => x ^ (1 / y)) x) = x)) =
    StrictMono.orderIsoOfRightInverse (fun x => x ^ (1 / y)) (_ : StrictMono fun x => x ^ (1 / y)) (fun x => x ^ y)
      (_ : Function.RightInverse (fun x => x ^ y) fun x => x ^ (1 / y))
rfl