∀ {R : Type u₁} [inst : CommSemiring R] (p : ℕ) [hp : Fact (Nat.Prime p)] [inst_1 : CharP R p] {S : Type u₂}
  [inst_2 : CommSemiring S] [inst_3 : CharP S p] (φ : R →+* S) (f : Ring.Perfection R p) (n : ℕ),
  ↑((Perfection.map p φ) f) n = φ ((Perfection.coeff R p n) f)