no goals
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type ?u.576510
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
x : R
y : { x // x ∈ M }
z₁ z₂ : S
⊢ mk' S x y + z₁ = z₂ ↔ ↑(algebraMap R S) x + z₁ * ↑(algebraMap R S) ↑y = z₂ * ↑(algebraMap R S) ↑y
rw [← mk'_spec S x y, ← IsUnit.mul_left_inj (IsLocalization.map_units S y), right_distrib]