no goals
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type ?u.817224
inst✝ : CommMonoid P
f : LocalizationMap S N
x₁ x₂ : M
y₁ y₂ : { x // x ∈ S }
H : mk' f x₁ y₁ = mk' f x₂ y₂
⊢ ↑(toMap f) (↑y₂ * x₁) = ↑(toMap f) (↑y₁ * x₂)
rw [f.toMap.map_mul, f.toMap.map_mul, f.mk'_eq_iff_eq_mul.1 H,← mul_assoc, mk'_spec',
  mul_comm ((toMap f) x₂) _]
no goals
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type ?u.817224
inst✝ : CommMonoid P
f : LocalizationMap S N
x₁ x₂ : M
y₁ y₂ : { x // x ∈ S }
H : ↑(toMap f) (↑y₂ * x₁) = ↑(toMap f) (↑y₁ * x₂)
⊢ mk' f x₁ y₁ = mk' f x₂ y₂
rw [mk'_eq_iff_eq_mul, mk', mul_assoc, mul_comm _ (f.toMap y₁), ← mul_assoc, ←
  f.toMap.map_mul, mul_comm x₂, ← H, ← mul_comm x₁, f.toMap.map_mul,
  mul_inv_right f.map_units]