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