∀ (A : Type u_1) (B : Type u_2) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : ValuativeRel A]
  [inst_3 : ValuativeRel B] [inst_4 : Algebra A B] [inst_5 : ValuativeExtension A B]
  (x : ↥(ValuativeRel.posSubmonoid A)), ↑((ValuativeExtension.mapPosSubmonoid A B) x) = (algebraMap A B) ↑x