no goals
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type ?u.742376
inst✝ : CommMonoid P
f : LocalizationMap S N
x : M
y : { x // x ∈ S }
⊢ ↑(toMap f) x *
        ↑(↑(IsUnit.liftRight (MonoidHom.restrict (toMap f) S) (_ : ∀ (y : { x // x ∈ S }), IsUnit (↑(toMap f) ↑y)))
              y)⁻¹ *
      ↑(toMap f) ↑y =
    ↑(toMap f) x
rw [mul_assoc, mul_comm _ (f.toMap y), ← mul_assoc, mul_inv_left, mul_comm]