∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {R : Type u₁} [inst : CommSemiring R] [inst_1 : CharP R p] [PerfectRing R p]
  {S : Type u₂} [inst_3 : CommSemiring S] [inst_4 : CharP S p] {f g : R →+* Ring.Perfection S p},
  (∀ (x : R), (Perfection.coeff S p 0) (f x) = (Perfection.coeff S p 0) (g x)) → f = g