∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : IsLocalRing R] [inst_2 : CommRing S]
  [inst_3 : IsLocalRing S] (f : R →+* S) [inst_4 : IsLocalHom f],
  (IsLocalRing.ResidueField.map f).comp (IsLocalRing.residue R) = (IsLocalRing.residue S).comp f