∀ {M : Type u_1} {N : Type u_2} [inst : AddCommMonoid M] {S : AddSubmonoid M} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) (n₁ : N) (motive : (∃ x, n₁ + f ↑x.2 = f x.1) → Prop) (x : ∃ x, n₁ + f ↑x.2 = f x.1),
  (∀ (ms₁ : M × ↥S) (eq₁ : n₁ + f ↑ms₁.2 = f ms₁.1), motive ⋯) → motive x