simp only [pth_root, h, dite_false]
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h : ringChar R ≠ 0
x : R
⊢ pth_root x ^ ringChar R = x
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h : ringChar R ≠ 0
x : R
⊢ Function.surjInv (_ : Function.Surjective fun x => x ^ ringChar R) x ^ ringChar R = x