∀ {R : Type u_1} [inst : AddMonoid R] (S : AddSubmonoid R) [inst_1 : AddOreLocalization.AddOreSet S] (X : Type u_2)
  [inst_2 : AddAction R X],
  (∀ (s s' : ↥S), AddCommute s s') →
    (∀ (x : X) (s s' : ↥S), s +ᵥ x = s' +ᵥ x → AddCommute s s' → x -ₒ s = x -ₒ s') →
      ∀ (hsurj : Function.Surjective fun x => x.1 -ₒ x.2),
        (Function.RightInverse (Function.surjInv hsurj) fun x => x.1 -ₒ x.2) →
          ∀ ⦃a₁ a₂ : AddOreLocalization S X⦄,
            ((fun x => (x.1, x.2 +ᵥ x.1)) ∘ Function.surjInv hsurj) a₁ =
                ((fun x => (x.1, x.2 +ᵥ x.1)) ∘ Function.surjInv hsurj) a₂ →
              a₁ = a₂