∀ {R : Type u_1} [inst : CommRing R] {ΓR : Type u_6} [inst_1 : LinearOrderedCommGroupWithZero ΓR] {vR : Valuation R ΓR}
  {S : Type u_9} {ΓS : Type u_10} [inst_2 : CommRing S] [inst_3 : LinearOrderedCommGroupWithZero ΓS]
  [inst_4 : Algebra R S] [IsLocalHom (algebraMap R S)] {vS : Valuation S ΓS} [inst_6 : vR.HasExtension vS],
  IsLocalHom (algebraMap ↥vR.integer ↥vS.integer)