Theorem: ECTate.PerfectRing.pth_root_pow_char (ECTate/FieldTheory/PerfectClosure.lean)

State before:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h : ringChar R ≠ 0
x : R
⊢ pth_root x ^ ringChar R = x
Tactic:
simp only [pth_root, h, dite_false]
State after:
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

State before:
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
Tactic:
exact Function.rightInverse_surjInv (pth_power_bijective_of_char_nonzero h).2 x
State after:
no goals