∀ {M : Type u_1} [inst : CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoidWithZero N]
  {P : Type u_3} [inst_2 : CommMonoidWithZero P] (f : S.LocalizationMap N) (g : M →*₀ P)
  (hg : ∀ (y : ↥S), IsUnit (g ↑y)) (x : N),
  (f.lift₀ g hg) x = g (f.sec x).1 * ↑((IsUnit.liftRight ((↑g).restrict S) hg) (f.sec x).2)⁻¹