no goals
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type ?u.851307
inst✝ : CommMonoid P
f : LocalizationMap S N
x₁ x₂ : M
y₁ y₂ : { x // x ∈ S }
⊢ mk' f x₁ y₁ = mk' f x₂ y₂ ↔ ↑(toMap f) (x₁ * ↑y₂) = ↑(toMap f) (x₂ * ↑y₁)
simp only [f.mk'_eq_iff_eq, mul_comm]