∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {P : Type u_3} [inst_1 : AddCommMonoid P] {g : M →+ P}
  {T : AddSubmonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T) {Q : Type u_2} [inst_2 : AddCommMonoid Q] (k : T.LocalizationMap Q)
  (y : ↥S), IsAddUnit (k ↑⟨g ↑y, ⋯⟩)