rw [←sub_eq_zero] at *
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hn : ringChar R ≠ 0
x y : R
h : (fun x => x ^ ringChar R) x = (fun x => x ^ ringChar R) y
⊢ x = y
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hn : ringChar R ≠ 0
x y : R
h✝ : (fun x => x ^ ringChar R) x = (fun x => x ^ ringChar R) y
h : (fun x => x ^ ringChar R) x - (fun x => x ^ ringChar R) y = 0
⊢ x - y = 0