∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {X : Type u_2}
  [inst_2 : AddAction R X] (r₁ : R) (r₂ : X) (s₁ s₂ u : ↥S) (v : R),
  ↑u + r₁ = v + ↑s₂ → OreLocalization.vadd'✝ r₁ s₁ r₂ s₂ = (v +ᵥ r₂) -ₒ (u + s₁)