no goals
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type ?u.908945
inst✝ : CommMonoid P
f : LocalizationMap S N
a₁ b₁ : M
a₂ b₂ : { x // x ∈ S }
H : b₁ * ↑a₂ = a₁ * ↑b₂
⊢ ↑a₂ * b₁ = ↑b₂ * a₁
simpa only [mul_comm] using H