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