no goals
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type ?u.871897
inst✝ : CommMonoid P
f : LocalizationMap S N
a₁ b₁ : M
a₂ b₂ : { x // x ∈ S }
⊢ mk' f a₁ a₂ = mk' f b₁ b₂ ↔ ↑(Localization.r S) (a₁, a₂) (b₁, b₂)
rw [f.eq, Localization.r_iff_exists]