. simp only [ne_eq]
  rw [Function.surjInv_eq
        (pth_power_bijective_of_char_nonzero (by assumption)).surjective,
      zero_pow]
  rwa [zero_lt_iff]
case inr
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ (fun x => x ^ ringChar R) (Function.surjInv (_ : Function.Surjective fun x => x ^ ringChar R) 0) =
    (fun x => x ^ ringChar R) 0

case inr.inj
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ Function.Injective fun x => x ^ ringChar R
case inr.inj
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : PerfectRing R
h✝ : ¬ringChar R = 0
⊢ Function.Injective fun x => x ^ ringChar R